The Assembly Language of Satisfiability

Recently there has been a some discussion about how much practical use is seen by certain methods coming out of academia, especially those methods for which a wide practical applicability is often claimed. Among these are techniques are SAT solvers, which I quite like and with which I am also somewhat familiar. This lead to questions about how to make SAT solvers easier to use. In this post I will give my personal perspective on that question.

The discussion started with Jeremy Kun’s post on Twitter, where he asked for concrete examples where SAT solvers are used in practice. He wrote about the responses in his newsletter and while he concedes that SAT solvers are more widely used than he initially thought, for some of the examples people responded with, he remains skeptical towards whether they really are as widely used as claimed.

While I don’t want to go into how widely used SAT solvers are on an absolute scale, I personally think that SAT solvers, or rather methods based on SAT solvers, have the potential to be used much more widely than they currently are. This raises the question: what is stopping the industry from making more use of SAT solvers wherever applicable?

Are We Bad at SAT Solvers?

In his latest newsletter titled “We’re Bad at SAT Solvers”¹, Hillel Wayne argues that this is a problem of usability. SAT solvers require the input problem to be a propositional logic formula in conjunctive normal form (CNF). Apart from a few rare exception, this is not a natural way to express most problems which we want to solve using a SAT solver. Even worse, as Hillel notes, translating problems into equivalent CNF formulas is not a straightforward process. For a single given problem, there are often many different ways to do this. Selecting a good approach often requires a lot of experience, some knowledge of SAT solver internals and running careful experiments. Additionally, experience in encoding one problem domain into CNF might not translate to the problems of a different domain.

Even for seemingly simple constraints which are part of many problems, like counting the number of set Boolean variables, there is a vast amount of literature, including recent publications, detailing different trade-offs that can be made. These trade-offs are also not just an academic concern, but can make the difference between solving a problems in seconds or giving up after running the solver for days. Many practical problems will contain different kinds of constraints and expecting users to be familiar with the corresponding literature for each of them is certainly a barrier for wide scale adoption.

Making SAT Solvers Easier to Use

In his newsletter Hillel then wonders what it would take to make them more useful to the industry. He does mention that the related SMT solvers seem to be doing much better in this regard, and consequently have a lot more users than SAT solvers. SMT solvers are similar to SAT solvers, but allow much more freedom in the way the input problem can be expressed. You are not limited to Boolean variables, but also have integers, fixed-width integers, arrays and other datatypes (depending on which SMT solver you use), you have many common operations on those types and you don’t have to get your problem into a specific normal form. All that often comes with an API that allows you to manipulate the input formula as an abstract syntax tree, which you can inspect at any time.

I think the observation that SMT solvers are much easier to use than SAT solvers is an important observation. At the same time, I think it also answers his question on how an easier to use SAT solver would look like: you would get an SMT solver.

So why are SAT solver authors not trying to lift some of the input restrictions like requiring CNF? Or if SMT solvers work just as well as SAT solvers, why are people still working on those hard to use SAT solvers?

To answer these questions we need to have a very high-level look at how SMT solvers work. This will also allow us to understand why people working on SAT solvers tend to implicitly count all applications of SMT solvers when talking about applications of SAT.

How do SMT Solvers Work?

For SMT solvers there are two general approaches which dominate the landscape: bit-blasting and CDCL(T). Often solvers combine these or add additional techniques on top of this, but those two techniques form the backbone of any SMT solver I’m aware of.

Bit-Blasting

Bit-blasting describes the process of taking the input formula and directly encoding it into an equivalent Boolean formula in CNF, which can then be solved by a SAT solver. This process is limited to formulas where every data type has a finite set of values, as otherwise there is no direct way to encode each variable using a finite set of Boolean variables. Luckily, a lot of software makes use of fixed-width integers, so bit-blasting is often very effective for problems that come from all kinds of software analysis.

