TAOCP 7.2.2.2 Exercise 109
Let $S(F)$ denote a SAT solver applied to a formula $F$.
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: 1m34s
Solution
Let $S(F)$ denote a SAT solver applied to a formula $F$. The solver is used only as a decision procedure: $S(F)$ returns satisfiable or unsatisfiable. The variables are considered in the order $x_1,x_2,\ldots,x_n$, and the lexicographic order is the order induced by $0<1$ on the binary strings $x_1\ldots x_n$.
The first question is whether the original formula $F$ is satisfiable. If $S(F)$ reports unsatisfiable, there is no solution. Otherwise, we determine the variables one at a time. For $i=1,2,\ldots,n$, suppose that values have already been fixed for $x_1,\ldots,x_{i-1}$ and that the remaining formula has at least one satisfying assignment. Try to force the smaller possible value $x_i=0$ by adding the unit clause $\bar{x}_i$ to the current formula. If the resulting formula is satisfiable, keep this choice. If the resulting formula is unsatisfiable, replace the trial value by $x_i=1$.
More explicitly, after choosing values $a_1,\ldots,a_{i-1}$, let
$$ F_{i-1}=F\land\bigwedge_{j=1}^{i-1}(x_j=a_j), $$
where $(x_j=0)$ represents the unit clause $\bar{x}_j$ and $(x_j=1)$ represents the unit clause $x_j$. At stage $i$, test
$$ F_{i-1}\land \bar{x}_i . $$
If this formula is satisfiable, define $a_i=0$ and set
$$ F_i=F_{i-1}\land\bar{x}_i . $$
If it is unsatisfiable, define $a_i=1$ and set
$$ F_i=F_{i-1}\land x_i . $$
The process terminates after $n$ stages and returns
$$ a_1a_2\cdots a_n . $$
To prove correctness, first consider the invariant that $F_i$ is satisfiable after every successful stage. Initially, $F_0=F$ is satisfiable by the first call to the SAT solver. At stage $i$, if $F_{i-1}\land\bar{x}i$ is satisfiable, the chosen value $a_i=0$ preserves satisfiability. If $F{i-1}\land\bar{x}i$ is unsatisfiable, every satisfying assignment of $F{i-1}$ must have $x_i=1$, because the only two possible values of a Boolean variable are $0$ and $1$. Therefore $F_{i-1}\land x_i$ is satisfiable, and the invariant is preserved.
The returned string is a satisfying assignment because $F_n$ is satisfiable and all variables have fixed values in $F_n$. The values chosen are lexicographically smallest because at each position $i$ the algorithm selects $x_i=0$ whenever any satisfying assignment with the already fixed prefix and with $x_i=0$ exists. If no such assignment exists, every satisfying assignment extending the current prefix must have $x_i=1$, so choosing $1$ cannot discard a lexicographically smaller solution. Applying this argument successively for $i=1,\ldots,n$ proves that no satisfying assignment precedes the returned one in lexicographic order.
The algorithm uses one initial SAT call and at most one additional SAT call for each variable, so the total number of SAT solver invocations is at most
$$ n+1 . $$
This gives the lexicographically smallest solution whenever the formula is satisfiable. If the initial call fails, the formula has no solution. ∎