jix.one

Introducing Varisat

Posted on May 20th 2018, tagged rust, sat

I’ve been interested in SAT solvers for quite some time. These are programs that take a boolean formula and either find a variable assignment that makes the formula true or find a proof that this is impossible. As many difficult problems can be rephrased as the satisfiability of a suitable boolean formula, SAT solvers are incredibly versatile und useful. I’ve recently finished and now released a first version of my SAT solver, Varisat, on crates.io.

Most modern state of the art SAT solvers are based on the conflict driven clause learning (CDCL) algorithm. With some handwaving this algorithm could be seen as a clever combination of recursive search, backtracking, resolution and local search.

The CDCL algorithm uses a lot of heuristics and can be extended in many ways. This is where different CDCL based solvers take different approaches and where a lot of active research happens.

A few years ago I decided to write my own CDCL based SAT solver. I wanted to get an in depth understanding of the CDCL algorithm and also have a code base I’m familiar with so I can easily experiment with new ideas. I started writing several prototypes. First I used C++ and later I switched to Rust. Earlier this year I decided that my current prototype was good enough to turn into a complete, usable solver. Just in time to enter this year’s SAT competition.

As varisat is in an early stage of development, implementing little beyond the minimum required for a modern CDCL based SAT solver, I don’t expect it to win any prizes in the competition. There are many problem instances that benefit a lot of additional techniques that varisat just doesn’t offer yet. Nevertheless I was pleasently surprised to find that it already is competitive for some graph coloring instances I needed to solve in the meantime.

Besides turning varisat into a library (command line only for now), I plan to incrementally add more and more of the proven techniques used by state of the art solvers. I also want to try some of my ideas for novel techniques and hope to find the time to write more about working on varisat.