Donald Knuth Talks Satisfiability and Combinatorics

By James Case

Donald Knuth, professor emeritus in the Department of Computer Science at Stanford University, delivered the John von Neumann Lecture at the 2016 SIAM Annual Meeting, held in Boston this July. Perhaps best known for his invention of the T_EX and METAFONT systems for computer typesetting, Knuth has enjoyed a long and fruitful research career while composing a multi-volume treatise on The Art of Computer Programming. Much of his lecture was drawn from Volume 4, Fascicle 6 of that still-emerging series. 

Knuth spoke about the satisfiability of Boolean formulae \(F(x_1,..., x_n)\), expressed as collections of OR clauses separated by ANDs in what is often described as “conjunctive normal form.” Is it possible to assign values from the set \({0,1}\) to the variables \((x_1,..., x_n)\) in such a way that \(F(x_1,..., x_n) = 1\)? Due to its growing importance, the problem has come to be known as SAT. If \(\wedge\) or \(\vee\) denote AND and OR respectively, if \(\bar{Q}\) denotes the complement of \(Q\)  in \({0,1}\), and if

\[F(x_1,x_2, x_3, x_4) = (x_1 \vee x_2 \vee \bar{x}_3) \wedge (x_2 \vee x_3 \vee \bar{x}_4) \wedge (x_3 \vee x_4 \vee x_1)\] \[ \wedge (x_4 \vee \bar{x}_1 \vee x_2) \wedge (\bar{x}_1 \vee \bar{x}_2 \vee x_3) \wedge (\bar{x}_2 \vee \bar{x}_3 \vee x_4) \wedge (\bar{x}_3 \vee \bar{x}_4 \vee \bar{x}_1), \]

