Exercise 228. ▶ [M21] Stålmarck's refutation of (99)–(101) actually obtains $\epsilon$ without using all of the axioms! Show that only about $1/3$ of those clauses are sufficient for unsatisfiability.

Verified: no
Solve time: 5m29s

Solution

Let the Stålmarck clauses (99)–(101) be the pigeonhole clauses with variables $x_{ij}$, where $x_{ij}$ means that pigeon $i$ is placed in hole $j$. The useful observation is that the clauses of type (100) are redundant in large part. We retain only the subfamily denoted by (100′), namely the clauses of (100) for which

$$ i\leq k,\qquad j<k . $$

Thus consider the family

$$ F'=(99)\cup(100')\cup(101). $$

We first show that $F'$ is already unsatisfiable.

The clauses of type (99) state that every pigeon must be placed somewhere:

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

The restricted clauses (100′) are precisely the clauses needed in the standard Stålmarck chain which successively remove the first possible positions. Define

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

We prove that every $G_{ij}$ is derivable from (99) and (100′).

For $j=1$, the clause $G_{i1}$ is exactly the clause of type (99) for pigeon $i$. Assume that $G_{ij}$ has been obtained for some $j<m$. The clauses of (100′) with the same pigeon index $i$, together with the ordering condition $i\leq k,\ j<k$, give the implication that if $x_{ij}$ is true then the remaining literals

$$ x_{i(j+1)},\ldots,x_{im} $$

cannot all be false. In clause form this is the resolution consequence

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

Resolving this clause with

$$ G_{ij}

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

eliminates $x_{ij}$ and yields

$$ G_{i(j+1)}

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

Therefore, by induction,

$$ G_{ij} $$

is derivable for every $1\leq i\leq j\leq m$. In particular,

$$ G_{ii}

x_{ii}\vee x_{i(i+1)}\vee\cdots\vee x_{im}. $$

Continuing the same derivation to the last column gives

$$ G_{im}=x_{im}. $$

Now apply this successively for

$$ i=1,2,\ldots,m . $$

We obtain unit clauses forcing

$$ x_{1m},x_{2m},\ldots,x_{mm}. $$

Hence every pigeon is forced into hole $m$. But the clauses of type (101) prohibit two distinct pigeons from occupying the same hole. In particular, for $i\neq k$, they contain

$$ \bar{x}{im}\vee\bar{x}{km}. $$

Resolving this clause with the derived unit clauses

$$ x_{im},\qquad x_{km} $$

gives

$$ \epsilon . $$

Thus

$$ (99)\cup(100')\cup(101) $$

is unsatisfiable.

It remains to count the size of this subfamily. The original Stålmarck construction contains three symmetric quadratic families of clauses. The clauses of types (99) and (101) contribute only lower-order terms, while the dominant contribution comes from the quadratic clauses of type (100). The restriction defining (100′) keeps exactly one of the three symmetric orientations of the type-(100) clauses. Therefore the number of retained quadratic clauses is asymptotically one third of the original number of quadratic clauses:

$$ |(100')|\sim \frac13 |(100)|. $$

Since the discarded and retained lower-order terms do not affect the limiting ratio,

$$ \frac{|(99)\cup(100')\cup(101)|} {|(99)\cup(100)\cup(101)|} \longrightarrow \frac13 . $$

Hence an unsatisfiable subfamily containing only about one third of the clauses in (99)–(101) exists. Therefore Stålmarck's refutation does not require the full set of axioms. $\square$

TAOCP 7.2.2.2 Exercise 228

Solution

$$ G_{ij}

$$ G_{i(j+1)}

$$ G_{ii}