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/minisat

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/glucose4

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

Structs

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