2025/05/21 by Christoph Jabs, Jabs, Christoph
Computer Science · Engineering · #3D Modeling in Geospatial Applications #Data Management and Algorithms #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Technology and Security Systems
paper · pdf · doi:10.48550/arxiv.2505.15221
openalex publication_date 2025/05/21 · openalex created_date 2025/10/19 · openalex updated_date 2026/07/28
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.