This is an old revision of the document!
Advanced SAT Solving Techniques
DPLL Imperatively
Simulate recursion with stack
- for each variable 'flipped' bit indicates if we have analyzed its previous value
status = preprocess(); if (status != UNKNOWN) return status; while (true) { decide_next_branch(); while (true) { status = deduce(); if (status == CONFLICT) { blevel = analyze_conflict(); if (blevel == 0) return UNSATISFIABLE; else backtrack(blevel); } else if (status == SATISFIABLE) return SATISFIABLE else break; } }
Deduction Algorithm - deduce()
Main: Boolean Constraint Propagation (BCP), also called unit propagation.
Problem with deleting clauses and literals:
Need efficient data structures:
- head/tail list
- two-literal watching
Other mechanisms less important: e.g. propagating equivalences.
Note: as a result of these data structures, we always work with original clauses (we just record how many literals are false)
Conflict Analysis and Lemma Learning - analyze_conflict()
Invoked when conflict detected.
- analyzes the reason for unsatisfiability
- remembers the reason for unsatisfiability (lemma)
- indicates where to backtrack to
Chronological Backtracking
Corresponds to recursive procedure: jump to last non-flipped variable.
Non-Chronological Backtracking (Backjumping)
analyze_conflict() { cl = find_conflicting_clause(); while (!stop_criterion_met(c1)) { var = var_of_lit(choose_literal(c1)); c1 = resolve(c1, antecedant(var), var); } add_clause_to_database(c1); return clause_asserting_level(c1); }
What is antecedant(var):
- var is variable whose value was set by deduction
- deduction rule was that some original clause C became unit clause because all literals exept literal containing var were false
- then antecedant(var) is C
Branching Heuristics - decide_next_branch()
Score variables: if a variable caused a conflict, increase its score.
- decrease existing scores gradually over time
Storing Clauses
Use big array.
Preprocessing, Restarts
Preprocessing: apply deduction (and perhaps more) before the start.
Restart: if no progress for a while, start over (keeping some lemmas), will most likely do different branching.