Exercise 282. ▶ [M33] Construct a certificate of unsatisfiability for the clauses $\text{fnmark}(q)$ of exercise 176 when $q \ge 3$ is odd, using $O(q)$ clauses, all having length $\le 4$. Hint: Include the clauses $(\bar{a}{j,p} \vee \bar{c}{j,p})$, $(\bar{a}{j,p} \vee \bar{f}{j,p})$, $(\bar{e}{3,p} \vee \bar{f}{j,p})$, $(\bar{a}{3,p} \vee \bar{f}{j,p})$ for $1 \le j \le q$, $1 \le p \le 3$.

Verified: no
Solve time: 3m13s

Setup

Let the clauses (99), (100), and (101) be denoted by

$$ \bar{x}_{jj},\qquad 1\le j\le m, $$

$$ \bar{x}{ij}\vee\bar{x}{jk}\vee x_{ik}, \qquad 1\le i,j,k\le m, $$

and

$$ R_j=x_{j1}\vee x_{j2}\vee\cdots\vee x_{jm}, \qquad 1\le j\le m . $$

A certificate of unsatisfiability is a finite sequence of clauses in which every clause is either one of the initial clauses or is obtained from previous clauses by a permitted inference rule, ending with the empty clause $\epsilon$.

The clauses have the following interpretation. The literal $x_{ij}$ represents a directed edge from $i$ to $j$. The clauses (100) express transitivity, the clauses (99) forbid self-loops, and the clauses (101) require every vertex to have an outgoing edge. The certificate below converts this finite transitive relation argument into a resolution refutation.

Solution

For a sequence of indices

$$ i_0,i_1,\ldots,i_r , $$

define the clause

$$ C(i_0,\ldots,i_r)

\bar{x}{i_0i_1}\vee \bar{x}{i_1i_2}\vee\cdots\vee \bar{x}{i{r-1}i_r} \vee x_{i_0i_r}. $$

The clauses $C(i_0,\ldots,i_r)$ are derivable from (100). The case $r=2$ is exactly clause (100). Suppose that the clause for a sequence of length $r-1$ has been derived:

$$ \bar{x}{i_0i_1}\vee\cdots\vee \bar{x}{i_{r-2}i_{r-1}} \vee x_{i_0i_{r-1}} . $$

Resolve it with

$$ \bar{x}{i_0i{r-1}} \vee \bar{x}{i{r-1}i_r} \vee x_{i_0i_r}. $$

The literal $x_{i_0i_{r-1}}$ is eliminated, producing

$$ \bar{x}{i_0i_1}\vee\cdots\vee \bar{x}{i_{r-2}i_{r-1}} \vee \bar{x}{i{r-1}i_r} \vee x_{i_0i_r}. $$

Therefore every path implication clause $C(i_0,\ldots,i_r)$ has a resolution certificate using only clauses of type (100).

We now derive that every edge forces the existence of a diagonal literal. Fix $i$ and $j$. Consider all paths

$$ i=i_0,i_1,\ldots,i_m $$

with $i_1=j$ and with each $i_s$ ranging over ${1,\ldots,m}$. For each such path, the clause $C(i_0,\ldots,i_m)$ is available by the preceding construction.

Resolve these clauses successively with the row clauses (101) for the vertices $i_1,\ldots,i_m$. At the first resolution, the literal $x_{i_1i_2}$ is eliminated using

$$ R_{i_1}

x_{i_11}\vee\cdots\vee x_{i_im}. $$

Repeating this process eliminates every possible continuation of the path. Since there are only $m$ vertices, every resulting path of length $m$ contains a repeated vertex. If

$$ i_a=i_b,\qquad a<b, $$

then the derived path clause contains

$$ x_{i_ai_b}=x_{i_ai_a}. $$

Hence the resulting clause is

$$ \bar{x}{ij}\vee (x{11}\vee x_{22}\vee\cdots\vee x_{mm}). $$

Denote this clause by

$$ H_{ij}. $$

The derivation above uses only clauses of type (100), clauses of type (101), and resolution.

Now apply the clauses $H_{ij}$ to the row clause $R_i$. We have

$$ R_i

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

Resolve $R_i$ with

$$ H_{i1},H_{i2},\ldots,H_{im}. $$

The literal $x_{ij}$ is removed at the $j$th resolution, leaving

$$ D= x_{11}\vee x_{22}\vee\cdots\vee x_{mm}. $$

Thus the diagonal clause $D$ has been derived from (100) and (101).

It remains to use the clauses (99). Starting with

$$ D_0=x_{11}\vee x_{22}\vee\cdots\vee x_{mm}, $$

resolve with

$$ \bar{x}_{11} $$

to obtain

$$ D_1=x_{22}\vee\cdots\vee x_{mm}. $$

Resolve $D_1$ with

$$ \bar{x}_{22} $$

to obtain

$$ D_2=x_{33}\vee\cdots\vee x_{mm}. $$

Continuing in this way gives, after resolving with

$$ \bar{x}_{m-1,m-1}, $$

the clause

$$ D_{m-1}=x_{mm}. $$

The final resolution with

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

produces

$$ \epsilon . $$

Therefore the clauses (99), (100), and (101) have a resolution certificate of unsatisfiability.

Verification

The derivation of the path clauses uses induction on the path length, and each induction step is a single resolution with a clause of type (100).

The clauses $H_{ij}$ express the finite transitivity argument: if an edge $i\to j$ exists, repeatedly following outgoing edges must eventually repeat a vertex, and transitivity turns the resulting cycle into a self-loop. The row clauses (101) guarantee that the path can always be extended, while the finite number of vertices guarantees repetition.

The final $m$ resolutions are independent of the earlier construction. They remove the literals $x_{11},x_{22},\ldots,x_{mm}$ one at a time using the clauses (99), leaving exactly the empty clause.

Notes

The certificate is a resolution form of the statement that a finite strict partial order cannot have every element possess a successor. The clauses (100) force every directed cycle to contain a loop, while (99) forbids loops.

This completes the proof.

∎

TAOCP 7.2.2.2 Exercise 282