I’ve been building a SAT solver on-and-off for a while, mostly to understand how they work under the hood, but also because I’ve been curious about applications of SAT solving to math problems.

Satisfiability basics #

The problem is to determine whether a given propositional formula (containing ands $\land$, ors $\lor$, and nots $\lnot$) can be satisfied by assigning booleans to its variables.

For example, the formula $$(x \lor y) \land (\lnot x \lor z)$$ can be satisfied by setting $(x, y, z) = (\text{true}, \text{false}, \text{true})$ You can verify this by substituting back into the formula and checking that it evaluates to true.

As another example, $$ (\lnot x \lor y) \land (\lnot y \lor z) \land (\lnot z) \land (x \lor y \lor z) $$ cannot be satisfied by any assignment to $x, y, z$. You can verify this by exhaustively checking all possible assignments, or by using logical inference.

There are many algorithms for doing this, with all kinds of accompanying heuristics:

• DPLL: a basic backtracking search with some optimizations that come from restricting/converting the input formula to CNF (conjunctive normal form)
• CDCL: extends DPLL with a way to learn new clauses from bad guesses and dynamically add them to the formula
• Cube-and-conquer: a divide-and-conquer approach that branches on a subset of variables and calls several CDCL solvers in parallel, often with shared access to learned clauses

A common theme with SAT is that if a formula is found to have a solution, it’s very easy to verify by simply substituting the assignment back into the formula. But if no solution exists, the solver needs to provide a proof of unsatisfiability, which is a trace of logical deductions that can be exponentially large.

Decision Procedures by Kröning and Strichman is a nice introduction to this topic, as well as SMT solving in several theories for various applications.

Problems in Ramsey theory #

(I presented this as part of CS 576 Formalized Mathematics.)

The boolean Pythagorean triples problem asks for the smallest number $S$ such that if you take the numbers ${1, \ldots, S}$ and color them with two colors, there will always be a triplet of numbers $x, y, z$ with the same color such that $x^2 + y^2 = z^2$.

Related are the Schur numbers $S(c)$, which are the smallest numbers $S$ such that any coloring of ${1, \ldots, S}$ with $c$ colors guarantees a triplet of numbers $x, y, z$ with the same color such that $x + y = z$.

Both of these problems can be represented as boolean formulas depending on $S$, where the formula is satisfiable (i.e. a coloring exists without a monochromatic triplet) for all values of $S$ up to a certain threshold, and unsatisfiable for all values of $S$ above that threshold.

For the Pythagorean triples case, the encoding looks like assigning each number $i \in \{1, \ldots, S\}$ a boolean variable $x_i$ representing its color (e.g. true for red and false for blue). Then, for every Pythagorean triple (e.g. $(3,4,5)$), we add a constraint like this: $$ (x_3 \lor x_4 \lor x_5) \land (\lnot x_3 \lor \lnot x_4 \lor \lnot x_5) $$ In words, at least one of the three variables must be true, and at least one must be false. This is equivalent to asserting that all three variables cannot have the same color. The final formula is the conjunction (“and”, $\land$) of all these constraints.

The encoding for the Schur numbers is similar, but since we can have more than two colors, we need more boolean variables per number to represent each possible color.

To actually “solve” the problem, we increment $S$, finding satisfying assignments for each one until we find one that is unsatisfiable (and return the ensuing proof). These proofs are massive:

• 200 terabytes for the boolean Pythagorean triple problem.
• 2 petabytes for the Schur number $S(5)$.

Variants of the Collatz conjecture #

The famously unsolved Collatz conjecture states that for any positive integer $n$, the sequence $$n \to \frac{n}{2} \text{ if } n \text{ is even}, \quad n \to 3n + 1 \text{ if } n \text{ is odd}$$ will eventually reach 1.

This is a little more complicated, since the exact problem can’t be expressed as a simple boolean formula. Instead, the approach goes like this:

First, reframe the Collatz function (or a variant) as a set of rewrite rules that can be applied to the front of a string of characters. The goal is now to prove that it’s impossible to apply infinitely many rewrites to any start string.

Then, reinterpret the characters in those strings as monotonically increasing functions over some set with a well-founded order, and strings as compositions of their characters’ functions.

Now, through clever math, it suffices to show that every rewrite rule (which used to be from string to string, but is now from function-composition to function-composition) has its output strictly smaller than its input.

• The point is that an infinite sequence of rule applications corresponds to an impossible infinite descent (because of the well-founded order), thus proving termination.

Let these functions be affine functions on $d$-dimensional vectors with a defined well-founded order. The goal is to now solve for the coefficients in these functions, which we bound by a “width” $n$.

• Note that this is where we lose completeness; a proof that comes out of this process will be correct, but we may be unable to prove certain statements (like the real Collatz conjecture; this paper only proves variants of it). We can increase $d$ and $n$, but only to a certain extent before the search space becomes intractable.

Finally, encode the aforementioned rewrite rule constraints as a boolean formula and solve.

The paper is here; this write-up captures my understanding so far and I intend to revisit it.