Crate rustsat

RustSAT - A Comprehensive SAT Library for Rust

RustSAT is a collection of interfaces and utilities for working with the boolean satisfiability problem in Rust. This library aims to provide implementations of elements commonly used in the development of software in the area of satisfiability solving. The focus of the library is to provide as much ease of use without giving up on performance.

Example

let mut instance: SatInstance = SatInstance::new();
let l1 = instance.new_lit();
let l2 = instance.new_lit();
instance.add_binary(l1, l2);
instance.add_binary(!l1, l2);
instance.add_unit(l1);
let mut solver = rustsat_minisat::core::Minisat::default();
solver.add_cnf(instance.into_cnf().0).unwrap();
let res = solver.solve().unwrap();
assert_eq!(res, SolverResult::Sat);
let sol = solver.full_solution().unwrap();
assert_eq!(sol[l1.var()], TernaryVal::True);
assert_eq!(sol[l2.var()], TernaryVal::True);

Crates

The RustSAT project is split up into multiple crates that are all contained in this repository. These are the crates the project consists of:

Crate	Description
rustsat	The main library, containing basic types, traits, encodings, parsers, and more.
rustsat-tools	A collection of small helpful tools based on RustSAT that can be installed as binaries. For a list of available tools, see this directory with short descriptions of the tools in the headers of the files.
rustsat-<satsolver>	Interfaces to SAT solvers that can be used alongside RustSAT. Currently interfaces are available for cadical, kissat, glucose, and minisat.
rustsat-ipasir	IPASIR bindings to use any compliant solver with RustSAT.
pigeons	A library for writing VeriPB proofs. Used by RustSAT with the proof-logging feature.

Installation

To use the RustSAT library as a dependency in your project, simply run cargo add rustsat. To use an SAT solver interface in your project, run cargo add rustsat-<satsolver>. Typically, the version of the SAT solver can be selected via crate features, refer to the documentation of the respective SAT solver crate for details.

To install the binary tools in rustsat-tools run cargo install rustsat-tools.

Features

Feature name	Description
optimization	Include optimization (MaxSAT) data structures etc.
multiopt	Include data structures etc. for multi-objective optimization.
compression	Enable parsing and writing compressed input.
fxhash	Use the faster firefox hash function from rustc-hash in RustSAT.
rand	Enable randomization features. (Shuffling clauses etc.)
ipasir-display	Changes Display trait for Lit and Var types to follow IPASIR variables indexing.
serde	Add implementations for serde::Serialize and serde::Deserialize for many library types
proof-logging	Add proof logging / certification support to constraint encodings
verbose-proofs	Make the generated proofs (see proof-logging) more verbose, for debugging and testing
bench	Enable benchmark tests. Behind feature flag since it requires unstable Rust.
internals	Make some internal data structures for e.g. encodings public. This is useful when basing a more complex encoding on the RustSAT implementation of another encoding. Note that the internal API might change between releases.

Examples

For example usage refer to the small example tools in the rustsat-tools crate at tools/src/bin. For a bigger example you can look at this multi-objective optimization solver.

Minimum Supported Rust Version (MSRV)

Currently, the MSRV of RustSAT is 1.76.0, the plan is to always support an MSRV that is at least a year old.

Bumps in the MSRV will not be considered breaking changes. If you need a specific MSRV, make sure to pin a precise version of RustSAT.

Modules

algs

SAT-Related Algorithms

encodings

Encodings for Common Constraint Types to CNF

instances

Satisfiability and Optimization Instance Representations

solvers

Interfaces to SAT Solvers

types

Common Types for SAT Solving

utils

Library-Internal Utilities

Macros

clause

Creates a clause from a list of literals

ipasir_lit

More easily creates literals with IPASIR/DIMACS indexing (starts from 1) and negation (negative value is negation). Mainly used in tests.

lit

More easily creates literals. Mainly used in tests.

var

More easily creates variables. Mainly used in tests.

Structs

NotAllowedinternals

Error returned if the user tries to perform an action that is not allowed

RequiresClausal

Error returned if an operation requires clausal constraints, but this is not the case

RequiresSoftLits

Error returned if an operation requires an objective represented as soft literals, but this is not the case

Enums

OutOfMemory

Error returned when an operation ran out of memory