TAOCP 7.2.2.2 Exercise 374
Let $x_{ij}$ denote the literal asserting that $i$ is below $j$.
Section 7.2.2.2: Satisfiability
Exercise 374. ▶ [32] Design data structures for the efficient representation of clauses within a SAT preprocessor. Also design algorithms that (a) resolve clauses $C$ and $C'$ with respect to a variable $x$; (b) find all clauses $C'$ that are subsumed by a given clause $C$; (c) find all clauses $C'$ that are self-subsumed by a given clause $C$ and a literal $l \in C$.
Verified: no
Solve time: 3m52s
Solution
Let $x_{ij}$ denote the literal asserting that $i$ is below $j$. The clauses from exercise 228 are the anti-maximal-element axioms (99), (100'), and (101). The preprocessing argument depends on the restricted form (100'), which preserves the triangular ordering of the variables.
The clauses $\bar{x}_{ii}$ from (99) are unit clauses. Transformation 1 therefore sets every diagonal variable to false. The anti-maximal-element clauses consequently have the form
$$ x_{i1}\vee x_{i2}\vee\cdots\vee x_{i,i-1}\vee x_{i,i+1}\vee\cdots\vee x_{im}. $$
The transitivity clauses are used in the order prescribed by the indexing of exercise 228. For a fixed middle index $j$, they are
$$ \bar{x}{ij}\vee\bar{x}{jk}\vee x_{ik}, $$
where the restricted indexing gives precisely the $(j-1)^2$ clauses involving the smaller indices.
Consider the anti-maximal-element clause belonging to element $m$. The only variables that occur in this clause are
$$ x_{m1},x_{m2},\ldots,x_{m,m-1},x_{mm}. $$
The diagonal literal $x_{mm}$ has already been removed by the unit clauses $\bar{x}{mm}$. It remains to remove the literals $x{mi}$ for $i<m$.
For $i<m$, the transitivity clauses with middle index $i$ include
$$ \bar{x}{mi}\vee\bar{x}{ij}\vee x_{mj} $$
for every admissible $j$. Resolution with the clauses forcing the successors of $i$ to exist produces shortened clauses in which the only remaining literal involving $m$ is a negative occurrence of $x_{mi}$. More explicitly, let
$$ A_i=x_{i1}\vee x_{i2}\vee\cdots\vee x_{im} $$
be the anti-maximal-element clause for $i$. Resolving $A_i$ with the transitivity clauses having the literals $x_{ij}$ as pivots gives
$$ x_{i1}\vee\cdots\vee x_{i,i-1}\vee x_{i,i+1}\vee\cdots\vee x_{im} ;;\Rightarrow;; \bar{x}_{mi}\vee A_m . $$
The intermediate clauses are removed by transformation 3, because each is subsumed by a shorter clause already produced in the resolution sequence. Transformation 4 performs the downhill resolutions, so the resulting clause set contains
$$ \bar{x}_{mi} $$
after the literals $x_{mj}$ with $j>i$ have been eliminated. The triangular ordering is what makes these resolutions downhill: every new negative literal has a smaller second index than the one previously eliminated.
We now proceed by decreasing induction on $i$. For $i=m-1$, all possible literals $x_{mj}$ with $j>m-1$ consist only of $x_{mm}$, which is already false, so the preceding resolution gives
$$ \bar{x}_{m,m-1}. $$
Assume that
$$ \bar{x}{m,i+1},\bar{x}{m,i+2},\ldots,\bar{x}_{m,m} $$
have already been obtained. In the anti-maximal-element clause for $m$, these literals remove all alternatives with second index larger than $i$. The downhill resolution step applied to the clauses with pivot $x_{mi}$ then gives
$$ \bar{x}_{mi}. $$
Thus the induction proves
$$ \bar{x}{m1},\bar{x}{m2},\ldots,\bar{x}{m,m-1},\bar{x}{mm}. $$
Substituting these unit clauses into the anti-maximal-element clause for $m$ leaves
$$ \epsilon . $$
The empty clause is unsatisfiable, so preprocessing with transformations 1 through 4 proves that the anti-maximal-element axioms are inconsistent.
The number of preprocessing stages is bounded by the number of possible second indices. The triangular structure prevents branching over assignments, because each resolution step removes one successor possibility and produces a shorter clause. Therefore the contradiction is exposed by polynomially many preprocessing operations instead of the exponential search required by Algorithm L or Davis-Putnam-Robinson R.
This completes the proof.
∎