Section 7.2.2.2: Satisfiability

Exercise 231. [M30] (Sam Buss.) Refute the clauses of exercise 229 with a resolution chain of length $O(m^3)$. Hint: Derive the clauses $G_{ij} = (\bar{x}{i1} \vee \bar{x}{i2j}) \vee \cdots \vee \bar{x}_{im})$ for $1 \le i \le j \le m$.

Verified: no
Solve time: 5m01s

---

Solution

The previous argument used the wrong intermediate clauses. The clauses required by Buss's construction are the suffix clauses

$$ G_{ij}=(x_{ij}\vee x_{i,j+1}\vee\cdots\vee x_{im}), \qquad 1\leq i\leq j\leq m . $$

These clauses express that element $i$ has a successor among the elements $j,j+1,\ldots,m$. We derive them using the clauses of exercise 229, namely the positive clauses (99), the restricted transitivity clauses (100'), and the anti-reflexivity clauses (101).

For fixed $i$, begin with the clause (99):

$$ x_{i1}\vee x_{i2}\vee\cdots\vee x_{im}. $$

This is exactly $G_{i1}$. We now show how to derive

$$ G_{i,j+1}

(x_{i,j+1}\vee x_{i,j+2}\vee\cdots\vee x_{im}) $$

from $G_{ij}$.

Assume that

$$ G_{ij}

(x_{ij}\vee x_{i,j+1}\vee\cdots\vee x_{im}) $$

has already been derived. We need to eliminate the literal $x_{ij}$.

The already derived clauses for row $j$ give

$$ G_{j,j+1}

(x_{j,j+1}\vee x_{j,j+2}\vee\cdots\vee x_{jm}). $$

For every $k$ with $j<k\leq m$, the restricted transitivity clauses (100') contain

$$ (\bar{x}{ij}\vee\bar{x}{jk}\vee x_{ik}). $$

Resolve this clause with $G_{j,j+1}$ on $x_{jk}$. Doing this successively for

$$ k=j+1,j+2,\ldots,m $$

eliminates all the literals of $G_{j,j+1}$ and gives

$$ (\bar{x}{ij}\vee x{i,j+1}\vee x_{i,j+2}\vee\cdots\vee x_{im}). $$

Now resolve this clause with

$$ G_{ij}

(x_{ij}\vee x_{i,j+1}\vee\cdots\vee x_{im}) $$

on $x_{ij}$. The result is

$$ (x_{i,j+1}\vee x_{i,j+2}\vee\cdots\vee x_{im}), $$

which is precisely

$$ G_{i,j+1}. $$

Thus, for each fixed $i$, the sequence

$$ G_{i1},G_{i2},\ldots,G_{im} $$

is derivable.

It remains to obtain a contradiction. Taking $i=m$, the last clause in this sequence is

$$ G_{mm}=x_{mm}. $$

The anti-reflexivity clause (101) gives

$$ \bar{x}_{mm}. $$

Resolving these two clauses produces the empty clause:

$$ \frac{x_{mm}\qquad \bar{x}_{mm}}{\epsilon}. $$

Hence the clauses of exercise 229 are refuted.

It remains to count the resolution steps. There are

$$ \sum_{i=1}^{m}(m-i)

\frac{m(m-1)}2 $$

extensions needed to derive all clauses $G_{ij}$ from their predecessors. Each extension from $G_{ij}$ to $G_{i,j+1}$ requires at most $m$ resolutions, because the literals

$$ x_{j,j+1},x_{j,j+2},\ldots,x_{jm} $$

must be eliminated once. Therefore the total number of resolution steps used in constructing the $G_{ij}$ clauses is at most

$$ m\frac{m(m-1)}2=O(m^3). $$

The final contradiction requires one additional resolution step, so the whole refutation has length

$$ O(m^3). $$

$$ \boxed{\text{The clauses of exercise 229 have a resolution refutation of length }O(m^3).} $$