> n$(
F/0|DArialNarrowanTT\-ܖ0ܖDTahomaarrowanTT\-ܖ0ܖ" DWingdingsowanTT\-ܖ0ܖ0DTimes New RomanTT\-ܖ0ܖ@DArial NarrowanTT\-ܖ0ܖ"
A.
@n?" dd@ @@``"()
0e0e
A A5% 8c8c
?1 d0u0@Ty2 NP'p<'pA)BCD|E||"0e@ @ABC DEEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN E5% N E5% N F
5%
!"?N@ABC DEFFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `ab@8K ʚ;Ge8ʚ;g42d2dT0bppp@<4dddd k0T8-<4BdBd l0T<4!d!d l0T80___PPT10
pp)*Chaff: Engineering an Efficient SAT SolverBMatthew W.Moskewicz,
Concor F. Madigan, Ying Zhao, Lintao Zhang, Sharad Malik
Princeton University
Presenting: Tamir Heyman
Some are from Malik s presentationPt?Chaff Philosophy Make the core operations fast
profiling driven, most time-consuming parts:
Boolean Constraint Propagation (BCP) and Decision
Emphasis on coding efficiency
Emphasis on optimizing data cache behavior
As always, good search space pruning (i.e. conflict resolution and learning) is important
V-2-2~BCP Algorithm What causes an implication? When can it occur? @(16All literals in a clause but one are assigned to False
(v1 + v2 + v3): implied cases: (0 + 0 + v3) or (0 + v2 + 0) or (v1 + 0 +0)
For an N-literal clause, this can only occur after N-1 of the literals have been assigned to False
So, (theoretically) we could completely ignore the first N-2 assignments to this clause
In reality, we pick two literals in each clause to watch and thus can ignore any assignments to the other literals in the clause.
Example: (v1 + v2 + v3 + v4 + v5)
( v1=X + v2=X + v3=? {i.e. X or 0 or 1} + v4=? + v5=? )
,P+>BCP Algorithm BCP s Invariants $Each clause has two watched literals
If a clause becomes unit via a sequence of assignments, then this sequence will include an assignment of one of the watched literals to F
Example again: (v1 + v2 + v3 + v4 + v5)
( v1=X + v2=X + v3=? + v4=? + v5=? )
BCP consists of identifying unit (and conflict) clauses (and the associated implications) while maintaining the BCP s Invariants
nZZZmBCP Algorithm Example (1/13)$ BCP Algorithm Example (2/13)$BCP Algorithm Example (3/13)$BCP Algorithm Example (4/13)$
BCP Algorithm Example (5/13)$
BCP Algorithm Example (6/13)$BCP Algorithm Example (7/13)$BCP Algorithm Example (8/13)$
BCP Algorithm Example (9/13)$BCP Algorithm Example (10/13)$BCP Algorithm Example (11/13)$BCP Algorithm Example (12/13)$BCP Algorithm Example (13/13)$BCP Algorithm Summary@ During forward progress: Decisions and Implications
Only need to examine clauses where watched literal is set to F
Can ignore any assignments of literals to T
Can ignore any assignments to non-watched literals
During backtrack: Unwind Assignment Stack
Any sequence of chronological unassignments will maintain our invariants
So no action is required at all to unassign variables.
Overall
Minimize clause access
4P?P_P*PIP7PPPP4?_*I7H
A + 0` 33PP` 13` 3333` Q_{` 333fpKNāvI` j@v۩ῑH>?" dd@,?n<d@ `7 `2@`7``2 n?" dd@ @@``PR @ ` `p>>
,Z
(
,
,
<|"
4 0
,
T@d"
4 0
,
<"U_
4 0
,
T䋮d">&
4 0
,
N"P
4 0
,
<X"p
4 0
,
Cx?d?"bUv
4 0
,
< #"`
T Click to edit Master title style!
!$
,
0 "
RClick to edit Master text styles
Second level
Third level
Fourth level
Fifth level!
S
,
6 "]}
F*0
,
6 "] }
H*0
,
6h "]T}
H*0B
,s*h ? 333380___PPT10.(г% Blends}
0 0 (
0T +
0"+bb P@
0#"Dwoh
0
s*"PP
0
Bd" P@bb P
0
0#"Nyh
0
s*"P
0
Bd"P
0z
0
<" a*h
0
s*"
0
f?d?"+)
0
B| ?#"` p
T Click to edit Master title style!
!
0
0~ " `
W#Click to edit Master subtitle style$
$
0
6 "`p
J* 0
0
6 "`p
L*"0
0
6@ "`
L*"0B
0s*h ? 333380___PPT10.(г%*0 *(
x
c$0 p
r
S
0 ` <
H
0h ? 3380___PPT10."!`I$
04$(
4r
4 S) ,
r
4 S4*
,
H
40h ? 333380___PPT10."!$
08$(
8r
8 S4 ,
r
8 S
,
H
80h ? 333380___PPT10.!@0
0<0(
<x
< c$, ,
x
< c$
,
H
<0h ? 333380___PPT10.!@
02*@(
@x
@ c$L ,
@
6Ԯ}M
rv2 + v3 + v1 + v4 + v5
v1 + v2 + v3
v1 + v2
v1 + v4
v1 ::H
@0h ? 333380___PPT10.!@A
00LA(
Lx
L c$" ,
L
6# }M
`rv2 + v3 + v1 + v4 + v5
v1 + v2 + v3
v1 + v2
v1 + v4
v1 :
L
6l2 -
BWatched literals
L
66 7Q
s Initially, we identify any two literals in each clause as the watched ones
Clauses of size one are a special casettH
L0h ? 333380___PPT10.!@l
0@ Pl(
Px
P c$48 ,
P
6**State:(v1=F)
H
P0h ? 333380___PPT10.!@Q
0PTQ(
Tx
T c$TA ,
T
6` }M
lv2 + v3 + v1 + v4 + v5
v1 + v2 + v3
v1 + v2
v1 + v4
7
T
6hn 7b
{To maintain our invariants, we must examine each clause where the
assignment being processed has set a watched literal to F B:|
T
Bu Uw
>State:(v1=F)
XB
T
0DpC- CXB
T
0DpS - S H
T0h ? 333380___PPT10.!@
0`X(
Xx
X c$q ,
X
6t} }M
jv2 + v3 + v1 + v4 + v5
v1 + v2 + v3
v1 + v2
v1 + v46
X
6 7
] To maintain our invariants, we must examine each clause where the
assignment being processed has set a watched literal to F
We need not process clauses where a watched literal has been set to T,
because the clause is now satisfied and so can not become unit.
6C=HD
X
B Uw
>State:(v1=F)
XB
X
0Dpc
- c
H
X0h ? 333380___PPT10.!@2
0p\2(
\x
\ c$ ,
\
6` }M
jv2 + v3 + v1 + v4 + v5
v1 + v2 + v3
v1 + v2
v1 + v46r
\
6p 7
To maintain our invariants, we must examine each clause where the
assignment being processed has set a watched literal to F
We need not process clauses where a watched literal has been set to T,
because the clause is now satisfied and so can not become unit.
We certainly need not process any clauses where neither watch
literal changes state (in this example, where v1 is not watched).bC=HC?E
v
\
BL Uw
>State:(v1=F)
XB
\
0Dp2- 2H
\0h ? 333380___PPT10.!@|
0`|(
`x
` c$ ,
`
6ĸ }M
jv2 + v3 + v1 + v4 + v5
v1 + v2 + v3
v1 + v2
v1 + v46
`
B4Ը Uw
>State:(v1=F)
XB
`
0DpC- C\
`
Nո ?"0@NNN?N
r Now let s actually process the second and third clauses:::XB
`
0DpS - S H
`0h ? 333380___PPT10.!@
04
,
d (
dx
d c$ܸ ,
d
6P }
jv2 + v3 + v1 + v4 + v5
v1 + v2 + v3
v1 + v2
v1 + v46
d
B
>State:(v1=F)
\
d
N ?"0@NNN?N
r Now let s actually process the second and third clauses:::
d
B?"0@NNN?N-d
B For the second clause, we replace v1 with v3 as a new watched literal.
Since v3 is not assigned to F, this maintains our invariants.
d
6p}qm
jv2 + v3 + v1 + v4 + v5
v1 + v2 + v3
v1 + v2
v1 + v46
d
BX
>State:(v1=F)
XB
d
0DpC CH
d0h ? 333380___PPT10.!@f
0 hf(
hx
h c$\9 ,
h
6=}
jv2 + v3 + v1 + v4 + v5
v1 + v2 + v3
v1 + v2
v1 + v46
h
BA
>State:(v1=F)
\
h
N??"0@NNN?N
r Now let s actually process the second and third clauses:::~
h
BLP?"0@NNN?Ns
For the second clause, we replace v1 with v3 as a new watched literal.
Since v3 is not assigned to F, this maintains our invariants.
The third clause is unit. We record the new implication of v2 , and add it to the
queue of assignments to process. Since the clause cannot again become unit,
our invariants are maintained. qM
h
6tX}qm
jv2 + v3 + v1 + v4 + v5
v1 + v2 + v3
v1 + v2
v1 + v46
h
Bh
V
NState:(v1=F)
Pending: (v2=F)XB
h
0DpS S H
h0h ? 333380___PPT10.!@
0H@
l(
lx
l c$2 ,
l
6L- }
jV2 + v3 + v1 + v4 + v5
v1 + v2 + v3
v1 + v2
v1 + v46
l
6F
=
DState:(v1=F, v2=F)z
l
N\ ?"0@NNN?N
t Next, we process v2 . We only examine the first 2 clauses;;: z
l
Bf ?"0@NNN?Ns
~In the first clause, we replace v2 with v4 as a new watched literal. Since v4 is not assigned to F, this maintains our invariants.
The second clause is unit. We record the new implication of v3 , and add it to the queue of assignments to process. Since the clause cannot again become unit, our invariants are maintained@@f?
l
6u }qm
zjv2 + v3 + v1 + v4 + v5
v1 + v2 + v3
v1 + v2
v1 + v46
l
B
V
T"State:(v1=F, v2=F)
Pending: (v3=F)##XB
l
0DpC CXB
l
0Dp20
2H
l0h ? 333380___PPT10.!@
0
p(
px
p c$lQ ,
p
68}
jV2 + v3 + v1 + v4 + v5
v1 + v2 + v3
v1 + v2
v1 + v46
p
6F
JState:(v1=F, v2=F, v3=F)v
p
N$^?"0@NNN?N
p Next, we process v3 . We only examine the first clause.998 b
p
B\ ?"0@NNN?Ns
fFor the first clause, we replace v3 with v5 as a new watched literal. Since v5 is not assigned to F, this maintains our invariants.
Since there are no pending assignments, and no conflict, BCP terminates and we make a decision. Both v4 and v5 are unassigned. Let s say we decide to assign v4=T and proceed.44f3
p
68r}qm
jv2 + v3 + v1 + v4 + v5
v1 + v2 + v3
v1 + v2
v1 + v4 6
p
B|
V
T"State:(v1=F, v2=F, v3=F)
Pending: ##XB
p
0Dp20
2H
p0h ? 333380___PPT10.!@\
0
t\
(
tx
t c$LQ ,
Q
t
6L }
jV2 + v3 + v1 + v4 + v5
v1 + v2 + v3
v1 + v2
v1 + v4 6
t
6Q
PState:(v1=F, v2=F, v3=F, v4=T)1
t
N\, ?"0@NNN?N'
{+ Next, we process v4. We do nothing at all.,,+ L
t
B?"0@NNN?N
JSince there are no pending assignments, and no conflict, BCP terminates and we make a decision. Only v5 is unassigned. Let s say we decide to assign v5=F and proceed 0f
t
64}qm
jv2 + v3 + v1 + v4 + v5
v1 + v2 + v3
v1 + v2
v1 + v4$6
t
B
V
[)State:(v1=F, v2=F, v3=F , v4=T)
Pending: **XB
t
0Dp20
2H
t0h ? 333380___PPT10.!@
0:
2
x (
xx
x c$h ,/
x
6 Q}
jV2 + v3 + v1 + v4 + v5
v1 + v2 + v3
v1 + v2
v1 + v4$6
x
6
V$State:(v1=F, v2=F, v3=F, v4=T, v5=F)%%
x
NQ?"0@NNN?NT
d Next, we process v5=F
x
BX-Q?"0@NNN?N
,The first clause is already satisfied by v4 so we ignore it.
Since there are no pending assignments, and no conflict, BCP terminates and we make a decision. No variables are unassigned, so the instance is SAT, and we are done.f
x
6hDJ
}qm
jv2 + v3 + v1 + v4 + v5
v1 + v2 + v3
v1 + v2
v1 + v4$6
x
6Q
X&State:(v1=F, v2=F, v3=F , v4=T , v5=F)''XB
x
0Dp]
H
x0h ? 333380___PPT10.!@0
0
|0(
|~
| s*@ ,
r
| Sp
,
H
|0h ? 333380___PPT10.!@r\v$ 3=?B/DgF1IzNSGZ`hn\yʅT·1z+(
F/0|DArialNarrowanhh\-0DTahomaarrowanhh\-0" DWingdingsowanhh\-00DTimes New Romanhh\-0@DArial NarrowanhOh+'009hp
,8@,Chaff: Engineering an Efficient SAT Solvertamirh heymanBlendstamirh heyman6Microsoft Office PowerPoint@pA@="!@pԋ1"qG7g Qy--$xx--'33--$,44,,--'-::--$,55,,--ff--$,5
5
,,----$
,
55,
,----$,55,,----$,55,,----$,55,,---'--$4<<44--'---$
3
<<3
3--X--$3<<33----$3<<33----$3<<33----$3<<33----$3<<33----$3<<33---'QA
2(
~~ll[[JJ99%%rraaOO>>--xxffUUDD5678&'()
0123 !"4$+,-./&'()
* !"#$%
'--$*==**--'---$89988-- --$89988--"""--$89988--$$$--$89 9 88--&&&--$ 8 9
9
8 8--)))--$
8
998
8--+++--$89988-------$89988--000--$89988--222--$89988--444--$89988--666--$89988--888--$89988--:::--$89988--===--$89988--???--$89988--AAA--$89988--CCC--$89988--EEE--$89988--HHH--$89988--JJJ--$89988--LLL--$89988--NNN--$89988--QQQ--$89988--SSS--$89 9 88--UUU--$ 8 9!9!8 8--WWW--$!8!9"9"8!8--YYY--$"8"9#9#8"8--[[[--$#8#9$9$8#8--]]]--$$8$9%9%8$8--___--$%8%9&9&8%8--aaa--$&8&9'9'8&8--ddd--$'8'9(9(8'8--fff--$(8(9)9)8(8--hhh--$)8)9*9*8)8--jjj--$*8*9+9+8*8--lll--$+8+9,9,8+8--nnn--$,8,9-9-8,8--ppp--$-8-9.9.8-8--sss--$.8.9/9/8.8--uuu--$/8/90908/8--www--$0809191808--zzz--$1819292818--|||--$2829393828--~~~--$3839494838----$4849595848----$5859696858----$6869797868----$7879898878----$8889999888----$9899:9:898----$:8:9;9;8:8----$;8;9<9<8;8----$<8<9=9=8<8----$=8=9>9>8=8----$>8>9?9?8>8----$?8?9@9@8?8----$@8@9A9A8@8----$A8A9B9B8A8----$B8B9C9C8B8----$C8C9D9D8C8----$D8D9E9E8D8----$E8E9G9G8E8----$G8G9H9H8G8----$H8H9I9I8H8----$I8I9J9J8I8----$J8J9K9K8J8----$K8K9L9L8K8----$L8L9M9M8L8----$M8M9N9N8M8----$N8N9O9O8N8----$O8O9P9P8O8----$P8P9Q9Q8P8----$Q8Q9S9S8Q8----$S8S9T9T8S8----$T8T9V9V8T8----$V8V9W9W8V8----$W8W9Y9Y8W8----$Y8Y9Z9Z8Y8----$Z8Z9[9[8Z8----$[8[9]9]8[8----$]8]9^9^8]8----$^8^9`9`8^8----$`8`9a9a8`8----$a8a9c9c8a8----$c8c9d9d8c8----$d8d9f9f8d8----$f8f9h9h8f8----$h8h9j9j8h8----$j8j9l9l8j8----$l8l9n9n8l8----$n8n9p9p8n8----$p8p9r9r8p8----$r8r9t9t8r8----$t8t9w9w8t8----$w8w9y9y8w8----$y8y9{9{8y8----${8{998{8----$89988----$89988----$89988----$89988----$89988----$89988---'@"Tahoma-. 3372
( Chaff: Engineering an Efficient ."System07-@"Tahoma-. 332
4
SAT Solver.-@"Tahoma-. 2
I5Matthew .-@"Tahoma-. 2
ILW.Moskewiczn.-@"Tahoma-.
2
Ii, .-@"Tahoma-. 2
OConcor.-@"Tahoma-. *2
O-F. Madigan, Ying Zhao, .-@"Tahoma-. 2
OfLintao.-@"Tahoma-. 2
OvZhang, .-@"Tahoma-. 2
TASharad.-@"Tahoma-. 2
TTMalikd.-@"Tahoma-. %2
[9Princeton University.-@"Tahoma-. -2
h1Presenting: Tamir Heyman i.-@"Tahoma-. 2
n'Some are from .-@"Tahoma-. 2
nLMalikd.-@"Tahoma-. 2
nW.-@"Tahoma-. 2
nXs.-@"Tahoma-. 2
n\presentation.-maarrowanhh\-0" DWingdingsowanhh\-00DTimes New Romanhh\-0@DArial Narrowanhh\-0"PD[SOal Narrowanhh\-0`DSymbolarrowanhh\-0
A.
@n?" dd@ @@`` /()
"#$&()*+,.0e0e
A A5% 8c8c
?1 d0u0@Ty2 NP'p<'pA)BCD|E||"0e@ @ABC DEEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN E5% N E5% N F
5%
!"?N@ABC DEFFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `ab@8[K ʚ;Ge8ʚ;g42d2dT0bppp@<4dddd4k0h8-<4BdBd4l0h<4!d!d4l0h___PPT10D[SOalx}0=XQhh0DArialx}0=XQhh0
pp+*Chaff: Engineering an Efficient SAT SolverBMatthew W.Moskewicz,
Concor F. Madigan, Ying Zhao, Lintao Zhang, Sharad Malik
Princeton University
Presenting: Tamir Heyman
Some are from Malik s presentationPt?Chaff Philosophy Make the core operations fast
profiling driven, most time-consuming parts:
Boolean Constraint Propagation (BCP) and Decision
Emphasis on coding efficiency
Emphasis on optimizing data cache behavior
As always, good search space pruning (i.e. conflict resolution and learning) is important
V-2-2 .Chaff s Main ProceduresEfficient BCP
Two watched literals
Fast back tracking
Efficient Decision procedure
Localizes search space
Restart
Increases robustnesst((~BCP Algorithm What causes an implication? When can it occur? @(16All literals in a clause but one are assigned to False
(v1 + v2 + v3): implied cases: (0 + 0 + v3) or (0 + v2 + 0) or (v1 + 0 +0)
For an N-literal clause, this can only occur after N-1 of the literals have been assigned to False
So, (theoretically) we could completely ignore the first N-2 assignments to this clause
In reality, we pick two literals in each clause to watch and thus can ignore any assignments to the other literals in the clause.
Example: (v1 + v2 + v3 + v4 + v5)
( v1=X + v2=X + v3=? {i.e. X or 0 or 1} + v4=? + v5=? )
,P+>BCP Algorithm BCP s Invariants $Each clause has two watched literals
If a clause becomes unit via a sequence of assignments, then this sequence will include an assignment of one of the watched literals to F
Example again: (v1 + v2 + v3 + v4 + v5)
( v1=X + v2=X + v3=? + v4=? + v5=? )
BCP consists of identifying unit (and conflict) clauses (and the associated implications) while maintaining the BCP s Invariants
nZZZmBCP Algorithm Example (1/13)$ BCP Algorithm Example (2/13)$BCP Algorithm Example (3/13)$BCP Algorithm Example (4/13)$
BCP Algorithm Example (5/13)$
!"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\^_`abcdefghijklmnopqrstuvwxy{|}~zRoot EntrydO)p 1"Current UserGSummaryInformation(]`9PowerPoint Document(DocumentSummaryInformation8h\-0"
A.
@n?" dd@ @@``P)()
"#$&(0e0e
A A5% 8c8c
?1 d0u0@Ty2 NP'p<'pA)BCD|E||"0e@ @ABC DEEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN E5% N E5% N F
5%
!"?N@ABC DEFFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `ab@8K ʚ;Ge8ʚ;g42d2dT0bppp@<4dddd4k0h8-<4BdBd4l0h<4!d!d4l0h80___PPT10
pp*Chaff: Engineering an Efficient SAT SolverBMatthew W.Moskewicz,
Concor F. Madigan, Ying Zhao, Lintao Zhang, Sharad Malik
Princeton University
Presenting: Tamir Heyman
Some are from Malik s presentationPt?Chaff Philosophy Make the core operations fast
profiling driven, most time-consuming parts:
Boolean Constraint Propagation (BCP) and Decision
Emphasis on coding efficiency
Emphasis on optimizing data cache behavior
As always, good search space pruning (i.e. conflict resolution and learning) is important
V-2-2~BCP Algorithm What causes an implication? When can it occur? @(16All literals in a clause but one are assigned to False
(v1 + v2 + v3): implied cases: (0 + 0 + v3) or (0 + v2 + 0) or (v1 + 0 +0)
For an N-literal clause, this can only occur after N-1 of the literals have been assigned to False
So, (theoretically) we could completely ignore the first N-2 assignments to this clause
In reality, we pick two literals in each clause to watch and thus can ignore any assignments to the other literals in the clause.
Example: (v1 + v2 + v3 + v4 + v5)
( v1=X + v2=X + v3=? {i.e. X or 0 or 1} + v4=? + v5=? )
,P+>BCP Algorithm BCP s Invariants $Each clause has two watched literals
If a clause becomes unit via a sequence of assignments, then this sequence will include an assignment of one of the watched literals to F
Example again: (v1 + v2 + v3 + v4 + v5)
( v1=X + v2=X + v3=? + v4=? + v5=? )
BCP consists of identifying unit (and conflict) clauses (and the associated implications) while maintaining the BCP s Invariants
nZZZmBCP Algorithm Example (1/13)$ BCP Algorithm Example (2/13)$BCP Algorithm Example (3/13)$BCP Algorithm Example (4/13)$
BCP Algorithm Example (5/13)$
BCP Algorithm Example (6/13)$BCP Algorithm Example (7/13)$BCP Algorithm Example (8/13)$
BCP Algorithm Example (9/13)$BCP Algorithm Example (10/13)$BCP Algorithm Example (11/13)$BCP Algorithm Example (12/13)$BCP Algorithm Example (13/13)$BCP Algorithm Summary@ During forward progress: Decisions and Implications
Only need to examine clauses where watched literal is set to F
Can ignore any assignments of literals to T
Can ignore any assignments to non-watched literals
During backtrack: Unwind Assignment Stack
Any sequence of chronological unassignments will maintain our invariants
So no action is required at all to unassign variables.
Overall
Minimize clause access
4P?P_P*PIP7PPPP4?_*I7H
A + Chaff Decision HeuristicVSIDS@ Variable State Independent Decaying Sum
Rank variables by literal count in the initial clause database
Only increment counts as new clauses are added.
Periodically, divide all counts by a constant.*(( VSIDS Example (1/3)@ VSIDS Example (2/3)@ VSIDS Example (3/3)@ (Chaff Decision HeuristicVSIDS - Summary))@( ~Quasi-static:
Static because it doesn t depend on variable state
Not static because it gradually changes as new clauses are added
Decay causes bias toward *recent* conflicts.
Use heap to find unassigned variable with the highest ranking
Even single linear pass though variables on each decision would dominate run-time!xt->St->R? 6
0 6(
~
s* ,
x
c$
,
H
0h ? 333380___PPT10.!@B
0@B(
~
s*_ ,
.
Nb?"0@NNN?NB
xFInitial data base
x1 + x4
x1 + x3 + x8
x1 + x8 + x12
x2 + x11
x7 + x3 + x9
x7 + x8 + x9
x7 + x8 + x10
Scores:
4: x8
3: x1,x7
2: x3
1: x2,x4,x9,x10,x11,x12N
N|&?"0@NNN?N
fNew clause added
x1 + x4
x1 + x3 + x8
x1 + x8 + x12
x2 + x11
x7 + x3 + x9
x7 + x8 + x9
x7 + x8 + x10
x7 + x10 + x12
Scores:
4: x8,x7
3: x1
2: x3,x10,x12
1: x2,x4,x9,x11
H
0h ? 333380___PPT10.!@
0z`(
~
s* ,
T
N0:
?"0@NNN?NTm
lCounters divided by 2
x1 + x4
x1 + x3 + x8
x1 + x8 + x12
x2 + x11
x7 + x3 + x9
x7 + x8 + x9
x7 + x8 + x10
x7 + x10 + x12
Scores:
2: x8,x7, x1
1: x3,x10,x12
0: x2,x4,x9,x11
H
0h ? 333380___PPT10.!@H
0H(
~
s* ,
N?"0@NNN?NTmI
Counters divided by 2 before new clause added
x1 + x4
x1 + x3 + x8
x1 + x8 + x12
x2 + x11
x7 + x3 + x9
x7 + x8 + x9
x7 + x8 + x10
x7 + x10 + x12
Scores:
3: x7
2: x8,x7
1: x3,x10,x12
0: x2,x4,x9,x11
H
0h ? 333380___PPT10.!@6
006(
~
s*, ,
x
c$
,
H
0h ? 333380___PPT10.!@r JP
Tn&1:(
/0DArialarrowanhh\-0DTaho
՜.+,0
$SOn-screen ShowCarnegie Mellon UniversityH$ArialTahoma
WingdingsTimes New Roman
Arial Narrow宋体SymbolBlends+Chaff: Engineering an Efficient SAT SolverChaff PhilosophyChaff’s Main ProceduresDBCP Algorithm What “causes” an implication? When can it occur?"BCP Algorithm BCP’s InvariantsBCP Algorithm Example (1/13)BCP Algorithm Example (2/13)BCP Algorithm Example (3/13)BCP Algorithm Example (4/13)BCP Algorithm Example (5/13)BCP Algorithm Example (6/13)BCP Algorithm Example (7/13)BCP Algorithm Example (8/13)BCP Algorithm Example (9/13)BCP Algorithm Example (10/13)BCP Algorithm Example (11/13)BCP Algorithm Example (12/13)BCP Algorithm Example (13/13)BCP Algorithm SummaryChaff Decision Heuristic VSIDSVSIDS Example (1/3)VSIDS Example (2/3)VSIDS Example (3/3))Chaff Decision Heuristic VSIDS - Summary,Interplay of BCP and the Decision Heuristic1Interpl%_܆
0tamirh heymantamirh heymanay of Learning and the Decision HeuristicRestart TimeLiBCP Algorithm Example (6/13)$BCP Algorithm Example (7/13)$BCP Algorithm Example (8/13)$
BCP Algorithm Example (9/13)$BCP Algorithm Example (10/13)$BCP Algorithm Example (11/13)$BCP Algorithm Example (12/13)$BCP Algorithm Example (13/13)$BCP Algorithm Summary@ During forward progress: Decisions and Implications
Only need to examine clauses where watched literal is set to F
Can ignore any assignments of literals to T
Can ignore any assignments to non-watched literals
During backtrack: Unwind Assignment Stack
Any sequence of chronological unassignments will maintain our invariants
So no action is required at all to unassign variables.
Overall
Minimize clause access
4P?P_P*PIP7PPPP4?_*I7H
A + Chaff Decision HeuristicVSIDS@ Variable State Independent Decaying Sum
Rank variables by literal count in the initial clause database
Only increment counts as new clauses are added.
Periodically, divide all counts by a constant.*(( VSIDS Example (1/3)@ VSIDS Example (2/3)@ VSIDS Example (3/3)@ (Chaff Decision HeuristicVSIDS - Summary))@( ~Quasi-static:
Static because it doesn t depend on variable state
Not static because it gradually changes as new clauses are added
Decay causes bias toward *recent* conflicts.
Use heap to find unassigned variable with the highest ranking
Even single linear pass though variables on each decision would dominate run-time!xt->St->R? +Interplay of BCP and the Decision HeuristicThis is only an intuitive description &
Reality depends heavily on specific instance
Take some variable ranking (from the decision engine)
Assume several decisions are made
Say v2=T, v7=F, v9=T, v1=T (and any implications thereof)
Then a conflict is encountered that forces v2=F
The next decisions may still be v7=F, v9=T, v1=T !
VSIDS variable ranks change slowly&
But the BCP engine has recently processed these assignments &
so these variables are unlikely to still be watched.
In a more general sense, the more active a variable is, the more likely it is to *not* be watched.@(Z-Z6Z"Z:Z0Z3Z$Z?Z5ZeZ(-6":03?#e0Interplay of Learning and the Decision HeuristicPAgain, this is an intuitive description &
Learnt clauses capture relationships between variables
Learnt clauses bias decision strategy to a smaller set of variables through decision heuristics like VSIDS
Important when there are 100k variables!
Decision heuristic influences which variables appear in learnt clauses
Decisions !implications !conflicts !learnt clause
Important for decisions to keep search strongly localizedZ*ZGZ2Z:Z*G
(":RestartAbandon the current search tree and reconstruct a new one
Helps reduce variance - adds to robustness in the solver
The clauses learned prior to the restart are still there after the restart and can help pruning the search space8BB8B TimeLine$
0$(
r
S\# ,
r
S
,
H
0h ? 333380___PPT10."T$
0$(
r
S ,
r
S࿉
,
H
0h ? 333380___PPT10."9>$
0$(
r
S ,
r
S%
,
H
0h ? 333380___PPT10."`Ų$
0$(
r
SL* ,
r
S
,
H
0h ? 333380___PPT10."W
0(
r
S( ,
^B
6DԔ\@\^
6
[^
6
J^
6
]^
6
_^
6
R^
6
z ^
6
P^
6
cX
0
9
BL}b
$1986
BDD
100 var>0 b b
B
b
&1992
GSAT
300 var>0
b bX
Bl
h=
41996
Stlmarck
1000 var
b0bbbb,
B
$1996
GRASP
1k var>0bb
Bz
G
1960
DP
10 var>0bb,
6
!
,1988
SOCRATES
3k var\0bbbb*
Bx^
,1994
Hannibal
3k varN0bbb
B|
bG
"1962
DLL
10 var>0 bb
Bd6 bw
&2001
Chaff
10k var>0bb
<` F
"1996
SATO
1k var>0
bbH
0h ? 333380___PPT10."pĖr HP&4R6~8:1$K 1:(
/0DArialarrowanTT\-ܖ0ܖDTahomaarrowanTT\-ܖ0ܖ" DWingdingsowanTT\-ܖ0ܖ0DTimes New RomanTT\-ܖ0ܖ@DArial NarrowanTT\-ܖ0ܖ"PD[SOneFonts UsedDesign Template
Slide Titlesal NarrowanTT\-ܖ0ܖ`DSymbolarrowanTT\-ܖ0ܖ
A.
@n?" dd@ @@`` /()
"#$&()*+,.0e0e
A A5% 8c8c
?1 d0u0@Ty2 NP'p<'pA)BCD|E||"0e@ @ABC DEEFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `abN E5% N E5% N F
5%
!"?N@ABC DEFFGHIJK5%LMNOPQRSTUWYZ[ \]^_ `ab@8[K ʚ;Ge8ʚ;g42d2dT0bppp@<4dddd k0T8-<4BdBd l0T<4!d!d l0T___PPT10D[SOaldx}0=XQTTx0xDArialdx}0=XQTTx0x
pp+*Chaff: Engineering an Efficient SAT SolverBMatthew W.Moskewicz,
Concor F. Madigan, Ying Zhao, Lintao Zhang, Sharad Malik
Princeton University
Presenting: Tamir Heyman
Some are from Malik s presentationPt?Chaff Philosophy Make the core operations fast
profiling driven, most time-consuming parts:
Boolean Constraint Propagation (BCP) and Decision
Emphasis on coding efficiency
Emphasis on optimizing data cache behavior
As always, good search space pruning (i.e. conflict resolution and learning) is important
V-2-2 .Chaff s Main ProceduresEfficient BCP
Two watched literals
Fast back tracking
Efficient Decision procedure
Localizes search space
Restart
Increases robustnesst((~BCP Algorithm What causes an implication? When can it occur? @(16All literals in a clause but one are assigned to False
(v1 + v2 + v3): implied cases: (0 + 0 + v3) or (0 + v2 + 0) or (v1 + 0 +0)
For an N-literal clause, this can only occur after N-1 of the literals have been assigned to False
So, (theoretically) we could completely ignore the first N-2 assignments to this clause
In reality, we pick two literals in each clause to watch and thus can ignore any assignments to the other literals in the clause.
Example: (v1 + v2 + v3 + v4 + v5)
( v1=X + v2=X + v3=? {i.e. X or 0 or 1} + v4=? + v5=? )
,P+>BCP Algorithm BCP s Invariants $Each clause has two watched literals
If a clause becomes unit via a sequence of assignments, then this sequence will include an assignment of one of the watched literals to F
Example again: (v1 + v2 + v3 + v4 + v5)
( v1=X + v2=X + v3=? + v4=? + v5=? )
BCP consists of identifying unit (and conflict) clauses (and the associated implications) while maintaining the BCP s Invariants
nZZZmBCP Algorithm Example (1/13)$ BCP Algorithm Example (2/13)$BCP Algorithm Example (3/13)$BCP Algorithm Example (4/13)$
BCP Algorithm Example (5/13)$
BCP Algorithm Example (6/13)$BCP Algorithm Example (7/13)$BCP Algorithm Example (8/13)$
BCP Algorithm Example (9/13)$BCP Algorithm Example (10/13)$BCP Algorithm Example (11/13)$BCP Algorithm Example (12/13)$BCP Algorithm Example (13/13)$BCP Algorithm Summary@ During forward progress: Decisions and Implications
Only need to examine clauses where watched literal is set to F
Can ignore any assignments of literals to T
Can ignore any assignments to non-watched literals
During backtrack: Unwind Assignment Stack
Any sequence of chronological unassignments will maintain our invariants
So no action is required at all to unassign variables.
Overall
Minimize clause access
4P?P_P*PIP7PPPP4?_*I7H
A + Chaff Decision HeuristicVSIDS@ Variable State Independent Decaying Sum
Rank variables by literal count in the initial clause database
Only increment counts as new clauses are added.
Periodically, divide all counts by a constant.*(( VSIDS Example (1/3)@ VSIDS Example (2/3)@ VSIDS Example (3/3)@ (Chaff Decision HeuristicVSIDS - Summary))@( ~Quasi-static:
Static because it doesn t depend on variable state
Not static because it gradually changes as new clauses are added
Decay causes bias toward *recent* conflicts.
Use heap to find unassigned variable with the highest ranking
Even single linear pass though variables on each decision would dominate run-time!xt->St->R? +Interplay of BCP and the Decision HeuristicThis is only an intuitive description &
Reality depends heavily on specific instance
Take some variable ranking (from the decision engine)
Assume several decisions are made
Say v2=T, v7=F, v9=T, v1=T (and any implications thereof)
Then a conflict is encountered that forces v2=F
The next decisions may still be v7=F, v9=T, v1=T !
VSIDS variable ranks change slowly&
But the BCP engine has recently processed these assignments &
so these variables are unlikely to still be watched.
In a more general sense, the more active a variable is, the more likely it is to *not* be watched.@(Z-Z6Z"Z:Z0Z3Z$Z?Z5ZeZ(-6":03?#e0Interplay of Learning and the Decision HeuristicPAgain, this is an intuitive description &
Learnt clauses capture relationships between variables
Learnt clauses bias decision strategy to a smaller set of variables through decision heuristics like VSIDS
Important when there are 100k variables!
Decision heuristic influences which variables appear in learnt clauses
Decisions !implications !conflicts !learnt clause
Important for decisions to keep search strongly localizedZ*ZGZ2Z:Z*G
(":RestartAbandon the current search tree and reconstruct a new one
Helps reduce variance - adds to robustness in the solver
The clauses learned prior to the restart are still there after the restart and can help pruning the search space8BB8B TimeLinerLK̆ 1Root EntrydO):t"Current User8SummaryInformation(]`9PowerPoint Document(z
mple (11/13)BCP Algorithm Example (12/13)BCP Algorithm Example (13/13)BCP Algorithm SummaryChaff Decision Heuristic VSIDSVSIDS Example (1/3)VSIDS Example (2/3)VSIDS Example (3/3))Chaff Decision Heuristic VSIDS - Summary,Interplay of BCP and the Decision Heuristic1Interpl _܆cbartziscbartzis heymanay of Learning and the Decision HeuristicRestart TimeLi**