Jix' Site


Refactoring Varisat 5: Incremental Solving and Proofs

This is the fifth and final post in my series about refactoring varisat. In the last post varisat gained the heuristics needed to solve some non-trivial instances. In this post we’ll add incremental solving and proof generation. This brings varisat to feature parity with the old version.

Incremental solving enables new use cases that just aren’t feasible with batch solving. Building SMT solvers on top of a SAT solver or techniques like symbolic execution often generate a vast amount of related SAT solver queries. Starting a new solving process for each query would result in a lot of repeated work. Incremental solving avoids some of this.

Proof generation makes it possible to independently check the work performed by a SAT solver. State of the art SAT solvers have a large codebase where it’s easy for a bug to hide. When the SAT solver finds a solution it is easy to tell whether it satisfies the input formula. For the unsatisfiable case, without proof generation, we have to trust the solver to be free of bugs. As solvers tend to have bugs from time to time, the yearly SAT competition started to require proof generation a few years ago.

Being able to generate proofs isn’t only helpful for uses who want to have better assurance of the solver’s correctness, it’s also great for finding and analyzing bugs.

[Read More]

Refactoring Varisat: 4. Heuristics

This is the fourth post in my series about refactoring varisat. In the last post we saw how conflict driven clause learning works, in this post we’re going to make it fast. To get there we add several smaller features that were already present in varisat 0.1. While there are still some things missing that varisat 0.1 supports, these are features like proof generation or incremental solving that don’t affect the solving performance.

This means you can solve some non-trivial instances using varisat 0.2 today. I haven’t made a new release on crates.io yet, but you can install it directly from github (replacing any previous version installed):

cargo install --force --git https://github.com/jix/varisat
varisat some_non_trivial_input_formula.cnf

One part of making the solver faster were low-level optimizations in the unit-propagation implementation. I won’t go into the details of that, but you can look at the new code. The bigger part were several heuristics that play a big role in making CDCL perform well. Below I will explain each implemented in varisat so far.

[Read More]

Refactoring Varisat: 3. Conflict Driven Clause Learning

This is the third post in my series about refactoring varisat. In this post the new code base turns into a working SAT solver. While you can use the command line tool or the library to solve some small and easy SAT problems now, there is still a lot ahead to gain feature and performance parity with varisat 0.1.

In the last post we saw how unit propagation is implemented. When some variables are known, unit propagation allows us to derive the values of new variables or finds a clause that cannot be satisfied. Unit propagation alone isn’t enough though, as there is no guarantee to make progress. To continue the search for a satisfying solution after propagating all assignments, it is necessary to make a guess. A natural way to handle this would be recursion and backtracking. This would give us a variant of the DPLL algorithm from which conflict driven clause learning evolved.

[Read More]

Refactoring Varisat: 2. Clause Storage and Unit Propagation

This is the second post in my series about refactoring varisat. Since the last post I started implementing some of the core data structures and algorithms of a CDCL based SAT solver: clause storage and unit propagation. In this post I will explain how the these parts work and the rationale behind some of the decisions I made.

[Read More]

Refactoring Varisat: 1. Basics and Parsing

This is the first post in a series of posts I plan to write while refactoring my SAT solver varisat. In the progress of developing varisat into a SAT solver that can compete with some well known SAT solvers like minisat or glucose, it accumulated quite a bit of technical debt. Varisat is the first larger project I’ve written in rust and there a lot of things I’d do differently now. Before I can turn varisat into a solver that competes with the fastest solvers out there, I need to do some refactoring.

[Read More]