Satoxid, a SATisfiability encoding library

Satoxid is a library to help with encoding SAT problems with a focus on ergonomics and debugability.

Features

• Predefined common constraints
• Variables are values of a user defined type instead of integers
• Modular, you can implement your own constraints and backends

Example

use satoxid::{CadicalEncoder, constraints::ExactlyK};

#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
enum Var {
    A, B, C
}

use Var::*;

fn main() {
    let mut encoder = CadicalEncoder::new();

    let constraint = ExactlyK {
        k: 1,
        lits: [A, B, C].iter().copied()
    };

    encoder.add_constraint(constraint);

    if let Some(model) = encoder.solve() {

        let true_vars = model.vars()
                             .filter(|v| v.is_pos())
                             .count();

        assert_eq!(true_vars, 1);
    }
}

For a more complex example see this rummy solver.

lib.rs:

Satoxid, a SATisfiability encoding library

Satoxid is a library to help with encoding SAT problems with a focus on ergonomics and debugability.

Example

use satoxid::{CadicalEncoder, constraints::ExactlyK};

#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
enum Var {
    A, B, C
}

use Var::*;

fn main() {
    let mut encoder = CadicalEncoder::new();

    let constraint = ExactlyK {
        k: 1,
        lits: [A, B, C].iter().copied()
    };

    encoder.add_constraint(constraint);

    if let Some(model) = encoder.solve() {

        let true_lits = model.vars()
                             .filter(|v| v.is_pos())
                             .count();

        assert_eq!(true_lits, 1);
    }
}

Concepts

Variables

SAT solvers usually use signed integers to represent literals. Depending on the sign, the literal is either positive or negative and the absolute value defines the SAT variable.

While this is a simple API for a SAT solver, it can be inconvenient the user to encode a problem like this. Therefore when using Satoxid we do not work directly with integers but define our own variable type where each value of that type is a SAT variable.

As an example, say we want to encode the famous puzzle Sudoku (see the examples for a full implementation). We have a 9x9 grid where each tile has a x-y-coordinate and a value. We can represent this like in this struct Tile.

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
struct Tile {
    x: u32,
    y: u32,
    value: u32,
}

A value of Tile has the meaning that the tile at position (x, y) has the number in value.

For a type to be usable as a SAT variable it needs to implement SatVar, which just requires the traits Debug, Copy, [Eq] and Hash.

We now can use Tile in constraints but by itself it only represents a positive literal. If we want to use a negative literal we need to wrap it in [Lit] which is an enum which cleary defines a positive or negative literal.

Finally there is a third type VarType which can be used as a literal. When using functions like add_constraint_implies_repr Satoxid generates new variables which have no relation to the user defined SAT variable like Tile. VarType enable the user to be able to use such unnamed variables.

Internally Satoxid handles the translation from user defined SAT variables to integer SAT variables for the solver using the VarMap type.

A common pattern is to use an enum which lists all possible kinds of variable in the problem. This enum is then used as the main variable type.

Constraints

Satoxid comes with a set of predefined constraints in the constraints module. A constraint is a type which can be turned into a finite amount of SAT clauses. This is represented using the Constraint trait.

For example if we wanted to constrain our Tile type such that every coordinate can only have exactly one value we would use the ExactlyK constraint.

use satoxid::constraints::ExactlyK;
#

let constraint = ExactlyK {
    k: 1,
    lits: (1..=9).map(|value| Tile { x, y, value })
};
encoder.add_constraint(constraint);

For most simple problems the constraints given should suffice, but if necessary the user can create their own by implementing this trait.

Sometimes it is necessary to compose multiple different constraints in non trivial ways. (e.g. We want at least four different constraints to be satisfied.) To do so, the ConstraintRepr trait allows constraints to be encoded to a single new variable which then can be used in other constraints.

Encoder and Solvers

The Encoder is the main type the user interacts with. It is given the constraints to be encoded and deals with mapping all SAT variables to their corresponding integer SAT variables. Additionally it has a debug flag which enables/disables debug functionality of the backend (printing the encoded constraints somewhere).

The clauses generated by constraints are given to a type implementing Backend. Such a backend might be a solver which is able to solve the encoded problem or maybe just prints the clauses somewhere for external use like DimacsWriter.

If a backend is capable of solving it implements the Solver trait and allows the user to call solve on the encoder. By default Satoxid provides the CaDiCaL SAT solver as a backend which can be used with the CadicalEncoder type definition. This dependency can be disabled using the cadical feature.