Crate cat_solver

source ·
Expand description

This is a stand alone crate that contains both the C source code of the Kissat SAT solver together with its Rust binding. The C files are compiled and statically linked during the build process.

Kissat variants dominated the main track of the Sat Competition 2022. Author Armin Biere describes Kissat as follows:

Kissat is a “keep it simple and clean bare metal SAT solver” written in C. It is a port of CaDiCaL back to C with improved data structures, better scheduling of inprocessing and optimized algorithms and implementation. Coincidentally “kissat” also means “cats” in Finnish.

Structs

  • Error type for configuration errors.
  • The Kissat SAT solver. The literals are unwrapped positive and negative integers, as in the DIMACS format. The common IPASIR operations are presented in a safe Rust interface.