Conflict-Driven Clause Learning IA085: Satisfiability and Automated Reasoning Martin Jonáš Fl MUNI, Spring 2024 Last Time • propositional resolution • Davis-Putnam algorithm • Davis-Putnam-Logemann-Loveland algorithm (dpll) • practical implementation of dpll 1/32 dpll: Reminder 1 def DPLL(formula 4>): 2 InitializeDatastructures() 3 4 if UnitPropagationO == CONFLICT: 5 return UNSAT 6 7 while not all variables are assigned: 8 (var, polarity) «— PickUnassignedVariable() 9 10 Decide(var, polarity) 11 while UnitPropagationO == CONFLICT: 12 if decisions == [ ]: 13 return UNSAT 14 Backtrack^) 15 16 return SAT 2/32 dpll: Not so clever

/] = false 7/32 Implication graph: example

> clause {^C, ^D} /\ • {C, E, D} clause {-.C, -.£, -.0} C7 ^ d@3 x 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, 8,0} clause {^A, -8,^0} • {C, D} ->> clause {^C, ^D} • {C, E, D} clause {-.C, -.£, ^D} 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 Unique implication points • D (last UIP) • E (first UIP) 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) {^C^D^E} 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} 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) {^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) {^D,E} {zCL^DlZE} {-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 0 = C 14/32 Computing the conflict clause 1 def ComputeConflictClause(formula ): 2 res «— current conflict clause 3 if res contains only one literal from the latest decision level: 4 return res 5 6 for I in reverse(trail): 7 if -iI in C: 8 res «— Resolve( var(l), res, reason[l]) 9 if res contains only one literal from the latest decision level: 10 return res For efficient implementation see https://github.com/niklasso/minisat/ blob/master/minisat/core/Solver .cc#L296 (until line 336) 15/32 Non-Chronological Backtracking Backjumping dpll • always changes the value of the last decision variable • chronological backtracking cdcl 1. learn the conflict clause 2. backtrack until the learnt clause becomes unit 3. 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 ): 2 InitializeDatastructures() 3 4 if UnitPropagation() == CONFLICT: 5 return UNSAT 6 7 while not all variables are assigned: 8 (var, polarity) «— PickUnassignedVariable() 9 Decide(var, polarity) 10 11 while UnitPropagation() == CONFLICT: 12 (learnt, backtrackLevel) «— ConflictAnalysis() 13 if (backtrackLevel == 0): 14 return UNSAT 15 else 16 Learn(learnt) 17 Backtrack(backtrackLevel, learnt) 18 19 return SAT 18/32 CDCL ConflictAnalysis() • analyzes the current conflict • returns the learnt clause and the highest decision level that should be backtracked (i.e., the level whose removal makes the learnt clause unit) Learn(clause) • adds clause to the current formula • initializes the watches etc. Backtrack(backtrackLevel, clause) • reverts all decisions up to the given level backtrackLevel (including) • unit propagates the clause clause 19/32 Literal Decision Heuristics Literal Decision Heuristics Selecting good decision literals is crucial for performance (an idealistic perfect oracle would assign a model on the first try). Multiple cheap literal selection heuristics (aka branching heuristics) exist Can be based on • current state of the solver (and the formula) • previous computation Literal selection often decomposed 1. select the decision variable 2. select its phase/polarity 20/32 dpll decision heuristics Dynamic Largest Individual Sum (dlis) • choose a literal that occurs most often in unsatisfied clauses • idea: satisfy as many remaining clauses as possible Jeroslow-Wang • maximize score(l) = J]ce,/ec2_'C' • idea: pick the literal with highest contribution to satisfying ip moms • pick the literal that occurs most often in inimal ize clauses • idea: try to satisfy the highest number of short clauses 21/32 vsids Idea • variables that occurred in recent conflicts are currently important Variable State Independent Decaying Sum (vsids, zChaff 2001) • maintain score for each variable • after each conflict increase score of each variable that occurred during conflict analysis by constant k • after each 256 conflicts, divide all scores by 2 and sort the variables by score • always choose the first unassigned variable 22/32 evsids Idea • decrease the scores of older variables more smoothly, not in chunks of 256 conflicts Exponential vsids (evsids, MiniSAT 2003) • keep the variable sorted all the time (binary heap) • after each conflict - increase score of each variable that occurred during conflict analysis by constant 1 and - divide scores of all other variables by a constant (e.g., 1.01) • always choose the first unassigned variable 23/32 evsids Idea • decrease the scores of older variables more smoothly, not in chunks of 256 conflicts Exponential vsids (evsids, MiniSAT 2003) • keep the variable sorted all the time (binary heap) • after each conflict - increase score of each variable that occurred during conflict analysis by constant 1 and - divide scores of all other variables by a constant (e.g., 1.01) • always choose the first unassigned variable • often also referred to as vsids © 23/32 evsids Idea • decrease the scores of older variables more smoothly, not in chunks of 256 conflicts Exponential vsids (evsids, MiniSAT 2003) • keep the variable sorted all the time (binary heap) • after each conflict - increase score of each variable that occurred during conflict analysis by constant 1 and - divide scores of all other variables by a constant (e.g., 1.01) • always choose the first unassigned variable • often also referred to as vsids © 23/32 Implementing evsids Decreasing scores of ail variables often is expensive. Increase the constant that is added to the score instead. • after each conflict, increase the variables that occurred during conflict analysis by constant k and set k to 1.01 • k 24/32 Implementing evsids Decreasing scores of ail variables often is expensive. Increase the constant that is added to the score instead. • after each conflict, increase the variables that occurred during conflict analysis by constant k and set k to 1.01 • k The constant k can become too large (1.014459 > 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 ): 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