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;
  }
}

Branching Heuristics - decide_next_branch()

Decision level: each variable whose value is chosed increase decision level.

Score variables: if a variable participates in deriving lemmas triggered by a conflict, increase its score.

decrease existing scores gradually over time

Deduction Algorithm - deduce()

Main: Boolean Constraint Propagation (BCP), also called unit propagation.

Deduced variables have same decision level as the last decision variable.

Data Structures

Problem with deleting clauses and literals: backtracking is expensive.

Instead: maintain truth value of literals in current assignment.

We always work with original clauses (we just record how many literals are false)

Need efficient data structures:

counters: simple, need many updates
head/tail list
two-literal watching: each var has list of unassigned literals, do search to see if there are other literals to watch in clause
- invariant: each non-conflicting clause has at least one watched literal, but not all literals need to be watched
- no need to do anything on backtrack

Mechanisms other than unit propagation are less important: e.g. propagating equivalences.

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 (!is_asserting_clause(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

asserting clause: