Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

RustSAT: A Library For SAT Solving in Rust

Christoph Jabs

TL;DR

RustSAT addresses the barrier to using SAT solving in Rust by providing a unified library for problem construction, solver interfacing, and high-level constraint encodings, with multiple solver backends and C/Python APIs. It emphasizes safety and performance through Rust's type system, trait-based interfaces, and zero-cost abstractions, while enabling practical workflows in configuration, puzzle solving, and MaxSAT. Empirical aspects highlight favorable performance relative to PySAT in solution enumeration and minimal overhead when calling solvers directly, underscoring the potential to boost Rust-based SAT tooling. The open-source, well-documented design aims to broaden adoption of SAT techniques in Rust-centric 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.

RustSAT: A Library For SAT Solving in Rust

TL;DR

RustSAT addresses the barrier to using SAT solving in Rust by providing a unified library for problem construction, solver interfacing, and high-level constraint encodings, with multiple solver backends and C/Python APIs. It emphasizes safety and performance through Rust's type system, trait-based interfaces, and zero-cost abstractions, while enabling practical workflows in configuration, puzzle solving, and MaxSAT. Empirical aspects highlight favorable performance relative to PySAT in solution enumeration and minimal overhead when calling solvers directly, underscoring the potential to boost Rust-based SAT tooling. The open-source, well-documented design aims to broaden adoption of SAT techniques in Rust-centric 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.

Paper Structure

This paper contains 8 sections, 3 figures, 2 tables.

Table of Contents

  1. Introduction
  2. The Rust Programming Language
  3. Design Principles and Functionality
  4. Working with Problem Instances
  5. SAT Solver Interfaces
  6. Constraint Encodings
  7. C and Python API
  8. Conclusions

Figures (3)

  • Figure 1: Runtime comparison of solution enumerator with RustSAT, PySAT, and C++ for the https://benchmark-database.de/file/0f27eae382e7dcd8fd956ab914083a29?context=cnf instance.
  • Figure 2:
  • Figure 3: Left: Number of clauses in a totalizer cardinality encoding over 300 input literals for a given bound. Middle/Right: Number of clauses for a binary adder (middle) and generalized totalizer (right) pseudo-Boolean encoding for a given number of input literals with random weight in $[1,100]$ and enforced bound of 300.