# 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 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 |

VarType | Type which represents |

## 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. |