I’m aware of two SMT solvers that use bit-blasting as their main strategy, Boolector and STP, both having won several awards at solver competitions. Both of them also use stand-alone SAT solvers to solve the encoded CNF formula. Boolector offers the choice between CaDiCaL, CryptoMiniSat, Lingeling, Minisat and Picosat, of which CryptoMiniSat and Minisat are also offered by STP.

For bit-blasting this makes clear that we need a SAT solver as backend and that any improvement to SAT solving also translates into a corresponding improvement to SMT solvers based on this approach. They can be accurately described as additional tooling around a SAT solver, that makes it easier to use and easier to apply to a wider area of problems. This way only the authors of the SMT solver need to be aware of all the techniques for encoding problems into CNF, lifting that burden from the users.

CDCL(T)

The other approach, CDCL(T), is slightly more complicated, but also more flexible, as it can handle input problems with variables that have an infinite domain. In common with bit-blasting though, is that it is again based around a SAT solver. The CDCL stands for conflict driven clause learning, which is the algorithm employed by most modern SAT solvers², and the T stands for the extension with certain so-called theories. A theory here is just a collection of supported non-Boolean datatypes and operations which are also allowed in the input formula.

To work around this in CDCL(T) we construct a Boolean formula which is a sound over-approximation of the input formula. I’m going to gloss over a lot of details, but essentially we can do this by replacing any subterm of the formula that we cannot encode by an unconstrained variable. This formula can then be solved by a SAT solver. If the solver declares the formula unsatisfiable, we know that our input problem is also unsatisfiable because our approximation can only make it easier to satisfy. If the SAT solver produces a Boolean solution to our approximated problem, we then need to check whether we can extend it to a solution to the input problem. This is done using so-called theory solvers, which handle the non-Boolean datatypes and operations. If they are able to extend the solution to satisfy the input problem, we are done, otherwise the theory solvers produce some data which allows us to refine our Boolean over-approximation in such a way that it better approximates the input formula. Then the process is repeated until either the SAT solver decides the problem to be unsatisfiable or until the theory solvers produce a solution.

As far as I’m aware³, most CDCL(T) solvers come with their own SAT solver, which is tightly integrated to make the interaction between theory solvers and the SAT solver as efficient as possible. Still those integrated SAT solvers use the same techniques, the same data structures and the same algorithms as stand-alone SAT solvers. Any improvement made to stand-alone SAT solvers will find its way into integrated SAT solvers and vice versa.

There are too many solvers based on this approach to list them all here, but examples are Z3, which seems to be the most popular, or CVC4 which has won many awards at solver competitions.

CNF as Assembly Language

This high-level description might leave you with the impression that SMT solvers are mostly thin wrappers around a SAT solver. This would be far from the truth. In my description I simply focused on the part where SAT solvers are used. Overall I think a SAT solver is a significant part of a state-of-the-art SMT solver, but the majority of necessary complexity lies elsewhere, especially for CDCL(T) based solvers.

I think a good analogy of the relationship between the interface offered by SAT solvers and SMT solvers is that of assembly language and high level languages. Here Boolean CNF formulas correspond to a universal assembly language that is supported by different SAT solver implementations, much like you can get CPUs that run the same instruction set from different vendors. Keeping this layer as simple and minimal as possible, even if that complicates manual use, helps a lot with making different implementations compatible. This in turn leads to increased competition between solvers, which I think played an important part in the improvements we’ve seen over the years.

SMT solvers then allow you to effectively use a SAT solver without having to be an expert in CNF encoding. They give you a much easier to use input language and at the same time free you from making a lot of low-level decisions that would require expert knowledge about SAT solvers. This is very much like compilers allow you to use high level languages while freeing you from having to worry about details like e.g. instruction scheduling or register allocation. Also these days no one would call a modern compiler a thin wrapper that produces assembly code (I hope!).

The analogy even extends a bit further: Sometimes for specific problems that could be solved with an SMT solver, an expert might find a better way to manually encode the problem into CNF, gaining extra performance. With further improvements to SMT solvers, I think in the future this could very well take the same place as manually coding routines in assembly now: mostly reserved for a few specific use cases where a lot of additional implementation and maintenance work is worth the potential increase in performance.