
## 2 Preliminaries

We now review the abstract transition system framework proposed for the DPLL procedure by Nieuwenhuis et al. (2006), and introduce some necessary terminology concerning logic programs and the logic PC(ID). Abstract DPLL. Most state-of-the-art SAT solvers are based on variations of the DPLL
procedure (Davis et al. 1962). Nieuwenhuis et al. (2006) described DPLL by means of a transition system that can be viewed as an abstract representation of the underlying DPLL
computation. In this section we review the abstract DPLL in the form convenient for our purposes, following the presentation proposed by Lierler (2011).

For a set A of atoms, a record relative to A is an ordered set M of literals over A ,
some possibly annotated by ∆, which marks them as decision literals. A state relative to A
is either a distinguished state *FailState* or a record relative to A . For instance, the states relative to a singleton set {a} are

FailState, /0, a, ¬a, a
∆, ¬a ∆, a¬a, a ∆¬a,
a¬a
∆, a
∆, ¬aa, ¬a
∆ a, ¬aa∆, ¬a
∆ a
∆.
$$\begin{array}{l l l}{{a t e,}}&{{0,}}&{{a,}}&{{\neg a,}}\\ {{,}}&{{a^{\Delta}\neg a^{\Delta},}}&{{\neg a a,}}\end{array}$$
Frequently, we consider M as a set of literals, ignoring both the annotations and the order among its elements. If neither a literal l nor its dual, written l, occurs in M, then l is unassigned by M. We say that M is inconsistent if both an atom a and its negation ¬a occur in it. For instance, states b
∆¬b and ba¬b are inconsistent.

If C is a disjunction (conjunction) of literals then by C we understand the conjunction
(disjunction) of the duals of the literals occurring in C. In some situations, we will identify disjunctions and conjunctions of literals with the sets of these literals.

In this paper, a clause is a non-empty disjunction of literals and a CNF formula is a conjunction (alternatively, a set) of clauses. Each CNF formula F determines its DPLL
graph DPF. The set of nodes of DPF consists of the states relative to the set of atoms occurring in F. The edges of the graph DPF are specified by four transition rules:

| Unit Propagate:   | M =⇒ Ml        | if C∨l ∈ F and C ⊆ M    |
|-------------------|----------------|-------------------------|
| Decide:           | M =⇒ Ml∆       | if l is unassigned by M |
| Fail:             | M =⇒ FailState | if  M is inconsistent, and M contains no decision literals                         |
| Backtrack:        | Pl∆Q =⇒ Pl     | if  Pl∆Q is inconsistent, and Q contains no decision literals.                         |

A node (state) in the graph is terminal if no edge originates in it. The following proposition gathers key properties of the graph DPF.

Proposition 1 For any CNF formula F,
(a) graph DPF is finite and acyclic,
(b) any terminal state of DPF other than *FailState* is a model of F,
(c) *FailState* is reachable from /0 in DPF if and only if F is unsatisfiable.