Atomic Diagram Normal Form

We next consider a syntactic normal form that helps us understand the decidability of the combination problem.

Flat Form

By introducing fresh variables, each conjunction of literals can be represented as an equisatisfiable conjunction of only “flat literals”, which are flat atomic formulas or their negation, where flat atomic formula is

$\begin{equation*} R(y_1,\ldots,y_n) \end{equation*}$

$\begin{equation*} x = y \end{equation*}$

$\begin{equation*} x = f(y_1,\ldots,y_n) \end{equation*}$

We call this “flat form” of the conjunction of literals. (We can also eliminate $x \neq f(y_1,\ldots,y_n)$ if needed.)

Rewrite rule that describes this transformation:

$\begin{equation*} C[t] \ \ \leadsto \ \ (x=t) \land C[x] \end{equation*}$

Example: Represent $f(x)+y < z$ as

$\begin{equation*} x_1 = f(x) \land s_1 = x_1 + y \land s_1 < z \end{equation*}$

Finiteness of Flat Literals with Fixed Variables

Consider a formula in flat form. Let language ${\cal L}$ contain only the symbols occurring in the formula. For the fixed set of variables occurring there is a finite number of flat atomic formulas.

Assume $K$ variables. ( $K = |FV(C)|$ )

Number of $R(y_1,\ldots,y_n)$ is: $K^n$

Number of $x=y$ atomic formulas is: $K^2$

Number of $x=f(y_1,\ldots,y_n)$ literals is: $K^{n+1}$

Note: if we did not have only flat literals, we could have infinitely many atomic formulas, because of arbitrarily large terms.

Example: When we have relation symbols $<$ and no function symbols, and consider 3 variables $x$ , $y$ , $z$ , possible atomic formulas are:

$x=x$ , $y=y$ , $z=z$ , $x=y$ , $y=x$ , $x=z$ , $z=x$ , $y=z$ , $z=y$
$x<x$ , $y<y$ , $z<z$ , $x<y$ , $y<x$ , $x<z$ , $z<x$ , $y<z$ , $z<y$

and there are 3^2+3^2=18 atomic formulas.

Atomic Diagram Normal Form

For each flat literal $L$ , $C$ is equivalent to $(C \land L) \lor (C \land \lnot L)$ and $\lnot L$ is a conjunction of flat literals.

Let variables of $C$ be $V_C$ .

Atomic diagram conjunction is a flat form such that for each flat atomic formula $A$ in variables $V_C$ either $A$ or $\lnot A$ appears.

Each conjunction of flat literals is equivalent to a disjunction of atomic diagram conjunctions. Such form can be very large and we do not need to go that far, but we can when we need to.

Note: if we simply guess all possible conjunctions of literals and negations, some of them will be unsatisfiable in the theory. Those are useless and we should eliminate them. For example, if we consider equality literals, then

$\begin{equation*} x \neq z \land y = z \land x = y \end{equation*}$

is unsatisfiable. Only those conjunctions of equality literals can be satisfiable that correspond to an equivalence relations on variables. Such conjunction of literals that corresponds to an equivalence relation is called arrangement in the context of combination techniques.

$C$ can be rewritten as such (notating $L_i$ the $i^{th}$ flat literal and $A_{n+i}^{\alpha^{n+i}}$ the truth value of the $i^{th}$ variable):

$C = \bigvee_{\alpha_{n+1}, ..., \alpha_m}L_1\land ...\land L_n\land A_{n+1}^{\alpha^{n+1}}\land ...\land A_m^{\alpha^m}$

Which in turn can be rewritten as (notating $Ar_i$ the $i^{th}$ possible arrangement):

$C \leadsto \bigvee_i C \land Ar_i$

Example: In last example, there are $2^{18}$ disjuncts to consider. If relations have special properties many cases are unsatisfiable and can be ignored. Nevertheless, the number of satisfiable atomic diagram formulas is typically exponential.

For example, if we have only equality symbol, each partition of the set of variables gives one satisfiable formula (asserting that elements in same partition are equal, in different partitions disequal). Partition $\{\{x,y\},\{z\}\}$ gives formula

$\begin{equation*} x = y \land x \neq z \end{equation*}$

or, if we include all atomic formulas:

$\begin{equation*} x = y \land y = x \land x \neq z \land z \neq x \land y \neq z \land z \neq y \land x = x \land y = y \land z=z \end{equation*}$

The number of partitions is given by Bell numbers.