Deciding Quantifier-Free First-Order Logic Formulas

Given a FOL formula with equality and without quantifiers, we wish to check whether it is satisfiable (does there exist an interpretation that makes this formula true).

We do not restrict ourselves to any particular class of structures, we look at all possible structures.

Example: are the following formulas satisfiable. If yes, give a model, if no give, proof that no model exists.

formula1: $a=f(a) \land a \neq b$

formula2:

$\begin{equation*} (f(a)=b \lor (f(f(f(a))) = a \land f(a) = f(b))) \land f(f(f(f(a)) \neq b \land b=f(b) \end{equation*}$

formula 3: $a = b \land P(a) \land \lnot P(b)$

Suggest a general algorithm to check satisfiability:

for conjunctions of literals $t_1 = t_2$ and $t_1 \neq t_2$
for arbitrary quantifier-free formulas in FOL with equality

Together with SAT solving engine, such algorithms are one of the main components of modern SMT provers.

Observation 1: We can represent predicate $P(t_1,\ldots,t_n)$ as equality $f_P(t_1,\ldots,t_n)=\mbox{true}$ , so it suffices to work with function symbols. The example $a = b \land P(a) \land \lnot P(b)$ becomes

$\begin{equation*} a=b \land P(a)=true \land \lnot (P(b)=true) \end{equation*}$

where true is a particular constant in the theory (so, no need to restrict oneself to a two-valued domain).

Observation 2: When checking satisfiability of quantifier-free formulas, we can replace all variables with constants. The question we ask in both cases is the same: are there values and functions such that the given quantifier-free formula evaluates to true.