Module solvers 

Interfaces to SAT Solvers

This module holds types and functions regarding SAT solvers. The main element is the Solve trait that every SAT solver in this library implements.

Available Solvers

Solvers are available through separate crates.

CaDiCaL

CaDiCaL is a fully incremental SAT solver by Armin Biere implemented in Cpp. It includes incremental inprocessing. It is available through the rustsat-cadical crate.

References

• Armin Biere and Katalin Fazekas and Mathias Fleury and Maximillian Heisinger: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling Entering the SAT Competition 2020, SAT Competition 2020.
• Original Repository: https://github.com/arminbiere/cadical
• Solver crate: https://crates.io/crates/rustsat-cadical

Kissat

Kissat is a non-incremental SAT solver by Armin Biere implemented in C. It is available through the rustsat-kissat crate.

References

• Armin Biere and Katalin Fazekas and Mathias Fleury and Maximillian Heisinger: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling Entering the SAT Competition 2020, SAT Competition 2020.
• Repository: https://github.com/arminbiere/kissat
• Solver crate: https://github.com/chrjabs/rustsat-kissat

Minisat

Minisat is an incremental SAT solver by Niklas Eén and Niklas Sörensson. It is available through the rustsat-minisat crate.

References

• Niklas Eén and Niklas Sörensson (2003): An Extensible SAT-solver, SAT 2003.
• Repository: https://github.com/niklasso/minisat
• Solver crate: https://crates.io/crates/rustsat-minisat
• Fork used in solver crate: https://github.com/chrjabs/rustsat/tree/main/minisat/cppsrc

Glucose

Glucose is a SAT solver based on Minisat and developed by Gilles Audemard and Laurent Simon. It is available through the rustsat-glucose crate.

References

• Gilles Audemard and Laurent Simon: Predicting Learnt Clauses Quality in Modern SAT Solvers, IJCAI 2009.
• More references at the Glucose web-page
• Solver crate: https://crates.io/crates/rustsat-glucose
• Fork used in solver crate: https://github.com/chrjabs/rustsat/tree/main/glucose/cppsrc

BatSat

BatSat is a SAT solver based on Minisat but fully implemented in Rust. Because it is fully implemented in Rust, it is a good choice for restricted compilation scenarios like WebAssembly. BatSat is available through the rustsat-batsat crate.

References

• Solver interface crate: https://crates.io/crates/rustsat-batsat
• BatSat crate: https://crates.io/crates/batsat
• BatSat repository: https://github.com/c-cube/batsat

External Solvers

RustSAT provides an interface for calling external solver binaries by passing them DIMACS input and parsing their output written to <stdout>. For more details, see the ExternalSolver type.

IPASIR

IPASIR is a C API for incremental SAT solvers. IPASIR bindings for RustSAT are provided in the rustsat-ipasir crate.

Re-exports

pub use external::Solver as ExternalSolver;

Modules

external

Solver Interface for External Executables

simulators

Solver Simulators

Structs

DefaultInitializer

An initializer that simply calls the Default method of another type

PropagateResult

A result returned from the Propagate trait

SolverStats

Solver statistics

StateError

A solver state error

Enums

ControlSignal

Return type for solver terminator callbacks

SolverResult

Return value for solving queries.

SolverState

States that the solver can be in.

Traits

FlipLit

Trait for all solvers that can flip a literal in the current assignment

FreezeVar

Trait for freezing and melting variables in solvers with pre-/inprocessing.

GetInternalStats

Trait for all solvers allowing access to internal search statistics

Initialize

Trait for types that allow for initializing a solver or other types

Interrupt

Trait for all solvers that can be asynchronously interrupt.

InterruptSolver

A thread safe interrupter for a solver

Learn

Trait for all solvers that can pass out learned clauses via a callback.

LimitConflicts

Trait for all solvers that can limit the number of conflicts

LimitDecisions

Trait for all solvers that can limit the number of decisions

LimitPropagations

Trait for all solvers that can limit the number of propagations

PhaseLit

Trait for all solvers that can force a face for a literal

Propagate

Trait for propagating a set of assumptions and getting all propagated literals

Solve

Trait for all SAT solvers in this library. Solvers outside of this library can also implement this trait to be able to use them with this library.

SolveIncremental

Trait for all SAT solvers in this library. Solvers outside of this library can also implement this trait to be able to use them with this library.

SolveStats

Trait for solvers that track certain statistics.

Terminate

Trait for all solvers that can be terminated by a termination callback.