RustSAT: A Library For SAT Solving in Rust

Abstract

State-of-the-art Boolean satisfiability (SAT) solvers constitute a practical and competitive approach for solving various real-world problems. To encourage their widespread adoption, the relatively high barrier of entry following from the low level syntax of SAT and the expert knowledge required to achieve tight integration with SAT solvers should be further reduced. We present RustSAT, a library with the aim of making SAT solving technology readily available in the Rust programming language. RustSAT provides functionality for helping with generating (Max)SAT instances, writing them to, or reading them from files. Furthermore, RustSAT includes interfaces to various state-of-the-art SAT solvers available with a unified Rust API. Lastly, RustSAT implements several encodings for higher level constraints (at-most-one, cardinality, and pseudo-Boolean), which are also available via a C and Python API.

Bibtex

@inproceedings{Jabs2025RustsatLibrarySat,
  title = {{RustSAT}: {A} Library For {SAT} Solving in Rust},
  author = {Jabs, Christoph},
  booktitle = {28th International Conference on Theory and Applications of Satisfiability
    Testing ({SAT} 2025)},
  editor = {Berg, Jeremias and Nordstr{\"o}m, Jakob},
  year = {2025},
  volume = {341},
  publisher = {Schloss Dagstuhl---Leibniz-Zentrum f{\"{u}}r Informatik},
  series = {Leibniz International Proceedings in Informatics ({LIPIcs})},
  pages = {24:1--24:13},
  doi = {10.4230/LIPIcs.SAT.2025.24},
  eprint = {2505.15221},
  eprinttype = {arXiv},
}