Section 7.2.2.2: Satisfiability

Exercise 281. [21] Construct a certificate of unsatisfiability that refutes (99), (100), (101).

Verified: no
Solve time: 5m42s

---

Solution

Let

$$ C_j=(\bar{x}_{jj}),\qquad 1\le j\le m, $$

$$ T_{ijk}=(\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 . $$

The certificate is obtained by deriving the clause

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

from the clauses (100) and (101), then resolving $D$ with the clauses (99).

For a set $S\subseteq{1,\ldots,m}$ define the clause

$$ P(S)= \left(\bigvee_{i\in S}x_{ii}\right) \vee \left(\bigvee_{\substack{i\in S\ k\notin S}}x_{ik}\right). $$

The clauses $P(S)$ form the intermediate clauses of the certificate. The desired clause $D$ is $P({1,\ldots,m})$.

For a singleton set $S={j}$, the clause $P(S)$ is exactly the row clause (101):

$$ P({j})= x_{jj}\vee\bigvee_{k\ne j}x_{jk}

R_j . $$

We now show how to combine two certificates. Suppose that $A$ and $B$ are disjoint nonempty sets and that $P(A)$ and $P(B)$ have already been derived. Write

$$ P(A)= \left(\bigvee_{i\in A}x_{ii}\right) \vee \left(\bigvee_{i\in A}x_{iv}\right) \vee E_A , $$

where $v\in B$ and $E_A$ contains the literals $x_{ik}$ with $k\notin A\cup{v}$.

For every $i\in A$, resolve the literal $x_{iv}$ in $P(A)$ with the clause

$$ T_{ivk}=(\bar{x}{iv}\vee\bar{x}{vk}\vee x_{ik}) $$

for each $k\notin A\cup{v}$. These resolutions replace an exit through $v$ by exits from $i$ to vertices outside $A\cup{v}$, together with the possible literal $x_{vv}$ coming from $P(B)$. Repeating the same resolution for all $i\in A$ and all possible exits from $v$ gives

$$ P(A\cup B)

\left(\bigvee_{i\in A\cup B}x_{ii}\right) \vee \left(\bigvee_{\substack{i\in A\cup B\ k\notin A\cup B}}x_{ik}\right). $$

Every step is a resolution using one clause already derived and one clause of type (100). Hence this is a valid certificate derivation.

Applying this construction successively to

$$ {1},{2},\ldots,{m} $$

derives

$$ P({1,\ldots,m})

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

because the second disjunction in the definition of $P(S)$ is empty when $S={1,\ldots,m}$.

The remaining part of the certificate resolves this clause with the diagonal 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 the same manner gives

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

and the final resolution with

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

produces

$$ \epsilon . $$

Thus the certificate consists of the derivation of the diagonal clause $D$ from (100), (101), followed by the $m$ resolutions with the clauses (99). The final derived clause is the empty clause, so clauses (99), (100), and (101) are unsatisfiable.

This completes the proof.

∎