1Chaff: Engineering an Efficient SAT SolverMatthew W.Moskewicz, Concor F. Madigan, Ying Zhao, Lintao Zhang, Sharad MalikPrinceton UniversitySlides: Tamir Heyman Some are from Malik’s presentationLast modified by Will Klieber on Sep 7, 20112Boolean Algebra Notation “+” denotes logical OR (“∨”). “ · ” denotes logical AND (“∧”). Overbar or postfix “ ’ ” denotes negation. Example:“(A ∨ (¬B ∧ C))” corresponds to“(A + (B’ · C))”.3Chaff Philosophy Make the core operations fastprofiling driven, most time-consuming parts:Boolean Constraint Propagation (BCP) and Decision Emphasis on coding efficiency Emphasis on optimizing data cache behavior Search space pruning: conflict resolution and learning4Chaff’s Main Procedures Efficient BCP Two watched literalsFast backtracking Efficient decision heuristicLocalizes search space RestartsIncreases robustness5Implication What “causes” an implication? When can it occur? All literals in a clause but one are assigned False.6Implication example The clause (v1 + v2 + v3) implies values only in the following cases. In case (F + F + v3) implies v3=T In case (F + v2 + F) implies v2=T In case (v1 + F + F) implies v1=T7Implication for N-literal clause Implication occurs after N-1 assignments to False to its literals. We can ignore the first N-2 assignments to this clause. The first N-2 assignments won’t have any effect on the BCP.8Watched LiteralsEach clause has two watched literals.Ignore any assignments to the other literals in the clause.BCP maintains the following invariant: By the end of BCP, one of the watched literalsis true or both are unassigned.(Can watch a false literal only if other watch is true.) Guaranteed to find all implications found by normal unit prop.9BCP with watched Literals Identifying conflict clauses Identifying unit clauses Identifying associated implications Maintaining “BCP Invariant”10Example (1/13)v2 + v3 + v1 + v4v1 + v2 + v3’v1 + v2’v1’+ v4(v1’ ) means (¬v1)Input formula has the following clauses:11Example (2/13)v2v2 + v3v3 + v1 + v4v1v1 + v2v2 + v3’v1 + v2’v1’+ v4Watched literalsInitially, we identify any two literals in each clause as the watched ones(v1’ ) means (¬v1)12Example (3/13)v2v2 + v3v3 + v1 + v4v1v1 + v2v2 + v3’v1 + v2’v1’+ v4Stack:(v1=F)Assume we decide to set v1 the value F13Example (4/13)v2v2 + v3v3 + v1 + v4v1v1 + v2v2 + v3’v1 + v2’v1’+ v4• Ignore clauses with a watched literal whose value is T.•(Such clauses are already satisified.)Stack:(v1=F)14Example (5/13)v2v2 + v3v3 + v1 + v4v1v1 + v2v2 + v3’v1 + v2’v1’+ v4• Ignore clauses where neither watched literal value changesStack:(v1=F)15Example (6/13)v2v2 + v3v3 + v1 + v4v1v1 + v2v2 + v3’v1 + v2’v1’+ v4•Examine clauses with a watched literal whose value is FStack:(v1=F)16Example (7/13)v2v2 + v3v3 + v1 + v4v1v1 + v2v2 + v3’v1 + v2’v1’+ v4v2v2 + v3v3 + v1 + v4v1v1 + v2v2 + v3’v1 + v2’v1’+ v417Example (7/13)Stack:(v1=F)• In the second clause, replace the watched literal v1 with v3’v2v2 + v3v3 + v1 + v4v1v1 + v2v2 + v3’v1 + v2’v1’+ v4Stack:(v1=F)v2v2 + v3v3 + v1 + v4v1v1 + v2v2 + v3’v1 + v2’v1’+ v418Example (8/13)v2v2 + v3v3 + v1 + v4v1 + v2v2 + v3’v1 + v2’v1’+ v4Stack:(v1=F)• The third clause is a unit and implies v2=F• We record the new implication, and add it to aqueue of assignments to process.v2v2 + v3v3 + v1 + v4v1v1 + v2v2 + v3’v1 + v2’v1’+ v4Stack:(v1=F)Pending: (v2=F)19Example (9/13)v2 + v3 + v1 + v4v1 + v2 + v3’v1 + v2’v1’+ v4Stack:(v1=F, v2=F)• Next, we process v2. • We only examine the first 2 clausesv2 + v3 + v1 + v4v1 + v2 + v3’v1 + v2’v1’+ v4Stack:(v1=F, v2=F)Pending: (v3=F)20Example (10/13)v2 + v3 + v1 + v4 v1 + v2 + v3’v1 + v2’v1’+ v4Stack:(v1=F, v2=F)• In the first clause, we replace v2 with v4 • The second clause is a unit and implies v3=F • We record the new implication, and add it to the queuev2 + v3 + v1 + v4v1 + v2 + v3’v1 + v2’v1’+ v4Stack:(v1=F, v2=F)Pending: (v3=F)21Example (11/13)v2 + v3 + v1 + v4v1 + v2 + v3’v1 + v2’v1’+ v4Stack:(v1=F, v2=F, v3=F)•Next, we process v3’. We only examine the first clause.v2 + v3 + v1 + v4v1 + v2 + v3’v1 + v2’v1’+ v4Stack:(v1=F, v2=F, v3=F)Pending: ()22Example (12/13)v2 + v3 + v1 + v4v1 + v2 + v3’v1 + v2’v1’+ v4Stack:(v1=F, v2=F, v3=F)• The first clause is a unit and implies v4=T.• We record the new implication, and add it to the queue.v2 + v3 + v1 + v4v1 + v2 + v3’v1 + v2’v1’+ v4Stack:(v1=F, v2=F, v3=F)Pending: (v4=T)23Example (13/13)Stack:(v1=F, v2=F, v3=F, v4=T)• There are no pending assignments, and no conflict• Therefore, BCP terminates and so does the SAT solverv2 + v3 + v1 + v4v1 + v2 + v3’v1 + v2’v1’+ v424Identify conflictsStack:(v1=F, v2=F, v3=F)• What if the first clause does not have v4? • When processing v3’, we examine the first clause.• This time, there is no alternative literal to watch.• BCP returns a conflictv2 + v3 + v1v1 + v2 + v3’v1 + v2’v1’+ v425BacktrackStack:()• We do not need to move any watched literalv2 + v3 + v1v1 + v2 + v3’v1 + v2’v1’+ v426BCP Summary During forward progress (decisions, implications)Examine clauses where watched literal is set to FIgnore clauses with assignments of literals to TIgnore clauses with assignments to non-watched literals27Backtrack Summary Unwind Assignment Stack No action is applied to the watched literals Overall Minimize clause access28Chaff Decision Heuristic VSIDS Variable State Independent Decaying Sum Rank variables based on literal count in the initial clause database. Only increment counts as new clauses are added. Periodically, divide all counts by a constant.29VSIDS Example (1/2)Initial data basex1 + x4x1 + x3’ + x8’x1 + x8 + x12x2 + x11x7’ + x3’ + x9x7’ + x8 + x9’x7 + x8 + x10’Scores:4: x83: x1,x72: x31: x2,x4,x9,x10,x11,x12New clause addedx1 + x4x1 + x3’ + x8’x1 + x8 + x12x2 + x11x7’ + x3’ + x9x7’ + x8 + x9’x7 + x8 + x10’x7 + x10 + x12’Scores:4: x8,x73: x12: x3,x10,x121: x2,x4,x9,x11watch what happens to x8, x7 and x130VSIDS Example (2/2)Counters divided by 2x1 + x4x1 + x3’ + x8’x1 + x8 + x12x2 + x11x7’ + x3’ + x9x7’ + x8 + x9’x7 + x8 + x10’x7 + x10 + x12’Scores:2: x8,x71: x3,x10,x12,x10:
View Full Document