Jix' Site

rust

Varisat 0.2.0 Released

After refactoring the complete code base in the last months, I’m excited to announce the release of Varisat 0.2.0. Varisat is a CDCL based SAT solver written in rust. Given a boolean formula in conjunctive normal form, it either finds a variable assignment that makes the formula true or finds a proof that this is impossible.

Varisat 0.2.0 is available as a rust library (varisat on crates.io) and as a command line solver (varisat-cli on crates.io).

If you want to get started check out the user manual and library API documentation. If you want to learn more about how Varisat works, you can read the blog posts about the development.

#rust #sat

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]

Introducing partial_ref

Recently there has been some discussion about interprocedural borrowing conflicts in rust. This is something I’ve been fighting with a lot, especially while working on my SAT solver varisat. Around the time Niko Matsakis published his blog post about this, I realized that the existing workarounds I’ve been using in varisat have become a maintenance nightmare. Making simple changes to the code required lots of changes in the boilerplate needed to thread various references to the places where they’re needed.

While I didn’t think that a new language feature to solve this would be something I’d be willing to wait for, I decided to sit down and figure out how such a language feature would have to look like. I knew that I wanted something that allows for partial borrows across function calls. I also prefer this to work with annotations instead of global inference. While trying to come up with a coherent design that fits neatly into the existing type and trait system, I realized that most of what I wanted can be realized in stable rust today.

Luckily some time ago I came across the frunk crate. From there I learned a trick that I’d call inference driven metaprogramming. Rust requires trait implementations to be unambiguously non-overlapping. The rules for this just consider the implementing type, not any bounds. The trick I’ve learned from frunk is to add an additional type parameter to the trait that would otherwise have overlapping implementations. That type parameter is only used to disambiguate the implementations. As long as there is only one implementation, but this time considering bounds, rust’s powerful type inference will infer that extra type parameter. An example would be frunk’s Plucker trait, where the Index type parameter selects between the otherwise overlapping instances.

Equipped with this, I was able to implement type-level borrow checking logic. Today I’ve released a first version of this. The documentation contains a small tutorial. I also documented the type-level borrow checking logic, as the involved types and traits will appear in error messages. While I tried to optimize for readable error messages, I think every trait and type that could be part of one should be documented.

Using the library looks like this (see the tutorial for an explanation):

use partial_ref::*;

part!(pub Neighbors: Vec<Vec<usize>>);
part!(pub Colors: Vec<usize>);
part!(pub Weights: Vec<f32>);

#[derive(PartialRefTarget, Default)]
pub struct Graph {
    #[part = "Neighbors"]
    pub neighbors: Vec<Vec<usize>>,
    #[part = "Colors"]
    pub colors: Vec<usize>,
    #[part = "Weights"]
    pub weights: Vec<f32>,
}

let mut g = Graph::default();
let mut g_ref = g.into_partial_ref_mut();

g_ref.part_mut(Colors).extend(&[0, 1, 0]);
g_ref.part_mut(Weights).extend(&[0.25, 0.5, 0.75]);

g_ref.part_mut(Neighbors).push(vec![1, 2]);
g_ref.part_mut(Neighbors).push(vec![0, 2]);
g_ref.part_mut(Neighbors).push(vec![0, 1]);

pub fn add_color_to_weight(
    mut g: partial!(Graph, mut Weights, Colors),
    index: usize,
) {
    g.part_mut(Weights)[index] += g.part(Colors)[index] as f32;
}

let (neighbors, mut g_ref) = g_ref.split_part_mut(Neighbors);
let (colors, mut g_ref) = g_ref.split_part(Colors);

for (edges, &color) in neighbors.iter_mut().zip(colors.iter()) {
    edges.retain(|&neighbor| colors[neighbor] != color);

    for &neighbor in edges.iter() {
        add_color_to_weight(g_ref.borrow(), neighbor);
    }
}

I have a bunch of additional features planned, but the next thing I want to do is to refactor my SAT solver to use this library.

I also hope that this library can be used to experiment with partial borrowing to gather experience for a possible future language extension.

#rust

Varisat 0.1.3: LRAT Generation and Proof Trimming

I’ve released a new version of my SAT solver Varisat. It is now split across two crates: one for library usage and one for command line usage.

The major new features in this release concern the genration of unsatisfiability proofs. Varisat is now able to directly generate proofs in the LRAT format in addition to the DRAT format. The binary versions of both formats are supported too. Varisat is also able to do on the fly proof trimming now. This is similar to running DRAT-trim but processes the proof while the solver runs.

[Read More]

Introducing Varisat

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.

[Read More]