Crate satoxid

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.

Modules

constraints

Collection of commonly used constraints.

Structs

DimacsWriter	Backend which collects all generated clauses and is able to print them in the DIMACS format.
Encoder	The Encoder type contains all data used for the encoding.
Model	The of successfully solving an encoded problem.
VarMap	Mapper from user defined variables and integer sat variables.

Enums

Lit	Enum to define the polarity of variables. By itself Lit is a constraint, which requires that the variable it wraps is true or false depending on the Variant Pos and Neg.
VarType	Type which represents every used SAT variable by the encoder. It is either a named user defined SAT variable. Or an unnamed generated SAT variable.

Traits

Backend	Backend abstraction trait.
Constraint	Trait used to express a constraint. Constraints generate a finite set of clauses which are passed to the given backend.
ConstraintRepr	Trait used to express a constraint which can imply another variable, a so called representative (repr).
SatVar	Trait which expresses the required trait bounds for a SAT variable.
Solver	A trait for Backends with are capable of solving SAT Problems.

Type Definitions

CadicalEncoder

Encoder using the CaDiCal SAT solver.