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

function-free formulas of the equality logic. Then the equality logic formula can
be transformed into a propositional one and a standard satisfiability checker
can be applied. Goel et al. [6] and Bryant et al. [3] reduced an equality formula
to a propositional one by adding transitivity constraints. In this approach it is
analyzed which transitivity properties may be relevant.
A different approach is called range allocation [9,10]. In this approach a
formula structure is analyzed to define a small domain for each variable. Then
a standard BDD-based tool is used to check satisfiability of the formula under
the domain.
Another approach is given in [7]. This approach is based on BDD compu-
tation, with some extra rules for dealing with transitivity. Unfortunately, the
unicity of the reduced BDDs is lost.
In this paper an approach based on the Davis-Putnam-Logemann-Loveland
procedure (DPLL) [5] is introduced.
The DPLL procedure was introduced in the early 60s as a proof procedure for
first-order logic. Nowadays, only its propositional logic core component is widely
used in ecient provers. The success was a motivation for developing a DPLL-
based procedure for the equality logic with uninterpreted functions. The main
idea of the DPLL method is to choose an atom from the formula and proceed
with two recursive calls: one obtained by assuming this atom and another by
assuming the negation of the atom. The procedure terminates with the answer
“unsatisfiable” if the empty clause is derived for all branches, and otherwise it
returns “satisfiable”.
ThefirsttechniquebasedontheDPLLmethod for EUF is introduced in [8].
The proposed DPLL procedure calls the congruence closure module for positive
equations.
In this paper the different procedure based on the DPLL method is proposed.
The main problem dealt with in the paper is: given an EUF formula, decide
whether it is satisfiable or not. Similar to the propositional logic every EUF
formula can be transformed into an EUF formula in conjunctive normal form
(CNF) such that the original formula is satisfiable if and only if the CNF is
satisfiable. Hence we may, and shall, concentrate on satisfiability of a formula in
conjunctive normal form. The idea of UIF-DPLL is to split a literal that occurs
in purely positive clauses of length more than one, and to apply the reduction
rules.
This paper is organized as follows. In Section 2 basic definitions are given. In
Section 3 the DPLL method is described. The UIF-DPLL calculus is presented in
Section 4. In Section 5 the UIF-DPLL procedure is introduced and a proof of its
soundness and completeness is given. The technique for reducing the size of a
formula and an optimized procedure are presented in Section 6. Some concluding
remarks are in Section 7.

2 Basic Definitions and Preliminaries

Each EUF formula can be straightforwardly converted into an equivalent CNF
in the same manner as in propositional logic. The well-known Tseitin transfor-