Suppose you are planning a holiday party for three dear friends: Alice, Bob and Carol. Bob and Carol are a couple, so you can either invite both of them or neither. Alice and Carol had a falling-out, so they cannot both come. And a party with just one guest could get awkward, so you want at least two guests. Who do you invite?

In this case, the only guest list that works is Bob and Carol — unfortunately, Alice can't come. To soften the news, you explain to Alice that it's nothing personal, just logic: "You see, if a, b and c are true/false variables for whether you (Alice), Bob and Carol attend my party, I need to choose a guest list in a way that satisfies this Boolean formula":

$$\underbrace{\rule[-0.4em]{0pt}{0.4em}(\lnot b \lor c) \land (b \lor \lnot c)}_{\text{Bob and Carol: both or neither}} \land \underbrace{\rule[-0.4em]{0pt}{0.4em}(\lnot a \lor \lnot c)}_{\text{not both Alice and Carol}} \land \underbrace{\rule[-0.4em]{0pt}{0.4em}(a \lor b) \land (a \lor c) \land (b \lor c)}_{\text{at least two guests}}$$

Alice's frown slowly gives way to a look of understanding. "Of course, it's just logic. You can't satisfy all those rules if I attend."

This guest-list puzzle is an instance of the Boolean Satisfiability (SAT) problem: given a Boolean formula, meaning a list of AND/OR/NOT constraints on true/false variables, is there an assignment to the variables that makes the formula true? Such an assignment is said to satisfy the formula.

It was easy to solve this SAT instance with only three friends (Boolean variables) by simply checking all eight possible guest lists. But perhaps by next year's party, your social circle has grown to 1000 friends. You are now faced with a tougher SAT problem: you don't have time to check all $2^{1000}$ possible guest lists. Is there a cleverer way? In theory, no: SAT is the canonical example of an NP-complete problem, so we expect that no algorithm can solve it efficiently for every Boolean formula.

In practice, we see something very different: SAT solvers are typically extremely fast on instances that arise in real-life applications, and routinely handle problems with millions of variables. A 1000-friend guest-list problem would, in most cases, take just a fraction of a second to solve. As a result of this efficiency, SAT solvers are used extensively in both hardware and software verification, as tools for proving the correctness of chip designs and code.

However, as the NP-completeness of SAT predicts, there are certain kinds of problems where SAT solvers perform poorly. A classic example comes from the pigeonhole principle: one can write a Boolean formula asserting that there exists a placement of $n+1$ pigeons into $n$ pigeonholes where no two pigeons share a pigeonhole. Although we can see from this description that this formula must be unsatisfiable, determining this with a modern SAT solver is already infeasible at just 20 pigeons (~400 variables).

A well-known framework for explaining poor SAT solver performance comes from proof complexity, a subfield of theoretical computer science studying the size of proofs. It turns out that state-of-the-art SAT solvers work by implicitly constructing a specific kind of proof known as a resolution proof. These are proofs using only a single proof rule called the resolution rule, shown below.

In 1985, Haken proved that the size of any resolution proof for the pigeonhole principle must scale exponentially in the number of pigeons. Therefore, SAT solvers require exponential time to construct these proofs and determine that a pigeonhole formula is unsatisfiable. In this way, proof complexity lower bounds can expose and explain the fundamental limitations of the underlying SAT solving algorithm.

Multiplication

SAT solvers struggle with another class of formulas that is closer to practice: those involving fixed-width integer multiplication. A wide variety of such formulas arises in software verification, whenever one is verifying programs that multiply integers. For example, consider the following implementation and specification of a multiplication overflow guard:

We can write down the following bit-vector formula asserting that there exist inputs x and y for which the code does not follow the specification:

(set-logic QF_BV)
(declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 32))

