Module rustsat::solvers

source ·
Expand description

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 C++. It includes incremental inprocessing. It is available through the rustsat-cadical crate.

References

Kissat

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

References

Minisat

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

References

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

IPASIR

IPASIR is a C API for incremental SAT solvers. RustSAT’s IPASIR interface is disabled by default since linking to multiple solvers implementing IPASIR at the same time is not possible. The main reason for including the IPASIR interface in RustSAT is to make it easier to include solvers that don’t have Rust interface crates. For this, make sure to not depend on any other SAT solver crate to avoid potential namespace conflicts. Then enable the ipasir feature and modify the following lines in the build script build.rs accordingly.

// Link to custom IPASIR solver
// Modify this for linking to your static library
// Uncomment and modify this for linking to your static library
// The name of the library should be _without_ the prefix 'lib' and the suffix '.a'
//println!("cargo:rustc-link-lib=static=<path-to-your-static-lib>");
//println!("cargo:rustc-link-search=<name-of-your-static-lib>");
// If your IPASIR solver links to the C++ stdlib, uncomment the next four lines
//#[cfg(target_os = "macos")]
//println!("cargo:rustc-flags=-l dylib=c++");
//#[cfg(not(target_os = "macos"))]
//println!("cargo:rustc-flags=-l dylib=stdc++");

Structs

Enums

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

Type Aliases

  • SolveMightFail
    Return type of solver calls that don’t return but might fail