perry_notes

gistfile1.md

DPLL Algorithm

Input: A formula in CNF

Output: Either "satisfiable" or "unsatisfiable".

Performance: O(2ⁿ), Space: O(n)

---

Implication Graph

A DAG with nodes representing partial assignments, leaves representing full assignments. An edge from a to b implies ~a is an element of Antecedent(b).

---

• Major Components: There are four discernible components to the general DPLL algorithm.

  • BCP : Boolean Constraint Propagation

  • DECIDE : Assigning an unassigned boolean var.

  • ANALYZE-CONFLICT : Compute the level to backtrack to.

  • BACKTRACK : Do the actual backtracking.

---

BCP

• Input: A partial assignment

• Output: "Conflict" only if conflict encountered.

• Synopsis: Apply unit clause rule until either a conflict or all implications have been instantiated.

• Note that BCP is applied once initially before the algorithm's main loop because we need to enact unary clauses.

---

DECIDE

• Input: A partial assignment

• Output: A new assignment

• Synopsis: Uses a heuristic to decide a truth value for an unassigned variable.

---

ANALYZE-CONFLICT

• Input: A conflict

• Output: "Unsatisfiable" if conflict at dl = 0. Otherwise, a new decision level to backtrack to along with a new conflict clause.

• Synopsis: Traverse the graph backwards, starting at a conflict node, generates a conflict clause.

• Note: This generation of conflict clauses is the systems way of learning.

---

ANALYZE-CONFLICT

• Does it terminate?
  • Yes. Since we don't duplicate assignments by theorem 2.8 we are going to terminate eventually. It follows immediately that the algorithm as a whole terminates.

---

ANALYZE-CONFLICT

• Some necessary definitions:

  • Unique Implication Point(UIP)

    • A node(not the conflict node), that is on all paths from the decision node to the conflict node in a partial implication graph.

  • First UIP

    • The closest UIP to the conflict node:

---

ANALYZE-CONFLICT

Algorithm:

proc analyze_conflict: 
  if current_dl == 0: 
    return -1
  cl = current_conflict_clause
  while !stop_crit_met
    lit = last_assigned_lit(cl)
    var = var_of_lit(lit)
    ant = antecedent(lit)
    cl = resolve(cl, ante, var)
  add_clause(cl)
  return level(cl)

Our point of interest is the resolve method.

---

ANALYZE-CONFLICT

• This is doing Binary Resolution.

---

BACKTRACK

• Input: An assignment level

• Output: Nothing

• Synopsis: Simply mutates the state of dl(our decision level, i.e. our depth in the tree)

---

Orchestrating the Components

-->  [ DECIDE ]  -------full-----------> SAT
     ^      |
     |      |
     |   part.   --------[ BACKTRACK ] <----------           
     |      |   |                                 | dl >= 0
no   |      |   |                                 |
conf.|      v   v                                 |
     ----- [ BCP ] --------conflict--------->[ANALYZE-CONFLICT]  
                                                    |
                                                    |
                                                    |
                                                    V
                                                  UNSAT    

---

Strategies for Assignment

Many techniques

• Jeroslaw-Wang
• DLIS
• VSIDS
• Berkmin

---

Jeroslaw-Wang

This strategy prioritizes literals which appear frequently in shorter clauses.

---

DLIS

• Stands for Dynamic Largest Individual Sum
• Assigns the literal which satisfies the most clauses.

---

VSIDS

• Stands for Variable State Individual Decaying Sum
• Similar to DLIS
• Different in that it counts already satisfied clauses to its sum total and all scores are divided by two.
  • The benefits of this are time complexity.

---

Berkmin

• A heuristic which uses a stack data structure to track literals most recently in conflict clauses.

---

Resolution Graph

A DAG composed of clauses, used for conflict resolution in ANALYZE-CONFLICT.