Inria Microsoft Joint Centre rue Jean Rostand

Said Jabbour

Description

Niveau: Supérieur
Learning in SAT Saıd Jabbour Inria-Microsoft Joint Centre 28 rue Jean Rostand 91893 Orsay Cedex, France LIX Seminar, January 21, 2010

• sat


• known refutation system


• modern sat


• generateconflict-clause


• conflict learning


• solvers can

Sujets

• Microsoft

Informations

• Publié par: profil-nechor-2012
• Nombre de lectures: 13
• Langue: English

Extrait

Learning

in

SAT

Sa¨d Jabbour ı

Inria-Microsoft Joint Centre 28 rue Jean Rostand 91893 Orsay Cedex, France

LIX Seminar, January 21, 2010

Outline

SAT : Definitions and Motivations

Architecture of Modern SAT Solvers

Definitions and notations

Classical Learning (CDCL)

Learning for Backjumping : an extention

Learning for Subsumption

Learning for Dynamic Assignment Reordering

Practical Benefits

Conclusion and perspectives

SAT?

I Given a CNF formulaF

(a∨b∨c)∧(¬a∨b)∧(¬b∨c)∧(¬c∨a)

I F ?admits a model

I Fis satisfiable :{a=true,b=true,c=true}is a model

I F ∪ {(¬a∨ ¬b∨ ¬c)}is unsatisfiable

I Bad news : SAT is NP-Complete [Cook 71] I Good news : Modern SAT solvers can solve structured instances with millions of variables and clauses in few seconds !

Moder

n

SAT

solvers

:

architecture

Resolution

Resolution is a well-known refutation system for sets of clauses F(the axioms), or, equivalently, propositional formulae in CNF. It operates with the single resolution rule.

(C∨x) (D∨ ¬x) ————————- (C∨D)←resolvent

A resolution refutationR F ofFsequence of clauses C1 , . .is a . , Cs s.t.

I each Ck is either inFor is the resolvent of two clauses Ci and Cj with i, j<k, and I Cs is the empty clause⊥

Resolution:an

(x∨y)

xe

y

amp

(¬z)

(x)

el

z

y

x

(¬y)

⊥

z

y

x

(¬y∨z)

(¬x)

y

(¬x∨y)

Resolution

There are several popular restrictions to resolution :

I Tree-like resolution: in whichR F must be a tree.

I Regular resolutionin which no variable may be resolved: more than once in any path inR F from an axiom to the empty clause.

Each of these is provably exponentially weaker than general resolution.

Learning

I

Conflict Driven Clause Learning (CDCL) [J. M. Silva et al. 96, M. Moskewicz et al. 01]is a fundamental component of Modern SAT solvers

I

I

Modern SAT solvers≈General resolution[Knot 09]

DPLL-like solver≈Tree-Like resolution

et

al.

Definitionsandonatitnos

CNF :F= (¬x 1 ∨ ¬x 2 ∨x 3 )∧(¬x 1 ∨x 2 )∧(¬x 2 ∨ ¬x 3 )∧(¬x 3 )

Partial interpretation:ρ:X⊆ V(F)→ {faux,vrai}

Simplification:F | ρ denotes the formula simplified byρ

−→ −→ Implication:imp(x 3 ) = (x 1 ∧x 2 →x 3 ),exp(x 3 ) ={x 1 ,x 2 }

FormulaFclosed by UP:F ∗ = (¬x 1 ∨ ¬x 2 )∧(¬x 1 ∨x 2 )

Resolvent:η[x 2 ,(¬x 1 ∨x 2 ),(¬x 2 ∨ ¬x 3 )] = (¬x 1 ∨ ¬x 3 )

Logical consequence:F|=(¬x 1 ∨ ¬x 3 )

Logical consequence % UP:F|= ∗ c, iff(F | ¯ c ) ∗ =⊥

Subsumption

:c 1 subsumsc 2 iffc 1 ⊆c 2 .

lCsasicalLearn

F ⊇ {c 1 , . . . ,c 10 }

nig(CD

(c 1 )¬x 2 ∨¬x 5 ∨x 6

(c 3 )¬x 6 ∨¬x 7 ∨x 8

C

(c 5 )¬x 1 ∨¬x 8 ∨x 10

L)

(c 7 )¬x 4 ∨¬x 9 ∨¬x 10 ∨x 12

(c 9 )¬x 11 ∨¬x 12 ∨x 14

(c 2 )

(c 4 )

(c 6 )

(c 8 )

(c 10 )

¬x 5 ∨x 7

¬x 3 ∨¬x 8 ∨x 9

¬x 4 ∨¬x 9 ∨x 11

¬x 10 ∨x 13

¬x 13 ∨¬x 14

Notations:x j i literalx i assigned at levelj. ρ=h. . .x 11 . . .¬x 7 1 1 ih(x 22 ). . .x 32 . . .ih(x 43 ). . .x 3 19 . . .i. . . h(x 55 ),x 65 ,x 75 ,x 85 ,x 95 ,x 1 5 0 ,x 11 5 ,x 2 5 1 ,x 13 5 ,x 41 5 i

Classical

Learning

(¬x

6

∨

¬x

7

∨

x

8)