TAOCP 7.2.2.2 Exercise 109
Let $F(x_1,\ldots,x_n)$ be the given satisfiability instance, and assume access to a SAT solver that decides satisfiability and returns a satisfying assignment when one exists.
Section 7.2.2.2: Satisfiability
Exercise 109. ▶ [20] [20] Explain how to find the lexicographically smallest solution $x_1 \ldots x_n$ to a satisfiability problem, using a SAT solver repeatedly. (See Fig. 37(a).)
Verified: yes
Solve time: 1m04s
Solution
Let $F(x_1,\ldots,x_n)$ be the given satisfiability instance, and assume access to a SAT solver that decides satisfiability and returns a satisfying assignment when one exists.
The lexicographically smallest satisfying assignment is constructed by fixing variables in order $x_1, x_2, \ldots, x_n$, always attempting $0$ before $1$.
For each $i$, define the working formula
$$ F^{(i)} = F \wedge \bigwedge_{j=1}^{i-1} (x_j = a_j), $$
where $a_j \in {0,1}$ are the values already fixed, and $(x_j = 0)$ is the unit clause $\bar{x}_j$, while $(x_j = 1)$ is the unit clause $x_j$.
At stage $i$, form the two candidate formulas
$$ F^{(i)}_0 = F^{(i)} \wedge \bar{x}_i, \qquad F^{(i)}_1 = F^{(i)} \wedge x_i. $$
The algorithm proceeds by testing satisfiability of $F^{(i)}_0$ using the SAT solver. If $F^{(i)}_0$ is satisfiable, set $a_i = 0$ and replace $F^{(i+1)}$ by a satisfiable instance of $F^{(i)}_0$. If $F^{(i)}_0$ is unsatisfiable, set $a_i = 1$ and replace $F^{(i+1)}$ by a satisfiable instance of $F^{(i)}_1$.
The construction produces an assignment $a_1 a_2 \ldots a_n$.
Correctness follows from the maintained condition that after choosing $a_1,\ldots,a_i$, the formula $F^{(i+1)}$ remains satisfiable whenever the original formula $F$ is satisfiable and the prefix $a_1\ldots a_i$ is extendable to a full solution. At step $i$, if $F^{(i)}_0$ is satisfiable, then some satisfying assignment of $F$ extends the prefix with $x_i=0$, and choosing $0$ preserves extendability. If $F^{(i)}_0$ is unsatisfiable, no satisfying assignment of $F$ can extend the current prefix with $x_i=0$, hence every satisfying assignment consistent with the prefix must have $x_i=1$, so setting $a_i=1$ preserves extendability.
At termination, the produced assignment satisfies $F$ because each step preserves satisfiability of the restricted formula down to $F^{(n+1)}$. It is lexicographically smallest because at each position $i$, the value $0$ is chosen whenever it is compatible with any full satisfying extension of the previously fixed prefix, and $1$ is chosen only when $0$ is impossible. Hence no satisfying assignment can have a smaller prefix at the first position of disagreement.
This completes the construction. ∎