LARA

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.

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.

Other Techniques