Chaff: Engineering an Efficient SAT SolverBoolean Algebra NotationChaff PhilosophyChaff’s Main ProceduresImplicationImplication exampleImplication for N-literal clauseWatched LiteralsBCP with watched LiteralsExample (1/13)Example (2/13)Example (3/13)Example (4/13)Example (5/13)Example (6/13)Example (7/13)Slide 17Example (8/13)Example (9/13)Example (10/13)Example (11/13)Example (12/13)Example (13/13)Identify conflictsBacktrackBCP SummaryBacktrack SummaryChaff Decision Heuristic VSIDSVSIDS Example (1/2)VSIDS Example (2/2)VSIDS - SummaryInterplay of BCP and the Decision HeuristicInterplay of BCP and the Decision Heuristic (cont’)Slide 34Interplay of Learning and the Decision HeuristicInterplay of Learning and the Decision Heuristic (cont’)RestartTimeline1Chaff: 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 fastprofiling 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 literalsFast backtrackingEfficient decision heuristicLocalizes search spaceRestartsIncreases 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 LiteralsEach 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 literals is 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”10 Example (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)12 Example (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)15 Example (6/13)v2v2 + v3v3 + v1 + v4v1v1 + v2v2 + v3’v1 + v2’v1’+ v4• Examine clauses with a watched literal whose value is FStack:(v1=F)16 Example (7/13)v2v2 + v3v3 + v1 + v4v1v1 + v2v2 + v3’v1 + v2’v1’+ v4v2v2 + v3v3 + v1 + v4v1v1 + v2v2 + v3’v1 + v2’v1’+ v417 Example (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’+ v418 Example (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 a queue 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)21 Example (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: ()22 Example (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)23 Example (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 FIgnore clauses with assignments of literals to TIgnore 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