Section 7.2.2.2: Satisfiability

Exercise 280. ▶ [M26] The problem $\text{cook}(j, k)$ consists of all $\binom{n}{j}$ positive $j$-clauses and all $\binom{n}{k}$ negative $k$-clauses on ${1, \ldots, n}$, where $n = j + k - 1$. For example, $\text{cook}(2, 3)$ is

$${12, 13, 14, 23, 24, 34, 123, 124, 134, 234}.$$

a) Why are these clauses obviously unsatisfiable?

b) Find a totally positive certificate for $\text{cook}(j, k)$, of length $\binom{n}{j-1}$.

c) Prove in fact that Algorithm C uses exactly $\binom{n}{j-1}$ clauses when it proves the unsatisfiability of $\text{cook}(j, k)$, if $M_0 = M_t = \infty$ (no purging or flushing).

Verified: no
Solve time: 5m23s

---

Setup

Let

$$ F=\operatorname{cook}(j,k), \qquad n=j+k-1 . $$

The clauses of $F$ are all positive clauses of length $j$ and all negative clauses of length $k$ on the variables ${1,\ldots,n}$. If $A$ is a set of variables, the positive clause on $A$ is denoted by $A$, and the negative clause on $A$ is denoted by $\bar A$.

We prove that $F$ is unsatisfiable, construct a totally positive certificate of length

$$ \binom{n}{j-1}, $$

and then analyze the exact clauses generated by Algorithm C when

$$ M_0=M_t=\infty . $$

The last condition means that learned clauses are neither purged nor flushed.

Solution

For part (a), suppose that an assignment satisfies $F$. Let $T$ be the set of variables assigned value $1$.

Every positive $j$-clause must contain a variable in $T$. If the complement of $T$ contained a set of $j$ variables, the positive clause on those variables would be false. Therefore

$$ |{1,\ldots,n}\setminus T|\le j-1 . $$

Using $n=j+k-1$, we obtain

$$ |T| =n-|{1,\ldots,n}\setminus T| \ge (j+k-1)-(j-1) =k . $$

Hence $T$ contains some subset $B$ with

$$ |B|=k . $$

The negative clause $\bar B$ belongs to $F$. Every variable in $B$ has value $1$, so every literal in $\bar B$ is false. Thus $\bar B$ is false, contradicting the assumption that the assignment satisfies $F$. Therefore $\operatorname{cook}(j,k)$ is unsatisfiable.

For part (b), let $A$ be any subset of ${1,\ldots,n}$ satisfying

$$ |A|=j-1 . $$

Let

$$ B={1,\ldots,n}\setminus A . $$

Then

$$ |B| =n-(j-1) =j+k-1-j+1 =k . $$

We prove that the positive clause $A$ follows from $F$.

Assume that all literals in $A$ are false. For each $b\in B$, the set

$$ A\cup{b} $$

has size $j$, so the positive clause $A\cup{b}$ belongs to $F$. Under the assumption that all variables in $A$ are false, this clause becomes the unit clause $b$. Unit propagation therefore forces every variable in $B$ to be true.

The negative clause $\bar B$ also belongs to $F$, because $|B|=k$. After propagation, all literals in $\bar B$ are false, so this clause becomes the empty clause $\epsilon$. Therefore

$$ F\wedge\bigwedge_{a\in A}\bar a\vdash_1\epsilon . $$

Resolving the contradiction with the assumptions ${\bar a:a\in A}$ produces the positive clause $A$. Hence every $(j-1)$-subset $A$ gives a valid positive derived clause.

The number of possible choices for $A$ is

$$ \binom{n}{j-1}. $$

Therefore the clauses

$$ A,\qquad |A|=j-1 , $$

form a totally positive certificate of length

$$ \boxed{\binom{n}{j-1}} . $$

For part (c), we analyze the behavior of Algorithm C. The previous construction gives a lower bound on the number of clauses that Algorithm C must generate. It remains to prove that Algorithm C generates precisely these clauses and no others.

