cat_solver 3.1.1

Rust bindings for the Kissat SAT solver
Documentation
  • Coverage
  • 83.33%
    10 out of 12 items documented1 out of 10 items with examples
  • Size
  • Source code size: 885.73 kB This is the summed size of all the files inside the crates.io package for this release.
  • Documentation size: 382.87 kB This is the summed size of all files generated by rustdoc for all configured targets
  • Ø build duration
  • this release: 32s Average build duration of successful builds.
  • all releases: 32s Average build duration of successful builds in releases after 2024-10-23.
  • Links
  • UncombedCoconut/cat_solver
    3 0 0
  • crates.io
  • Dependencies
  • Versions
  • Owners
  • UncombedCoconut

Kissat SAT solver

Crate Documentation GitHub

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.

This crate is based on the "cadical" crate, and is as API-compatible as possible. This enables a switch back to cadical::Solver (which has extra features like file I/O) as a debugging strategy. Beware: this also means the API will let you try to modify the problem after solving, but Kissat will abort if you do. Incremental solving is not yet implemented.

The literals are unwrapped positive and negative integers, exactly as in the DIMACS format. The common IPASIR operations are presented in a safe Rust interface.

let mut sat: cat_solver::Solver::new();
sat.add_clause([1, 2]);
sat.add_clause([-1, 2]);
assert_eq!(sat.solve(), Some(true));
assert_eq!(sat.value(2), Some(true));