TAOCP 7.2.2.2 Exercise 439
We construct forcing clauses directly from a finite-state process that counts the number of $1$s while remembering whether the preceding bit was $1$.
Section 7.2.2.2: Satisfiability
Exercise 439. [20] [20] Construct forcing clauses expressing the constraint that $x_1 + \cdots + x_n = l$ and that there are no two consecutive 1s. (This is the special case $l_1 = \cdots = l_t = 1$ of the previous exercise, but a much simpler construction is possible.)
Verified: no
Solve time: 7m50s
Solution
We construct forcing clauses directly from a finite-state process that counts the number of $1$s while remembering whether the preceding bit was $1$. This avoids the need to specify all possible runs separately.
For $0\leq k\leq n$ and $0\leq j\leq l$, let
$$ A_{k,j} $$
denote the state that after reading $x_1,\ldots,x_k$ exactly $j$ of the symbols have been $1$. We also need to remember whether the last symbol read was a $1$. Thus define two kinds of states:
$$ Q={q_{j,0}:0\leq j\leq l}\cup{q_{j,1}:0\leq j\leq l}. $$
The second subscript records the value of the most recently read bit. The state $q_{j,0}$ means that exactly $j$ ones have occurred so far and the last bit read is $0$ (or no bit has yet been read when $j=0$). The state $q_{j,1}$ means that exactly $j$ ones have occurred so far and the last bit read is $1$.
The initial state is
$$ q_{0,0}. $$
The accepting states are
$$ {q_{l,0},q_{l,1}}. $$
The transition rules are the following.
For every $0\leq j\leq l$,
$$ (q_{j,0},0,q_{j,0})\in T . $$
A zero does not change the number of ones and leaves the automaton in the state whose second component is $0$.
For
$$ 0\leq j<l, $$
we have
$$ (q_{j,0},1,q_{j+1,1})\in T . $$
A one increases the count by one and makes the last bit equal to $1$.
For
$$ 0\leq j\leq l, $$
we have
$$ (q_{j,1},0,q_{j,0})\in T . $$
A zero after a one is allowed and resets the last-bit flag.
No transition of the form
$$ (q_{j,1},1,r) $$
is present, because two consecutive ones are forbidden. No transition increasing the number of ones beyond $l$ is present.
This deterministic automaton accepts exactly the binary strings having exactly $l$ ones and no two consecutive ones. The count component of every reachable state is the number of ones in the prefix, and the second component records whether the last symbol is one. Therefore an accepting state can be reached exactly when the complete string has $l$ ones and the final symbol does not violate the restriction. Conversely, every string satisfying the two constraints follows the unique transitions above and ends in one of the two accepting states.
We now convert this automaton into forcing clauses. Introduce variables
$$ P_{k,q} \qquad (0\leq k\leq n,\ q\in Q), $$
where $P_{k,q}$ means that the automaton is in state $q$ after reading
$$ x_1\ldots x_k . $$
The initial conditions are
$$ (P_{0,q_{0,0}}) $$
and
$$ (\bar P_{0,q}) \qquad (q\in Q,\ q\ne q_{0,0}). $$
For every transition
$$ (q,b,r)\in T $$
and every
$$ 1\leq k\leq n, $$
include the clause
$$ (\bar P_{k-1,q}\vee \overline{L_{k,b}}\vee P_{k,r}), $$
where
$$ L_{k,1}=x_k, \qquad L_{k,0}=\bar{x}_k . $$
These clauses force every successor state required by an active state and the current input bit.
To force the converse direction, introduce auxiliary variables
$$ Y_{k,q,b} $$
for every pair $(q,b)$ that occurs in a transition. The intended meaning is
$$ Y_{k,q,b}\iff P_{k-1,q}\wedge(x_k=b). $$
For $b=1$, use the clauses
$$ (\bar Y_{k,q,1}\vee P_{k-1,q}), $$
$$ (\bar Y_{k,q,1}\vee x_k), $$
and
$$ (\bar P_{k-1,q}\vee\bar x_k\vee Y_{k,q,1}). $$
For $b=0$, use the clauses
$$ (\bar Y_{k,q,0}\vee P_{k-1,q}), $$
$$ (\bar Y_{k,q,0}\vee\bar x_k), $$
and
$$ (\bar P_{k-1,q}\vee x_k\vee Y_{k,q,0}). $$
For every $k$ and every state $r$, add
$$ \left( \bar P_{k,r} \vee \bigvee_{(q,b,r)\in T}Y_{k,q,b} \right). $$
This clause requires every active state at time $k$ to have a predecessor transition from time $k-1$.
Finally, require acceptance:
$$ (P_{n,q_{l,0}}\vee P_{n,q_{l,1}}). $$
Suppose first that
$$ x_1\ldots x_n $$
has exactly $l$ ones and contains no two consecutive ones. The automaton has a unique computation beginning at $q_{0,0}$ and ending in either $q_{l,0}$ or $q_{l,1}$. Set
$$ P_{k,q}=1 $$
exactly for the state reached after the first $k$ symbols, and set each $Y_{k,q,b}$ according to its defining equivalence. Every transition clause is satisfied because the computation follows a transition of $T$. Every reverse clause is satisfied because each active state has the transition that produced it. The final clause is satisfied because the computation ends in an accepting state.
Conversely, suppose the clauses have a satisfying assignment. The initial clauses force the computation to start in $q_{0,0}$. The clauses defining the $Y$ variables make them true exactly for the active predecessor state and the current input symbol. The forward clauses force every valid successor state to become active, while the reverse clauses prevent any state without a predecessor from becoming active. Since the transition relation is deterministic, induction on $k$ shows that exactly one variable $P_{k,q}$ is true, namely the state reached by the automaton after reading
$$ x_1\ldots x_k . $$
The accepting clause forces the final state to be either $q_{l,0}$ or $q_{l,1}$. By the definition of the states, the input contains exactly $l$ ones. Since no transition permits a one after a state whose second component is $1$, the input has no two consecutive ones.
The auxiliary variables are forcing variables. For a fixed input string, the deterministic computation fixes every value of every $P_{k,q}$, and the defining clauses then fix every value of every $Y_{k,q,b}$.
The number of states is
$$ 2(l+1). $$
The number of transitions is bounded by
$$ (l+1)+(l)+ (l+1)=3l+2, $$
coming respectively from the zero transitions from $q_{j,0}$, the one transitions from $q_{j,0}$ for $j<l$, and the zero transitions from $q_{j,1}$. Thus the number of clauses is linear in $n$ for fixed $l$.
This completes the proof.
∎