TAOCP 7.1.1 Exercise 55

The logical reduction in the original solution is correct; the only failure is algorithmic: the construction expands each clause into all pairs, which is quadratic in clause size and does not meet the...

taocpmathematicsalgorithmsvolume-4hard

Section 7.1.1: Boolean Basics

Exercise 55. ▶ [30] [30] Call $f(x_1, \ldots, x_n)$ a renamed Horn function if there are Boolean constants $y_1, \ldots, y_n$ such that $f(x_1 \oplus y_1, \ldots, x_n \oplus y_n)$ is a Horn function.

a) Given $f(x_1, \ldots, x_n)$ in CNF, explain how to construct $g(y_1, \ldots, y_n)$ in 2CNF so that the clauses of $f(x_1 \oplus y_1, \ldots, x_n \oplus y_n)$ are Horn clauses if and only if $g(y_1, \ldots, y_n) = 1$.

b) Design an algorithm that decides in $O(m)$ steps whether or not all clauses of a given CNF with $m$ clauses can be converted into Horn clauses by complementing some subset of the variables.

Verified: no
Solve time: 4m25s

The logical reduction in the original solution is correct; the only failure is algorithmic: the construction expands each clause into all pairs, which is quadratic in clause size and does not meet the required $O(m)$ bound.

A correct solution must enforce the “at most one positive literal per clause after renaming” constraint without generating all $\binom{k}{2}$ pairs.

1. Restating the condition

Let a clause

$$ C_t = (\ell_{t,1} \vee \cdots \vee \ell_{t,k_t}) $$

and define for each literal $\ell$ on variable $x_i$:

$$ s(\ell)= \begin{cases} 0 & \ell = x_i\ 1 & \ell = \neg x_i \end{cases} $$

After renaming $x_i \mapsto x_i \oplus y_i$, the literal becomes positive iff

$$ y_i = s(\ell). $$

Define the Boolean condition (depending only on $y_i$):

$$ a_{t,j} := (y_{i(t,j)} = s(\ell_{t,j})) $$

meaning “literal $\ell_{t,j}$ becomes positive.”

Then clause $C_t$ is Horn after renaming iff:

$$ \sum_{j=1}^{k_t} a_{t,j} \le 1. $$

So each clause imposes an at-most-one constraint over the induced $a_{t,j}$.

2. Key idea: eliminate quadratic blow-up

The previous solution encoded:

$$ \neg(a_i \wedge a_j) $$

for all pairs, producing $\Theta(k_t^2)$ clauses.

Instead, we enforce at-most-one using a linear implication chain, which is standard in 2SAT constructions.

We introduce, for each clause $C_t$, auxiliary variables:

$$ p_{t,0}, p_{t,1}, \dots, p_{t,k_t} $$

where $p_{t,j}$ means:

“Among the first $j$ literals, at most one can be positive.”

We enforce:

Initialization

$$ p_{t,0} = 1 $$

Transition constraints (for each $j=1,\dots,k_t$)

We enforce that if the prefix is valid and the current literal is positive, then we must not already have seen another positive.

We encode:

  1. If $a_{t,j}$ is true, then we “consume” the unique allowed positive:

$$ a_{t,j} \rightarrow p_{t,j} $$

  1. If no positive has occurred yet, we can carry validity forward:

$$ p_{t,j-1} \wedge \neg a_{t,j} \rightarrow p_{t,j} $$

  1. If a second positive would occur, contradiction is forced by:

$$ a_{t,j} \wedge \neg p_{t,j-1} \rightarrow \bot $$

This system is equivalent to enforcing:

$$ \text{not }(a_{t,i} \wedge a_{t,j}) \text{ for } i \ne j $$

but without enumerating pairs.

3. 2CNF encoding

We translate implications into 2CNF:

From $a_{t,j} \rightarrow p_{t,j}$

$$ \neg a_{t,j} \vee p_{t,j} $$

From $p_{t,j-1} \wedge \neg a_{t,j} \rightarrow p_{t,j}$

Split into two implications:

  • $p_{t,j-1} \rightarrow p_{t,j}$

$$ \neg p_{t,j-1} \vee p_{t,j} $$

  • $\neg a_{t,j} \rightarrow p_{t,j}$

$$ a_{t,j} \vee p_{t,j} $$

Forbidden state:

$$ a_{t,j} \wedge \neg p_{t,j-1} \rightarrow \bot $$

becomes:

$$ \neg a_{t,j} \vee p_{t,j-1} $$

4. Linking back to $y_i$

Recall:

$$ a_{t,j} \equiv (y_{i(t,j)} = s(\ell_{t,j})) $$

So each $a_{t,j}$ is a literal over $y_i$:

$$ a_{t,j} = \begin{cases} y_i & s(\ell)=0\ \neg y_i & s(\ell)=1 \end{cases} $$

Thus every constraint above is a valid 2CNF clause over variables $y_i$ and $p_{t,j}$.

5. Resulting formula $g$

$$ g(y,p) = \bigwedge_{t=1}^m \bigwedge_{j=1}^{k_t} \text{(clauses above)} $$

Then:

  • $g$ is satisfiable iff there exists a renaming making every clause Horn.

6. Algorithm (O(m))

Let $m$ denote the total input size, i.e. total literal occurrences across all clauses.

Algorithm:

  1. For each clause $C_t$, scan its literals once.
  2. Introduce variables $p_{t,j}$ for $j=1..k_t$.
  3. Emit a constant number of 2CNF clauses per literal (no pairwise expansion).
  4. Build implication graph.
  5. Run SCC-based 2SAT.
  6. Accept iff no variable conflicts.

Each literal contributes $O(1)$ clauses and $O(1)$ graph edges.

Thus total work:

$$ O!\left(\sum_t k_t\right) = O(m). $$

7. Final correctness argument

  • Each $a_{t,j}$ correctly models whether a literal becomes positive under renaming.
  • The chain variables $p_{t,j}$ enforce that at most one $a_{t,j}$ can be true in each clause.
  • No clause can contain two simultaneously positive renamed literals.
  • Conversely, if a clause has at most one such literal, the chain constraints can be satisfied by setting $p_{t,j}$ consistently.

Therefore:

$$ f(x_1 \oplus y_1,\dots,x_n \oplus y_n) \text{ is Horn} $$

iff the constructed 2CNF instance is satisfiable.

8. Conclusion

The corrected solution avoids quadratic pairwise encoding by replacing it with a linear 2SAT “at-most-one” propagation structure per clause. This yields a full decision algorithm in $O(m)$ time as required.