TAOCP 7.2.2.2 Exercise 438
The construction can be obtained from exercise 436 by using a deterministic finite automaton for the required regular language.
Section 7.2.2.2: Satisfiability
Exercise 438. [21] [21] Construct a set of forcing clauses that are satisfiable if and only if a given binary string $x_1 \ldots x_n$ contains exactly $t$ runs of 1s, having lengths $(l_1, l_2, \ldots, l_t)$ from left to right. (Equivalently, the string $x_1 \ldots x_n$ should belong to the language defined by the regular expression $0^1^{l_1}0^+1^{l_2}0^+ \ldots 0^+1^{l_t}0^$.)
Verified: yes
Solve time: 6m53s
Solution
The construction can be obtained from exercise 436 by using a deterministic finite automaton for the required regular language. The states must record both the number of completed runs and the position inside the current run or the intervening zeros.
Let
$$ s_i=\sum_{h=1}^{i}l_h $$
denote the total number of $1$s required in the first $i$ runs. Define the state set
$$ Q={q_0}\cup {q_{i,j}:1\le i\le t,\ 1\le j\le l_i} \cup {z_i:1\le i<t} \cup {q_t^\ast}. $$
The state $q_0$ represents the initial block of zeros before the first run. The state $q_{i,j}$ represents that the automaton is in the $i$th run of $1$s and that exactly $j$ symbols of this run have been read. The state $z_i$ represents that the $i$th run has been completed and that the automaton is reading the positive block of zeros between the $i$th and $(i+1)$st runs. The state $q_t^\ast$ represents that all $t$ runs have been completed and that only trailing zeros remain.
The initial state set is
$$ I={q_0}. $$
The output state set is
$$ O={q_t^\ast}\cup{q_{t,l_t}}. $$
The inclusion of $q_{t,l_t}$ is necessary because the last run may end at the end of the input, since the final factor $0^*$ may have length zero.
The transition relation $T$ is defined by the following rules.
From the initial zero state,
$$ (q_0,0,q_0)\in T, $$
and
$$ (q_0,1,q_{1,1})\in T. $$
Inside a run of $1$s,
$$ (q_{i,j},1,q_{i,j+1})\in T $$
for
$$ 1\le i\le t,\qquad 1\le j<l_i. $$
After a nonfinal run has been completed, the next symbol must be a zero, so
$$ (q_{i,l_i},0,z_i)\in T $$
for
$$ 1\le i<t. $$
The separating zero blocks have positive length, hence
$$ (z_i,0,z_i)\in T $$
and
$$ (z_i,1,q_{i+1,1})\in T $$
for
$$ 1\le i<t. $$
After the last run, only zeros are permitted:
$$ (q_{t,l_t},0,q_t^\ast)\in T, $$
and
$$ (q_t^\ast,0,q_t^\ast)\in T. $$
All other transitions are absent. This automaton accepts exactly
$$ 0^1^{l_1}0^+1^{l_2}0^+\cdots0^+1^{l_t}0^ . $$
Indeed, every accepted computation must begin in $q_0$, pass through the states $q_{1,1},\ldots,q_{1,l_1}$, then through the positive zero block represented by $z_1$, and so on, until it reaches either $q_{t,l_t}$ or $q_t^\ast$. Conversely, every string having the prescribed runs follows exactly these transitions.
Now apply the forcing construction of exercise 436. Introduce variables
$$ P_{k,q}\qquad(0\le k\le 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 state conditions are
$$ (P_{0,q_0}) $$
and
$$ (\bar P_{0,q}) \qquad(q\in Q,\ q\ne q_0). $$
For a transition
$$ (q,b,r)\in T, $$
define
$$ L_{k,1}=x_k, \qquad L_{k,0}=\bar{x}_k . $$
The forward transition clauses are
$$ (\bar P_{k-1,q}\vee \overline{L_{k,b}}\vee P_{k,r}) $$
for
$$ 1\le k\le n,\qquad (q,b,r)\in T. $$
These clauses force every state reached by a transition from an active state to become active.
To force the converse direction, introduce variables
$$ Y_{k,q,b} $$
for every transition label pair $(q,b)$ occurring in $T$. The variable $Y_{k,q,b}$ represents
$$ P_{k-1,q}\wedge(x_k=b). $$
For $b=1$ we use
$$ (\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$ we use
$$ (\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 the clause
$$ \left( \bar P_{k,r} \vee \bigvee_{(q,b,r)\in T}Y_{k,q,b} \right). $$
This forces every active state to have a predecessor transition from the preceding time step.
Finally, the accepting condition is represented by
$$ (P_{n,q_t^\ast}\vee P_{n,q_{t,l_t}}). $$
The clauses are satisfiable exactly for the desired strings. If
$$ x_1\ldots x_n $$
has the required sequence of runs, the deterministic automaton has a unique computation
$$ q_0,q_1,\ldots,q_n . $$
Set
$$ P_{k,q}=1 $$
exactly when
$$ q=q_k. $$
Set each $Y_{k,q,b}$ according to the equivalence
$$ Y_{k,q,b}\iff(P_{k-1,q}\wedge(x_k=b)). $$
Every forward clause is satisfied because each step of the computation follows a transition in $T$. Every reverse clause is satisfied because the unique active state at time $k$ has the transition that produced it. The final state is either $q_{t,l_t}$ or $q_t^\ast$, so the accepting clause is satisfied.
Conversely, suppose the clauses have a satisfying assignment. The initial clauses force the automaton to start in $q_0$. The clauses defining the $Y$ variables force them to represent exactly the active state and the current input symbol. Since the transition relation is deterministic, induction on $k$ shows that exactly the state reached by the automaton after reading
$$ x_1\ldots x_k $$
has its variable $P_{k,q}$ set to $1$. The forward clauses guarantee that the actual successor is active, and the reverse clauses prohibit any state without a predecessor from becoming active. Therefore the accepting clause implies that the unique computation ends in $q_{t,l_t}$ or $q_t^\ast$. By the definition of the automaton, the input string has exactly the required $t$ runs of $1$s with lengths
$$ (l_1,l_2,\ldots,l_t). $$
The forcing property follows from the uniqueness of the computation. The input variables determine a unique automaton state after every prefix. Hence every $P_{k,q}$ is uniquely determined. Each $Y_{k,q,b}$ is uniquely determined by the values of $P_{k-1,q}$ and $x_k$. Thus all auxiliary variables have forced values whenever the clauses are satisfiable.
The number of states is
$$ 1+\sum_{i=1}^{t}l_i+(t-1)+1, $$
and the number of transitions is bounded by a constant depending only on
$$ t,l_1,\ldots,l_t . $$
For each transition and each position $k$, the construction adds a constant number of clauses, and each state contributes one reverse clause for each $k$. Therefore the total number of clauses is
$$ O(n). $$
This completes the proof.
∎