TAOCP 7.2.2.2 Exercise 437
Let A=\{a_1,\ldots,a_m\}.
Section 7.2.2.2: Satisfiability
Exercise 437. [M21] [M21] Extend exercise 436 to the general case where $A$ has more than two letters.
Verified: no
Solve time: 8m16s
Solution
Let
$$ A={a_1,\ldots,a_m}. $$
Introduce variables
$$ X_{k,a}\qquad(1\le k\le n,\ a\in A), $$
where $X_{k,a}$ denotes that the $k$th letter is $a$. The input encoding is forced by the clauses
$$ (X_{k,a_1}\vee\cdots\vee X_{k,a_m}) \qquad(1\le k\le n), $$
and
$$ (\bar X_{k,a}\vee\bar X_{k,b}) \qquad(1\le k\le n,\ a,b\in A,\ a\ne b). $$
The first family forces at least one letter at each position, and the second family forbids two different letters at the same position. Hence every satisfying assignment determines a unique word $x_1\ldots x_n\in A^n$ by
$$ X_{k,a}=1\iff x_k=a . $$
Let
$$ T\subseteq Q\times A\times Q $$
be the transition relation. Introduce auxiliary variables
$$ P_{k,q}\qquad(0\le k\le n,\ q\in Q), $$
where $P_{k,q}$ means that state $q$ is reachable after reading the prefix $x_1\ldots x_k$.
The initial values of the reachable-state variables are forced by
$$ (P_{0,q})\qquad(q\in I), $$
and
$$ (\bar P_{0,q})\qquad(q\in Q\setminus I). $$
For each transition
$$ (q,a,r)\in T $$
and each position $k$, introduce an auxiliary variable
$$ Y_{k,q,a,r}. $$
This variable represents the statement
$$ P_{k-1,q}\wedge X_{k,a}. $$
It is forced by the three clauses
$$ (\bar Y_{k,q,a,r}\vee P_{k-1,q}), $$
$$ (\bar Y_{k,q,a,r}\vee X_{k,a}), $$
and
$$ (\bar P_{k-1,q}\vee\bar X_{k,a}\vee Y_{k,q,a,r}). $$
The first two clauses give
$$ Y_{k,q,a,r}=1\Longrightarrow (P_{k-1,q}=1\ \wedge\ X_{k,a}=1), $$
and the third clause gives the converse implication. Therefore
$$ Y_{k,q,a,r} \iff (P_{k-1,q}\wedge X_{k,a}). $$
The reachable-state variables are then forced by requiring that a state is reachable exactly when some transition variable entering it is true. For every $k$ and every $r\in Q$, let
$$ S_{k,r}={Y_{k,q,a,r}:(q,a,r)\in T}. $$
If $S_{k,r}$ is nonempty, include the clauses
$$ (\bar Y\vee P_{k,r}) \qquad(Y\in S_{k,r}), $$
and
$$ (\bar P_{k,r}\vee\bigvee_{Y\in S_{k,r}}Y). $$
The first family says that every active transition entering $r$ makes $r$ reachable. The second says that a reachable state must have an active incoming transition. If $S_{k,r}$ is empty, include instead the unit clause
$$ (\bar P_{k,r}). $$
Thus, for every $k$ and $r$,
$$ P_{k,r} \iff \bigvee_{(q,a,r)\in T} Y_{k,q,a,r}. $$
Since every $Y_{k,q,a,r}$ is forced by the preceding values of the $P$ and $X$ variables, the $P$ variables are forced inductively from the input word.
The accepting condition is represented by the clause
$$ \bigvee_{q\in O}P_{n,q}. $$
It remains to prove that the formula is satisfiable exactly for the words accepted by the automaton.
Suppose first that
$$ x_1\ldots x_n\in L. $$
There exists a sequence of states
$$ q_0,q_1,\ldots,q_n $$
such that
$$ q_0\in I, $$
$$ (q_{k-1},x_k,q_k)\in T \qquad(1\le k\le n), $$
and
$$ q_n\in O. $$
Set
$$ X_{k,a}=1\iff x_k=a. $$
For each $k$, set $P_{k,r}=1$ exactly for the states reachable after reading the prefix $x_1\ldots x_k$. Set every $Y_{k,q,a,r}$ according to
$$ Y_{k,q,a,r}=P_{k-1,q}\wedge X_{k,a}. $$
The clauses defining the $Y$ variables are satisfied by construction. The clauses defining the $P$ variables are satisfied because a state is reachable precisely when there is an active transition entering it. Finally, $P_{n,q_n}=1$ and $q_n\in O$, so the accepting clause is satisfied.
Conversely, suppose that the clauses have a satisfying assignment. The letter clauses determine a unique word
$$ x_1\ldots x_n\in A^n. $$
The clauses for the $Y$ variables force
$$ Y_{k,q,a,r}=1 $$
exactly when
$$ P_{k-1,q}=1 $$
and
$$ x_k=a. $$
The clauses for the $P$ variables therefore force
$$ P_{k,r}=1 $$
exactly when there exists a transition
$$ (q,x_k,r)\in T $$
with
$$ P_{k-1,q}=1. $$
Together with the forced initial values, induction on $k$ gives
$$ P_{k,r}=1 \iff \text{state $r$ is reachable after reading }x_1\ldots x_k . $$
The accepting clause gives some $q_n\in O$ with
$$ P_{n,q_n}=1. $$
Hence $q_n$ is reachable after reading the entire word, so there exists an accepting state sequence. Therefore
$$ x_1\ldots x_n\in L. $$
The construction is forcing because the variables $X_{k,a}$ determine the word, the $Y$ variables are uniquely determined by the preceding $P$ and $X$ variables, and the $P$ variables are uniquely determined by the initial conditions and the exact recurrence above.
The clause count is obtained directly. The input encoding contributes
$$ n $$
clauses of length $|A|$ and
$$ n\binom{|A|}{2} $$
binary clauses. The $Y$ definitions contribute
$$ 3n|T| $$
clauses. The clauses defining the $P$ variables contribute at most one reverse clause for each pair $(k,r)$ and one implication clause for each transition occurrence, already counted among the transition contributions. Therefore the total number of clauses is
$$ O\bigl(n(|A|^2+|T|+|Q|)\bigr). $$
For a fixed finite automaton, $|A|$, $|Q|$, and $|T|$ are constants, so the number of clauses is
$$ O(n|T|). $$
This extends the construction of exercise 436 to every finite alphabet $A$. This completes the proof.
∎