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

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

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

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

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:

• head/tail list
• two-literal watching

Other mechanisms less important: e.g. propagating equivalences.

Invoked when conflict detected.

• analyzes the reason for unsatisfiability
• remembers the reason for unsatisfiability (lemma)
• indicates where to backtrack to

Corresponds to recursive procedure: jump to last non-flipped variable.

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

Use big array.

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.

• The Quest for Efficient Boolean Satisfiability Solvers