TAOCP 7.2.2.2 Exercise 440
Edit Let the fixed context free grammar be given by the nonterminal set $N$, the set of initial nonterminals $S\subseteq N$, the terminal productions $U$, and the binary productions $W$.
Section 7.2.2.2: Satisfiability
Exercise 440. [M33] [M33] Extend exercise 436 to context free languages, which can be defined by a set $S \subseteq N$ and by production rules $U$ and $W$ of the following well-known forms: $U \subseteq {P \to a \mid P \in N,\ a \in A}$ and $W \subseteq {P \to QR \mid P, Q, R \in N}$, where $N$ is a set of "nonterminal symbols." A string $x_1 \ldots x_n$ with each $x_i \in A$ belongs to the language if and only if it can be produced from a nonterminal symbol $P \in S$.
Verified: yes
Solve time: 7m32s
Edit
Setup
Let the fixed context free grammar be given by the nonterminal set $N$, the set of initial nonterminals $S\subseteq N$, the terminal productions $U$, and the binary productions $W$. Let the input string be
$$ x_1x_2\cdots x_n, $$
where every $x_i\in A$.
For every interval $1\leq i\leq j\leq n$ and every nonterminal $P\in N$, introduce a Boolean variable
$$ X_{i,j,P}. $$
The intended meaning is that $X_{i,j,P}$ is true when the substring
$$ x_i x_{i+1}\cdots x_j $$
has a derivation from $P$.
We construct forcing clauses that are satisfiable exactly when some $P\in S$ derives the whole string.
Solution
The construction uses witness variables so that a true interval variable always has an explicit production witnessing its derivation.
For every terminal production
$$ P\to a\in U $$
and every position $i$ satisfying
$$ x_i=a, $$
introduce a witness variable
$$ Y_{i,P,a}. $$
This variable represents the use of the production $P\to a$ on the one-letter interval $x_i$. Add the clauses
$$ (\overline{Y}{i,P,a}\vee X{i,i,P}), $$
and
$$ (\overline{X}{i,i,P}\vee Y{i,P,a}). $$
The first clause says that a terminal witness implies the corresponding interval is derivable. The second clause says that a true one-letter interval variable must have a terminal witness.
For every position $i$ and every nonterminal $P$ for which no terminal production
$$ P\to x_i $$
exists, add the clause
$$ (\overline{X}_{i,i,P}). $$
Thus a one-letter interval variable can be true exactly when a matching terminal production exists and a corresponding witness is chosen.
Now consider a binary production
$$ P\to QR\in W. $$
For every interval $[i,j]$ with $i<j$ and every split point
$$ i\leq k<j, $$
introduce a witness variable
$$ Y_{i,k,j,P,Q,R}. $$
Its intended meaning is
$$ Y_{i,k,j,P,Q,R} \iff X_{i,k,Q}\wedge X_{k+1,j,R}. $$
The equivalence is represented by the three clauses
$$ (\overline{Y}{i,k,j,P,Q,R}\vee X{i,k,Q}), $$
$$ (\overline{Y}{i,k,j,P,Q,R}\vee X{k+1,j,R}), $$
and
$$ (\overline{X}{i,k,Q}\vee\overline{X}{k+1,j,R}\vee Y_{i,k,j,P,Q,R}). $$
The first two clauses make every chosen binary witness require its two child derivations. The third clause allows the witness to be chosen whenever both child derivations are present.
For every $P\in N$ and every interval $[i,j]$ with $i<j$, add the clause
$$ \left( \overline{X}{i,j,P} \vee \bigvee{\substack{P\to QR\in W\i\leq k<j}} Y_{i,k,j,P,Q,R} \right). $$
This clause states that a true interval variable must have a binary production and split point witnessing it.
Finally add the start clause
$$ \left( \bigvee_{P\in S}X_{1,n,P} \right). $$
This completes the forcing clauses.
To prove correctness, suppose first that the string belongs to the language generated by the grammar. Choose a parse tree whose root is some $P\in S$. For every node of the parse tree labelled by a nonterminal $P$ and covering the interval $[i,j]$, set
$$ X_{i,j,P}=1. $$
Set every witness variable corresponding to a production occurrence in the parse tree equal to $1$, and set all other witness variables equal to $0$.
Every terminal witness clause is satisfied because each leaf of the parse tree corresponds to a production $P\to x_i$. Every binary witness clause is satisfied because each internal node labelled by $P$ with production $P\to QR$ has two child nodes corresponding to the two subintervals. The production clauses for the interval variables are satisfied because each true interval variable has a witness coming from the parse tree. The start clause is satisfied because the root nonterminal belongs to $S$.
Therefore every generated string gives a satisfying assignment.
Conversely, suppose the forcing clauses have a satisfying assignment. We prove by induction on interval length that
$$ X_{i,j,P}=1 $$
implies that
$$ x_i x_{i+1}\cdots x_j $$
can be derived from $P$.
For an interval of length one, if
$$ X_{i,i,P}=1, $$
then the clauses for terminal witnesses require some variable $Y_{i,P,x_i}$ to be true. By construction, this witness exists only when
$$ P\to x_i\in U. $$
Hence the one-letter string has a derivation from $P$.
Assume the claim holds for all intervals shorter than $[i,j]$, and suppose
$$ X_{i,j,P}=1 $$
with $i<j$. The clause for $X_{i,j,P}$ requires some witness
$$ Y_{i,k,j,P,Q,R}=1 $$
for a production
$$ P\to QR\in W $$
and some split point
$$ i\leq k<j. $$
The clauses defining this witness imply
$$ X_{i,k,Q}=1 $$
and
$$ X_{k+1,j,R}=1. $$
Both intervals have smaller length than $[i,j]$, so the induction hypothesis gives derivations
$$ x_i\cdots x_k $$
from $Q$ and
$$ x_{k+1}\cdots x_j $$
from $R$. Applying the production
$$ P\to QR $$
gives a derivation of
$$ x_i\cdots x_j $$
from $P$.
The start clause yields some $P\in S$ with
$$ X_{1,n,P}=1. $$
The induction result therefore gives a derivation of the entire input string from an allowed starting nonterminal. Hence the string belongs to the language generated by the grammar.
The number of variables and clauses is finite because there are finitely many intervals, nonterminals, and productions. Therefore every fixed context free grammar and input string can be transformed into a finite set of forcing clauses.
This completes the proof.
∎
Verification
The terminal case uses witness variables rather than forcing all possible terminal derivations to be true. This preserves the required satisfiability equivalence because a nonterminal is marked as deriving an interval only when a production occurrence witnesses that fact.
The binary case has the same structure as the usual context free parsing recurrence. A binary witness records one production and one split point, and the induction reconstructs a parse tree from any satisfying assignment.
The final clause requires exactly the condition defining membership in the language, namely that the complete string is derivable from at least one initial nonterminal.