2026-07-20T10:41:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23749 2025-11-12T13:00:06Z ddc:004 open_access

RustSAT: A Library for SAT Solving in Rust Jabs, Christoph Rust library SAT solvers constraint encodings 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Christoph Jabs 2025 Is Part Of LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2025.15 urn:nbn:de:0030-drops-237498 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.15 eng https://creativecommons.org/licenses/by/4.0/legalcode