Inria Microsoft Joint Centre rue Jean Rostand

Inria Microsoft Joint Centre rue Jean Rostand

-

English
41 Pages
Read
Download
Downloading requires you to have access to the YouScribe library
Learn all about the services we offer

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


Subjects

Informations

Published by
Reads 13
Language English
Report a problem
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?
IGiven a CNF formulaF
(abc)(¬ab)(¬bc)(¬ca)
IF ?admits a model
IFis satisfiable :{a=true,b=true,c=true}is a model
IF ∪ {(¬a∨ ¬b∨ ¬c)}is unsatisfiable
IBad news : SAT is NP-Complete [Cook 71] IGood 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.
(Cx) (D∨ ¬x) ————————-(CD)resolvent
A resolution refutationRFofFsequence of clauses C1 , . .is a . , Cs s.t.
Ieach Ck is either inFor is the resolvent of two clauses Ci and Cj with i, j<k, and ICs is the empty clause
Resolution:an
(xy)
xe
y
amp
(¬z)
(x)
el
z
y
x
(¬y)
z
y
x
(¬yz)
(¬x)
y
(¬xy)
Resolution
There are several popular restrictions to resolution :
ITree-like resolution: in whichRFmust be a tree.
IRegular resolutionin which no variable may be resolved: more than once in any path inRFfrom 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 solversGeneral resolution[Knot 09]
DPLL-like solverTree-Like resolution
et
al.
Denitionsandonatitnos
CNF :F= (¬x1∨ ¬x2x3)(¬x1x2)(¬x2∨ ¬x3)(¬x3)
Partial interpretation:ρ:X⊆ V(F)→ {faux,vrai}
Simplification:F |ρdenotes the formula simplified byρ
Implication:imp(x3) = (x1x2x3),exp(x3) ={x1,x2}
FormulaFclosed by UP:F= (¬x1∨ ¬x2)(¬x1x2)
Resolvent:η[x2,(¬x1x2),(¬x2∨ ¬x3)] = (¬x1∨ ¬x3)
Logical consequence:F|=(¬x1∨ ¬x3)
Logical consequence % UP:F|=c, iff(F |¯c)=
Subsumption
:c1subsumsc2iffc1c2.
lCsasicalLearn
F ⊇ {c1, . . . ,c10}
nig(CD
(c1)¬x2¬x5x6
(c3)¬x6¬x7x8
C
(c5)¬x1¬x8x10
L)
(c7)¬x4¬x9¬x10x12
(c9)¬x11¬x12x14
(c2)
(c4)
(c6)
(c8)
(c10)
¬x5x7
¬x3¬x8x9
¬x4¬x9x11
¬x10x13
¬x13¬x14
Notations:xjiliteralxiassigned at levelj. ρ=h. . .x11. . .¬x711ih(x22). . .x32. . .ih(x43). . .x319. . .i. . . h(x55),x65,x75,x85,x95,x150,x115,x251,x135,x415i
Classical
Learning
(¬x
6
¬x
7
x
8)