TAOCP 7.2.2.2 Exercise 230
Edit Let (F) denote the set of clauses from the previous exercise after removing the tautological cases (i=j) from ((100')).
Section 7.2.2.2: Satisfiability
Exercise 230. [M22] Show that the clauses with $i \ne j$ in the previous exercise form a minimal unsatisfiable set: Removing any one of them leaves a satisfiable remainder.
Verified: no
Solve time: 5m42s
Edit
Solution
Let (F) denote the set of clauses from the previous exercise after removing the tautological cases (i=j) from ((100')). Exercise 229 proves that (F) is unsatisfiable. Therefore it remains only to prove that every clause of (F) is essential.
We interpret (x_{ij}=1) as a directed relation (i\prec j). The clauses
[ \bar{x}_{jj} ]
express irreflexivity, the clauses
[ \bar{x}{ij}\vee\bar{x}{jk}\vee x_{ik} ]
express the required instances of transitivity, and the clauses
[ x_{j1}\vee x_{j2}\vee\cdots\vee x_{jm} ]
express that every element has a successor.
First consider deleting a clause of type ((99)), say
[ \bar{x}_{aa}. ]
Assign (x_{ij}=1) for all (i,j). Every clause of type ((100')) is satisfied, because every positive literal (x_{ik}) is true. Every clause of type ((101)) is satisfied because each row contains true literals. The only false clauses are the clauses (\bar{x}{jj}), and among them only the removed clause (\bar{x}{aa}) is false. Hence the remaining clauses are satisfiable.
Next delete a clause of type ((101)), say
[ x_{a1}\vee x_{a2}\vee\cdots\vee x_{am}. ]
Choose any strict total ordering of the elements in which (a) is the greatest element, and let (x_{ij}=1) exactly when (i) precedes (j) in this ordering. This relation is irreflexive and transitive, so all clauses of types ((99)) and ((100')) hold. Every element different from (a) has a successor, namely (a). The element (a) has no successor, because it is the greatest element. Thus every clause of type ((101)) except the deleted one is satisfied.
It remains to consider a clause of type ((100')). Let the deleted clause be
[ \bar{x}{ij}\vee\bar{x}{jk}\vee x_{ik}, ]
where
[ i\leq k,\qquad j<k,\qquad i\ne j . ]
There are two cases.
Suppose first that (i<k). Choose a strict total ordering of the elements in which (i), (j), and (k) occur consecutively in the order
[ i\prec j\prec k . ]
Let (R) consist of all pairs of this total ordering except the pair ((i,k)). In addition, if the greatest element of the ordering has no successor, add the pair from the greatest element to the least element. Because (i,j,k) are consecutive, the only missing transitive consequence created by deleting ((i,k)) is
[ i\prec j,\qquad j\prec k,\qquad i\nprec k . ]
The added successor edge can be chosen at the end of the ordering away from (i,j,k), so it creates no additional instance of a clause of type ((100')). Thus every transitivity clause except the deleted one is satisfied. The deleted clause is false because
[ x_{ij}=1,\qquad x_{jk}=1,\qquad x_{ik}=0 . ]
Every element has a successor, because the original ordering supplies successors except for its greatest element, which receives the added successor edge.
Now suppose that (i=k). The deleted clause has the form
[ \bar{x}{ij}\vee\bar{x}{ji}\vee x_{ii}. ]
Because the clauses of type ((99)) remain, (x_{ii}=0), so this clause is precisely the prohibition of the two-cycle
[ i\prec j,\qquad j\prec i . ]
Choose a directed ordering of the elements in which (j) is immediately followed by (i). Let (R) contain all forward pairs in this ordering, together with the single reverse pair
[ i\prec j . ]
If the final element of the ordering has no successor, add one successor edge from it to the first element of the ordering. The adjacency of (j) and (i) ensures that the only possible failure of transitivity involving the added reverse pair is
[ i\prec j,\qquad j\prec i, ]
whose missing conclusion is
[ i\prec i . ]
This is exactly the deleted clause. No other clause of type ((100')) is violated. All elements have successors by the added edge. Therefore the remaining clauses are satisfiable after deleting any clause of type ((100')), including the cases (i=k) that were omitted in the previous argument.
We have shown that removing any clause of type ((99)), ((100')), or ((101)) leaves a satisfiable formula. Since the complete set is unsatisfiable by exercise 229, every clause is necessary. Hence the clauses with (i\ne j) form a minimal unsatisfiable set.
This completes the proof.
∎