Consider a stage of Algorithm C before the final contradiction is obtained. Let $D$ be the set of decision literals that have been assigned false. Because all positive $j$-clauses are present, Algorithm C cannot continue with $j$ variables false without immediately encountering a falsified positive clause. Thus every consistent branch has

$$ |D|\le j-1 . $$

Suppose first that

$$ |D|=j-1 . $$

Write

$$ D=A . $$

The variables outside $A$ form the set

$$ B={1,\ldots,n}\setminus A , $$

with

$$ |B|=k . $$

For every $b\in B$, the original clause

$$ A\cup{b} $$

has all literals in $A$ false, so unit propagation forces $b$ to be true. Consequently the negative clause

$$ \bar B $$

becomes false.

Algorithm C resolves the conflict clause $\bar B$ against the clauses $A\cup{b}$ used in the propagation chain. Each resolution removes one negative literal $\bar b$ from $\bar B$ and leaves the literals of $A$. After all $k$ variables of $B$ have been eliminated, the learned clause is

$$ A . $$

Thus every conflict reached after exactly $j-1$ false decisions produces the corresponding positive $(j-1)$-clause.

It remains to show that Algorithm C reaches every such conflict exactly once and reaches no other kind of conflict before the final contradiction.

When $M_0=M_t=\infty$, every learned clause remains available. A learned clause

$$ A $$

with

$$ |A|=j-1 $$

blocks exactly the assignments in which every variable of $A$ is false. It cannot block any branch corresponding to a different $(j-1)$-subset, because some literal of the two subsets differs and that literal is not false on the other branch.

Therefore each newly learned clause eliminates only the unique maximal false decision set from which it was derived. As long as some $(j-1)$-subset $A$ has not been learned, the branch assigning all variables of $A$ false is not blocked by any previously learned clause. Algorithm C therefore reaches that branch, performs the propagation described above, and learns the clause $A$.

There are

$$ \binom{n}{j-1} $$

possible choices of $A$, so Algorithm C must generate at least this many learned clauses.

Conversely, every conflict before the final contradiction arises from a maximal consistent branch of the search tree. Such a branch has exactly $j-1$ false decisions. A branch with fewer false decisions is not a terminal branch, because its complement contains more than $k$ variables and no negative $k$-clause can yet be falsified. A branch with more false decisions is impossible because a positive $j$-clause would already be false. Hence every learned clause before the final contradiction has exactly $j-1$ positive literals and is one of the clauses described above.

After all

$$ \binom{n}{j-1} $$

positive clauses have been learned, every maximal false decision set is blocked. The search cannot produce another such conflict, and the remaining propagation reaches the empty clause. Since $M_0=M_t=\infty$, no learned clause has disappeared during this process.

Therefore Algorithm C generates exactly the positive clauses

$$ A,\qquad A\subseteq{1,\ldots,n},\quad |A|=j-1 , $$

before the final contradiction. Their number is

$$ \boxed{\binom{n}{j-1}} . $$

Verification

For the example $\operatorname{cook}(2,3)$,

$$ n=2+3-1=4 . $$

The predicted number of clauses generated by Algorithm C is

$$ \binom{4}{2-1}

\binom41

4 . $$

The possible sets $A$ of size $j-1=1$ are

$$ {1},{2},{3},{4}. $$

The learned clauses are therefore

$$ 1,\qquad 2,\qquad 3,\qquad 4 . $$

For example, assuming $1$ false forces $2,3,4$ true through the positive binary clauses

$$ 12,\qquad 13,\qquad 14 , $$

and the negative clause

$$ \bar2\bar3\bar4 $$

creates the conflict whose resolution gives the learned clause $1$. The other three cases are symmetric.

The count agrees with the general formula, and the argument above proves that no additional clauses are generated before the final contradiction.

This completes the proof. ∎