= {{-A,^B,C}i, {B,-A,C}2, {A,^B,C}3, {-C,A^}4, {-C,A-£}s, {-C,-A^}e, {-C,-A-^}7} 5 0 AB C ABC ABCD E trail = [A, B, C, D, E] decisions = [0,1,3] The decisions partition trail into decision levels • decision literal followed by unit propagations • level 1: [A], level 2: [B,C], level 3: [D,E] 5/32 Antecedents antecendent (reason) clause = clause that caused the unit propagation 6/32 Antecedents antecendent (reason) clause = clause that caused the unit propagation
/] = false 7/32 Implication graph: example
clause {-.A, -.£>} • {C,D} -> clause {-C,-L>} • {C,E,D} -> clause {^C,^E,^D} 10/32 Separating Cuts Separating cut • cut = partition of vertices into two disjoint sets • separating cut = decision vertices in one set, the conflict vertex is in the other • each separating cut corresponds to a conflict set From left to right correspond to conflict sets • {A, B, D} -> clause {-.A, -■£>} • {C,D} -> clause {-C,-L>} • {C,E,D} -> clause {-.C,-■£>} Which is the best one? 10/32 Properties of learnt clauses The learnt conflict clauses should be • small: prune the search space as much as possible • asserting = contain only one literal at the current decision level 11 I 32 Unique Implication Point (UIP) • a vertex V ^ k such that ail paths from the current decision vertex to k go through V • always exists (why?) • first UIP = closest to the conflict 12/32 Computing the conflict clause 1. start with the conflicting clause 2. resolve with the reason clauses until the clause contains only one literal at the current decision level (asserting first UIP) 13/32 Computing the conflict clause 1. start with the conflicting clause 2. resolve with the reason clauses until the clause contains only one literal at the current decision level (asserting first UIP) 13/32 Computing the conflict clause 1. start with the conflicting clause 2. resolve with the reason clauses until the clause contains only one literal at the current decision level (asserting first UIP) {^C^D,E} {^C^D^E} {-C, ^D} 13/32 Computing the conflict clause 1. start with the conflicting clause 2. resolve with the reason clauses until the clause contains only one literal at the current decision level (asserting first UIP) {^C^D,E} {^C^D^E} {-C, ^D} 13/32 Computing the conflict clause It is always safe to add the computed conflict clause C to the formula. Why? 14/32 Computing the conflict clause It is always safe to add the computed conflict clause C to the formula. Why? It was derived by resolution, so = C 14/32 Computing the conflict clause 1 def ComputeConflictClause(formula $): 2 result «— current conflict clause 3 if result contains only one literal from the latest decision level: 4 return result 5 6 for I in reverse(trail): 7 if -iI in result: 8 result «— Resolve( var(l), result, reason[l]) 9 if result contains only one literal from the latest decision level: 10 return result For efficient implementation see https://github.com/niklasso/minisat/ blob/master/minisat/core/Solver .cc#L296 (until line 336) 15/32 Non-Chronological Backtracking Backjurn ping dpll • always changes the value of the last decision variable • chronological backtracking cdcl 1. learn the conflict clause 2. remove last decision level 3. backtrack until the learnt clause is still unit 4. unit propagate its asserting unit literal cdcl can undo multiple decision levels and prune large parts of the search space -> non-chronological backtracking (or backjumping) 16/32 Complete cdcl: Example
}8, {-C}9 } A B A 0 AB C ABC D, ABCD E ABCD E trail decisions reason [C] reason [-*D] reason [E] [A, B, C, -A E] [0,1; 1 8 4 17/32 Complete cdcl: Example
}8, {-C}9 } A B A 0 AB C ABC D, ABCD E ABCD E trail decisions reason [C] reason [-*D] reason [E] [A, B, C, -A E] [0,1; 1 8 4 17/32 Complete cdcl: Example
}8, {-C}9 } A B A 0 AB C ABC D, ABCD E ABCD E C C trail = [-.C] decisions = | reason[^C] = 9 17/32 Complete cdcl: Example
}8, {-C}9 } A B A 0 C A C AB C CA ABC D, ABCD E ABCD E trail = [-.C, A] decisions = [1 reason[^C] = 9 17/32 Complete cdcl: Example
}8, {-C}9 } A B A 0 C A C AB C CA ABC B D, AB ABCD E ABCD E trail = [-.C, A, ^B decisions = [1 reason [-*B] = 1 reason[^C] = 9 17/32 Complete cdcl: Example
264 and 1.0171333 > 1.797 • 10308) • when k > 10100 divide all scores and k by 10100 24/32 Phase selection MlNlSAT • in most of the cases assign the variable to false • with a small probability pick a random phase Phase saving • choose the phase that the variable had assigned previously • idea: the phase was likely important, focus on it unless we have a reason for flipping it Modern sat solvers (CaDiCaL) • cycle between multiple modes • e.g., phase saving ->> set to opposite ->> set to zero ->> set to random 25/32 Restarts Restarts If the solver gets "stuck" in the region containing no solutions, a restart of the search can help. Restart • clear the current assignment • keep the learnt clauses and the variable scores and other heuristics 26/32 Restart strategies Usually, the solver is restarted after a certain number of conflicts. Geometric sequence • after 1,2,4,8,16,32,... conflicts (multiplied by a constant) Luby sequence • 1,1,2,1,1,2,4,1,1,2,4,8,1,1,2,4,8,16,. conflicts (multiplied by a constant) • used in modern sat solvers ... and many others. 27/32 Restarts with phase saving Restarts + phase saving • the restart does not escape the current search region • the variables are set to previous variables, but their order and dependencies are different • explore the same region, but via a different path 28/32 Complete CDCL-based SAT solver Complete CDCL-based SAT solver 1 def CDCL(formula 3>): 2 InitializeDatastructures() 3 4 if UnitPropagation() == CONFLICT: 5 return UNSAT 6 7 conflicts = 0; 8 while not all variables are assigned: 9 (var, polarity) PickUnassignedVariable() 10 Decide(var, polarity) 11 12 while UnitPropagation() == CONFLICT: 13 ++conflicts; 14 if ShouldRestart(conflicts): 15 RestartO 16 17 (learnt, backtrackLevel) ConflictAnalysis() 18 if (backjumpLevel == 0): 19 return UNSAT 20 else: 21 Learn(learnt) 22 Backtrack(backtrackLevel, learnt) 23 24 return SAT 29/32 Effect of individual techniques In 2011, Marques-Silva et. al evaluated effect of all mentioned features on the solver MiniSAT. Tested configurations • full MiniSAT (CDCL) • without clause learning (->CL) • without VSIDS (-VSIDS) • without 2-watched literal scheme (-2WL) • without restarts (-iRST) 30/32 Effect of individual techniques 1000 Instances 31/32 Next time Additional features of sat solvers • solving under assumptions • proof generation • unsatisfiable core generation • interpolation 32/32