# Crate satoxid[−][src]

Expand description

# 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 constraint = ExactlyK {
k: 1,
lits: [A, B, C].iter().copied()
};

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 })
};

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.