arminbiere / kissat

MIT License
452 stars 85 forks source link

License: MIT

The Kissat SAT Solver

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.

Run ./configure && make test to configure, build and test in build.

Binaries are provided with each major release.

You can get more information about Kissat in the last solver description for the SAT Competition 2024:

Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks and Florian Pollitt
CaDiCaL, Gimsatul, IsaSAT and Kissat Entering the SAT Competition 2024
Proc. SAT Competition 2024: Solver, Benchmark and Proof Checker Descriptions
Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors)
Department of Computer Science Report Series B
vol. B-2024-1, pages 8-10, University of Helsinki 2024
[ paper | bibtex | cadical | kissat | gimsatul | medals ]

See NEWS.md for feature updates.