3 releases
0.1.2 | May 24, 2021 |
---|---|
0.1.1 | May 23, 2021 |
0.1.0 | May 22, 2021 |
#1078 in Encoding
130KB
3.5K
SLoC
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.
Dependencies
~0.8–1.2MB
~26K SLoC