LARA

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:

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:

  • false at current decision level
  • only one literal has current decision level (others were assigned before)

If c1 is not asserting clause yet, we resolve it with antecedants of variables, following backwards deduction steps.

In other words: we remove variables at current decision level until only one at the current is left.

The clause forces a different value of a decision variable at a previous level.

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.

Some Relevant Papers

Other Techniques