; mul_overflows code:
(define-const z (_ BitVec 32) (bvmul x y))
(define-const b Bool (and (not (= x #x00000000)) (not (= (bvudiv z x) y))))

; specification:
(define-const xy (_ BitVec 64) (bvmul ((_ zero_extend 32) x) ((_ zero_extend 32) y)))
(define-const spec Bool (bvuge xy #x0000000100000000))

; assert counterexample to specification
(assert (not (= b spec)))

(check-sat)

To verify the correctness of mul_overflows, we can feed this formula into a bit-vector solver and check that it outputs UNSAT, which indicates that there are no counterexamples to the specification. Internally, most bit-vector solvers translate this bit-vector formula into a SAT formula in a process known as bit-blasting. The solver then feeds this SAT formula into a SAT solver to get the final answer. As we said earlier, SAT solvers scale poorly on formulas involving multiplication, and this example is no exception: as the table below shows, although state-of-the-art bit-vector solvers can verify the 16-bit version of mul_overflows in seconds, they time out after three hours on the 32-bit instance shown above.

This weakness came into focus during several talks and workshops around 2015. Practitioners found that although SAT solvers were generally effective at solving large, complicated formulas involving bitwise operations and fixed-width addition, they were not capable of reasoning about even simple properties of multiplication. Key examples came from the algebraic properties of multiplication: commutativity, distributivity and associativity. In 2016, Biere reported that no known technique could prove these properties of $n$-bit multiplication beyond $n = 16$.

Unlike with pigeonhole formulas, we did not have any theoretical explanation for the difficulty of multiplication; for over a decade the problem of showing a super-polynomial lower bound on resolution proof size, for any natural formula containing multiplication, remained open. (In a surprising turn of events, Beame and Liew actually found polynomial-size resolution proofs for commutativity and distributivity of multiplication, albeit of impractical size.)

Our main result gives the first lower bound of this kind.

Main Theorem (informal): Resolution proofs of the associativity of $n$-bit multiplication have size at least $2^{\Omega((n/\log n)^{1/4})}$.

Encoding associativity

Bit-vector solvers typically encode multiplication using a Boolean circuit that performs the grade-school multiplication algorithm. This circuit computes partial products, which are ANDs of each pair of input bits, and then sums the partial products to get the output bits. The diagram below illustrates an example of a 4-bit multiplication circuit.

Once we have fixed a multiplier circuit, we can write a formula $\mathrm{Assoc}_n$ asserting that there exist inputs $x, y, z$ such that $x(yz) \neq (xy)z$. The structure of $\mathrm{Assoc}_n$ is shown below.

If a SAT solver determines that the formula $\mathrm{Assoc}_n$ is unsatisfiable, then it has proven that the multiplier circuit is associative: for all $x, y, z$ we have $x(yz) = (xy)z$.

Key ideas

The key idea of the proof is to reduce from another class of formulas that encode perfect matching constraints on a bipartite graph. Given a graph, the corresponding perfect matching constraints assert that we can select a subset of the graph's edges so that each node is incident to exactly one selected edge. If the bipartite graph is unbalanced, meaning that its two parts have different numbers of nodes, then no selection of edges can satisfy these constraints. Hence, the perfect matching constraints are unsatisfiable on such a graph.

We choose a family of unbalanced bipartite graphs whose perfect matching formulas require exponentially large resolution proofs. It turns out that by carefully setting some of the bits of the inputs $x, y, z$ to the constants 0 or 1, we can embed a perfect matching formula inside the $\mathrm{Assoc}_n$ instance. This is a reduction: since these perfect matching formulas require large proofs, so does $\mathrm{Assoc}_n$.

Using the inner multipliers $xy$ and $yz$ to enforce perfect matching

We now give an idea of how we get the inner multipliers to enforce the perfect matching constraints. The reduction also needs to consider other details, such as what happens in the outer multipliers computing $x(yz)$ and $(xy)z$, but those are out of scope for this blog post.

Given a bipartite graph, we will set the bits of $x, y, z$ in a way similar to the diagram below (the real construction would need 28-bit vectors). The unset bits of $y$ represent edges of the graph. In our example, $y_4=1$ means that edge $e_1$ is selected for the perfect matching.

The main thing to notice is that $x, y, z$ are sparse. In the diagram above, the only nonzero entries occur at indices that are multiples of 4. So in the multipliers $xy$ and $yz$, the only nonzero partial products occur at column indices that are multiples of 4. Furthermore, none of these columns contains enough nonzero entries to add "carries" to the next multiple-of-4 column. So we can partition the columns of each multiplier into strips that each independently sum their partial products, as shown in the diagram below.

Now we need a bit of combinatorial magic. Let's focus on the multiplier $xy$, shown below. We define a map $\mathrm{col}_{xy}(v)$ that sends each right node $v$ of the bipartite graph to a unique multiple-of-4 column in the multiplier for $xy$. We carefully set the $x, y, z$ bits so that $\mathrm{col}_{xy}(v)$ contains exactly the edge variables incident to the node $v$ (recall that we think of each unset $y$ variable as an edge variable). The strip of 4 columns at $\mathrm{col}_{xy}(v)$ must output the count of these edge variables in binary. So if we set the outputs of this strip to 0001, then the multiplier circuit for $xy$ enforces the constraint "exactly one edge incident to $v$ is selected". This is exactly what the perfect matching constraints enforce for this node $v$!

Similarly, the perfect matching constraints for each left node $u$ are enforced by the other multiplier circuit for $yz$, as illustrated below.

Conclusion

This result is a first step toward a theoretical understanding of why SAT solvers struggle with multiplication. We now have an explanation when associativity of multiplication is involved: the underlying resolution proofs are exponentially large.

Beyond the lower bound itself, our reduction uncovers a connection between two seemingly unrelated principles: the associativity of grade-school multiplication and perfect matching in bipartite graphs.

But many directions remain open. For example, we saw that solvers have trouble with mul_overflows: can we show that it requires exponentially large proofs? Can we prove lower bounds for a more general class of multiplication problems?

For further reading, check out the arXiv paper and the supplementary material in the GitHub repository.