Skip to content

Some Notions

A clause is satisfied if one or more of its literal are satisfied.

A clause is conflicting if all literals are assigned but not satisfied.

A clause is unit if only one literals are unassigned.

In all other cases, the clause is unresolved.

For a unit clause \(C\) with unassigned literal \(\ell\), we say that \(\ell\) is implied by \(C\) and \(C\) is the antecedent clause of \(\ell\): \(C=\text{Antecedent}(\ell)\)

Boolean Constraint Propagation (BCP): given a unit clause with unassigned \(\ell\):

  1. Remove all other clauses containing \(\ell\).
  2. If a clause contains \(\neg\ell\), remove this literal.

Trails and Implication Graph

Given a formula.

First, we make a decision to set the Boolean value of one literal.

With BCP, we find unit clause and set the Boolean value of related literals.

Trail: an annotated sequence of literals, showing that the process of BCP. (We can also derive an equivalent graph)

If no unit clause found, we need to make another decision and propagate.

The implication graph can be built automatically from a trial:

  • The vertices are the literals that appear in the trail.
  • There is an edge \(\neg\ell_i,\ell\) for each literal \(\ell_i\) that is in a clause \(\ell^C,C=(\ell_1\lor\ell_2\lor\cdots\lor\ell_k\lor\ell)\), i.e., there is an edge between \(\ell\) and all the negated literals in \(\text{Antecedent}(\ell)\).
  • If there is a conflict, there is an edge to false from all the literals of a conflicting clause.
  • The entry points of the implication graph are the decisions.

We can build the implication graph: make a decision, do BCP and populate the graph, repeat until conflict or all variables are assigned and there is no conflict.

One possibility: in case of conflict, backtrack and take the opposite decision. DPLL algorithm works in this way.

Conflict Cuts

A conflict cut of the implication graph is a partition of vertices in two sets \(A\) and \(B\) s.t.:

  • All the decision vertices are in \(A\)
  • The conflict vertex False is in \(B\).

There can be multiple conflict cuts on an implication graph.

Instead of backtracking to the last decision, we can do learn something from cuts.

Reason set \(R=\{\ell\in A|\ell'\in B\text{ s.t.}(\ell,\ell')\text{ is an edge}\}\)

Learned clause: \(\bigvee_{\ell_i\in R}\neg\ell_i\).

We add the learned clause to the set of clauses.

Unique Implication Point

A UIP is a vertex \(\ell\) in the implication graph s.t. all the paths from the last decision vertex to the conflict vertex go through \(\ell\).

If a vertex \(\ell\) is UIP, a corresponding UIP cut is a partition \((A,B)\) s.t. \(B\) contains all and only the successors of \(\ell\) from which there is a path to False (and \(A\) contains the rest).

First UIP Cut

The First UIP cut is the UIP cut with the largest set \(A\).

❓How to choose the cut? Choose the first UIP cut.

Non-chronological Back-jumping

Suppose we have learned a clause \(C\) following the first UIP cut:

  • Let \(m\) be the second largest decision level of literals in \(C\).
  • Remove all literals with decision level greater than \(m\) from the trail.

Conflict-Driven Clause Learning (CDCL): repeat the process (propagate, decide, back-jump)

  • For SAT formulae, CDCL will terminate and find the assignment.
  • For UNSAT formulae, CDCL will produce conflicting unary clauses.

Heuristics

How to select variables?

  1. Given a formula \(B\), select the literal with the highest value of \(J(\ell)=\sum_{w\in B,\ell\in w}2^{-|w|}\) where \(w\) is a clause.
  2. Dynamic Largest Individual Sum (DLIS): At each decision level, choose the unassigned literal that satisfies the largest number of currently unsatisfied clauses.
  3. Variable State Independent Decaying Sum (VSIDS): give higher scores to variables involved in recent conflicts.