one can easily verify that the assignment \((x_1,x_2, x_3, x_4) = (0, 1, \#, 1)\) satisfies \(F(x_1,x_2, x_3, x_4) = 1\), where \(\#\) may denote either \(0\) or \(1\). On the other hand, no such assignment satisfies \(G(x_1,x_2, x_3, x_4) = 1\) if \(G\) is the formula obtained by appending the clause \((\bar{x}_4 \vee x_1 \vee \bar{x}_2)\) to \(F\). Finally, because \(G\) is invariant under the cyclic permutation \(x_1 \rightarrow x_2 \rightarrow x_3 \rightarrow x_4\rightarrow \bar{x}_1 \rightarrow \bar{x}_2 \rightarrow \bar{x}_3  \rightarrow \bar{x}_4 \rightarrow x_1\), the omission of any clause in \(G\) yields a problem equivalent to the satisfiability of \(F\). For this and other reasons, the Boolean formula \(G\) is well known to computer scientists. 

Applying De Morgan’s laws to a formula \(F\) in conjunctive normal form yields a formula \(\bar{F}\) in “disjunctive normal form,” consisting of a collection of AND clauses separated by ORs. So \(F\) is unsatisfiable if and only if \(F(x_1,..., x_n) \equiv 0\), which happens if and only if \(\bar{F}(x_1,..., x_n) \equiv 1\). And since a formula identically equal to \(1\) is called a tautology, one may conclude that a given formula \(F\) is satisfiable unless \(\bar{F}\)  is a tautology.

SAT solvers are algorithms for discovering satisfactory Boolean assignments – or proving that none exist. Such solvers are of growing practical importance, in part because a host of significant combinatorial problems can be reduced to SAT problems, and in part because highly-effective SAT solvers (capable of handling “industrial strength” problems with millions of variables) have suddenly and unexpectedly become available. After all, a polynomial algorithm capable of deciding whether or not a given Boolean formula \(F\) is satisfiable would confirm that \(P = NP!\)

Employing the notation kSAT conveniently indicates that a particular Boolean formula consists of clauses containing no more than \(k\) variables. One can show that every SAT problem is logically equivalent to a 3SAT problem whose “size” is polynomial in the size of the original.

Knuth used the early part of his lecture to exhibit a variety of problems, including several about map coloring, reducible to SAT problems. Among the latter were the McGregor map of order ten (see Figure 1) and an ordinary \(8 \times 8\) chessboard, colored in such a way that any two squares separated by a queen’s move are the same color.

Questions concerning John Horton Conway’s famous Game of Life can be similarly resolved. The game is played on a succession of rectangular grids, and each cell is colored either black or white by a solitary player who cannot deviate from the following two-rule strategy:

(i)  A black cell shall remain black if and only if either two or three of its eight neighboring cells are currently black
(ii) A white cell shall become black if and only if three of its eight neighbors are currently black.

Knuth displayed initial configurations, all found by SAT solvers, of black and white cells on a \(7 \times 15\) grid that spell out the word LIFE in block letters five cells high after one, two, or three player moves. He also presented several pairs of configurations in which designated cells alternate between black and white on successive moves (see Figure 2). Finally, he exhibited a configuration known as a “Garden of Eden,” which has no predecessor within the game.

To educate himself about SAT solvers, Knuth began building his own several years ago. He has since built at least a dozen of them, each more sophisticated than the last. During his talk, Knuth displayed a progression of these solvers, labeled SAT0 through SAT13. All accept input clauses in the following format,

\[ \begin{array}{ccc} x2 \qquad & x3 \qquad & \sim x4 \\
x1 \qquad & x2 \qquad & x4 \\ \sim x1 \qquad & x2 \qquad & x4 \\ \sim x1 \qquad & \sim x2 \qquad & x3 \\ \sim x2 \qquad & \sim x3 \qquad & x4 \\ \sim x1 \qquad & \sim x3 \qquad & \sim x4 \\ x1 \qquad & \sim x2 \qquad & \sim x4 \\ x1 \qquad & \sim x2 \qquad & x4 \\ x1 \qquad & x2 \qquad & x3, \end{array} \]

corresponding to Ronald Rivest’s well-known formula \(G(x_1,x_2, x_3, x_4)\). Knuth’s solvers all return YES or NO answers, along with a satisfactory \(0/1\) vector if any such exist. It is important to note, when comparing results, that many authors require their algorithms to return all possible satisfactory vectors.

A brute-force SAT solver would construct and search a binary tree with \(2^n - 1\) branch nodes and \(2^n\) leaf nodes, in which all paths from root to leaf are of length \(n\). Each leaf node must be labeled either \(F=0\) or \(F=1\), depending on whether the formula \(F\) is satisfied by the \(0/1\) values labeling the edges of the path from root to leaf.

Backtracking methods seek to guess a partial solution to the problem by assigning \(0/1\) values to a subset of the variables \(x_1,..., x_n\), and testing the hypothesis that those values are correct by extending the partial solution to a complete one. Success confirms the hypothesis while failure rejects it, indicating only that the initial guess was wrong and another must be made. Therein lies the rub, for there are \(C^k_n\) \(k\)-subsets of \(N = {1,...,n}\), and \(2^k\) ways of assigning \(0/1\) values to a \(k\)-subset of the \(n\) problem variables.

It can be obvious which subsets to choose and which values to assign. If a single variable \(x_i\) appears in every clause, the set \({x_i}\) and value \(x_i = 1\) are clear choices. Or if \(x_i\) appears in “almost all” of the clauses, then the previous guess still seems appropriate. The choice \(x_i = 1\) then eliminates (i.e. satisfies) all but a few of the clauses, and \(\bar{x}_i\) may be stricken from those that remain, leaving behind a greatly-reduced SAT problem. There is, of course, no guarantee that the latter will prove solvable, but its solvability remains a natural hypothesis to explore. Advanced SAT solvers employ a variety of strategies—some of them are quite elaborate—when deciding which subsets to choose and what values to assign.

Knuth referenced a 1982 paper [1] that presented empirical evidence indicating that \(0\)-level algorithms outperform \(1\)-level algorithms on fairly small problems, while \(1\)-level algorithms excel both \(0\)-level and \(2\)-level algorithms on slightly larger problems. The same two authors had previously obtained asymptotic estimates indicating that truly large problems will require higher-level algorithms. As matters stand, art rather than science indicates which algorithms are most appropriately applied to which problems.

Having exercised several of his SAT solvers on the following puzzle: Find a binary sequence \(x_1,..., x_8\) containing no three equally-spaced \(0\)s and no three equally-spaced \(1\)s, Knuth illustrated a number of the results with rows of red and blue balls rather than \(0\)s and \(1\)s. There are six admissible sequences, none of which is extendable to an admissible sequence of length 9. This is a special case of the general fact that, given any two positive integers \(i\) and \(j\), along with sufficiently-large \(n\), every binary sequence \(x_1,..., x_n\) must contain exactly \(i\) equally-spaced \(0\)s and exactly \(j\) equally-spaced \(1\)s. The smallest such \(n\) is denoted \(W(i,j)\) in honor of B. L. van der Waerden, who proved an even more general result. Despite the best efforts of current SAT solvers, relatively little is known about the numbers \(W(i,j)\).

The most promising SAT solving applications appear to lie in the fields of hardware and software verification. One can usually represent a typical design as a relation \(R\) on \(S \times S\), where \(S\) denotes a set of admissible “state vectors” \(X=(x_1,..., x_n)\) and \(X'\) is a possible successor of \(X\) if and only if \((X,X') \in R\). Thus, a sequence \(X_0 \rightarrow X_1 \rightarrow \dotsb \rightarrow X_\omega\) is possible if and only if \((X_0, X_1) \in R \enspace\& \enspace (X_1, X_2) \in R \enspace\&\enspace...\enspace\& \enspace(X_{\omega-1}, X_\omega) \in R\). One would like to know, for instance, if there are any sequences in which \(X_0\) and \(X_\omega\)

In the last part of his lecture, Knuth displayed a series of eye-catching illustrations (see Figure 3) dramatizing the complexity of the problems that current SAT solvers are able to resolve. In some of his images, differently-colored connectors indicate the number of clauses containing both connected variables. Such information is invaluable to backtrackers deciding which sets to try and what values to assign.

The lecture was well attended, and not surprisingly, the audience seemed quite spellbound by the progress Knuth reported.

References
[1] Brown, C.A., & Purdom, P.W. (1982, May). An Empirical Comparison of Backtracking Algorithms. IEEE Transactions on Pattern Analysis and Machine Intelligence, 4(3), 309-316.

[2] Knuth, D.E. (2015). The Art of Computer Programming. (Vol. 4, Fascicle 6: Satisfiability). Boston, MA: Addison-Wesley. 

James Case writes from Baltimore, Maryland.