A Decision Procedure for Equality Logic with Uninterpreted Functions - Artificial Intelligence and Symbolic Computation - page 70

3 The DPLL Procedure

The DPLL procedure is a decision procedure for CNF formulae in propositional
logic, and it is the basis of some of the most successful propositional satisfiability
solvers to date. This is the fastest known algorithm for satisfiability testing that
is not just sound, but also complete.
The basic DPLL procedure recursively implements the three rules: unit prop-
agation, pure literal elimination and recursive splitting.

• Unit propagation : Given a unit clause , remove all clauses that contain the

literal l , including the clause itself and delete all occurrences of the literal
¬l from all other clauses. Moreover, the literal l is assigned to true .

{l}

• Pure literals elimination : A pure literal is a literal that appears only in pos-

itive or only in negative form. Eliminate all clauses containing pure literals.
Moreover, each pure literal is assigned to true .

• Splitting : Choose some literal l ∈ Lit ( φ ). Now φ is unsatisfiable iff both

φ ∪{{l}} are unsatisfiable. Selecting a literal for splitting is

nondeterministic, so various heuristics can be employed.

and φ ∪ {{¬l}}

The algorithm starts with a set of clauses and simplifies the set of clauses
simultaneously. The stopping cases are:

• An empty set of clauses is satisfiable-in this case, the entire algorithm ter-

minates with “satisfiable”.

• A set containing an empty clause is not satisfiable-in this case, the algorithm

backtracks and tries a different value for an instantiated variable.

The DPLL procedure returns a satisfying assignment, if one exists. It can be
extended to return all satisfying assignments.
We have chosen the DPLL procedure to develop our procedure for the fol-
lowing reasons.

• DPLL is a simple and an ecient algorithm.

• Many current state-of-the-art solvers are based on DPLL.

• It can be extended to compute an interpretation.

4The UIF-DPLL Calculus

UIF-DPLL can be used to decide the satisfiability of equality logic formulas with
uninterpreted functions in conjunctive normal form. The main operations of the
method are unit propagation I , unit propagation II , tautology atom removing ,
and splitting (recursive reduction to smaller problems). If the empty clause for
all branches is derived then the procedure returns “unsatisfiable”. Otherwise it
returns “satisfiable”.
The rules of the UIF-DPLL calculus are depicted in Figure 1.