RustSAT: A Library For SAT Solving in Rust

TL;DR

RustSAT is a Rust library that simplifies the integration and use of SAT solvers, offering tools for generating, reading, and encoding SAT instances with a unified API across multiple languages.

Contribution

The paper introduces RustSAT, a library that makes SAT solving more accessible in Rust by providing APIs, encodings, and interoperability with existing solvers.

Findings

Provides a unified Rust API for multiple SAT solvers

Includes encodings for higher-level constraints like cardinality and pseudo-Boolean

Facilitates easier integration of SAT solving in Rust applications

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.