sat-solvers

A unified Rust interface to multiple SAT solvers with automatic source compilation.

Overview

sat-solvers provides a simple way to use popular SAT solvers (CaDiCaL, MiniSat, Glucose, Lingeling, Kissat) without requiring pre-installed binaries. The solvers are compiled from source during cargo build, ensuring reproducible builds across different systems.

Key Features

• Self-contained builds: Solvers are built from bundled source code during compilation
• Unified interface: All solvers implement the SolverExecutor trait
• Feature-gated: Only compile the solvers you need
• Timeout support: Built-in timeout handling for long-running problems
• DIMACS format: Standard CNF input format supported by all solvers

Installation

Add sat-solvers to your Cargo.toml:

[dependencies]
sat-solvers = "0.1"

By default, CaDiCaL and MiniSat are enabled. To use specific solvers:

[dependencies]
sat-solvers = { version = "0.1", default-features = false, features = ["cadical", "kissat"] }

Available Features

Feature	Solver	Description
cadical	CaDiCaL	State-of-the-art CDCL solver, SAT Competition winner
minisat	MiniSat	Classic, widely-used SAT solver
glucose	Glucose	MiniSat derivative with improved learning
lingeling	Lingeling	High-performance solver by Armin Biere
kissat	Kissat	Successor to CaDiCaL, SAT Competition 2020+ winner

Usage

Basic Example

use sat_solvers::solvers::cadical::CaDiCaLExecutor;
use sat_solvers::solvers::SolverExecutor;
use sat_solvers::SATResult;
use std::time::Duration;

fn main() {
    let executor = CaDiCaLExecutor;

    // Define a CNF formula in DIMACS format:
    // (x1 OR NOT x2) AND (x2 OR x3)
    let dimacs = "p cnf 3 2\n1 -2 0\n2 3 0\n";

    // Solve with a 30-second timeout
    let result = executor.execute(dimacs, Some(Duration::from_secs(30))).unwrap();

    match result {
        SATResult::Satisfiable(assignment) => {
            println!("Satisfiable! Assignment: {:?}", assignment);
            // Output: Satisfiable! Assignment: [1, -2, 3]
            // Meaning: x1 = true, x2 = false, x3 = true
        }
        SATResult::Unsatisfiable => {
            println!("Unsatisfiable - no solution exists");
        }
        SATResult::Unknown => {
            println!("Unknown - solver timed out or hit resource limit");
        }
    }
}

DIMACS CNF Format

The solvers accept input in DIMACS CNF format:

p cnf <num_variables> <num_clauses>
<literal1> <literal2> ... 0
<literal1> <literal2> ... 0
...

• Variables are positive integers (1, 2, 3, ...)
• Negative literals represent negation (-1 means NOT x1)
• Each clause ends with 0

Example - encoding (x1 OR x2) AND (NOT x1 OR x3) AND (NOT x2 OR NOT x3):

p cnf 3 3
1 2 0
-1 3 0
-2 -3 0

Using Different Solvers

All solver executors implement the same SolverExecutor trait:

use sat_solvers::solvers::SolverExecutor;
use std::time::Duration;

// Use any solver through the trait
fn solve_with<E: SolverExecutor>(executor: E, dimacs: &str) {
    match executor.execute(dimacs, Some(Duration::from_secs(60))) {
        Ok(result) => println!("Result: {}", result),
        Err(e) => eprintln!("Error: {}", e),
    }
}

// With CaDiCaL
#[cfg(feature = "cadical")]
solve_with(sat_solvers::solvers::cadical::CaDiCaLExecutor, dimacs);

// With MiniSat
#[cfg(feature = "minisat")]
solve_with(sat_solvers::solvers::minisat::MiniSatExecutor, dimacs);

// With Kissat
#[cfg(feature = "kissat")]
solve_with(sat_solvers::solvers::kissat::KissatExecutor, dimacs);

Build Requirements

Since solvers are compiled from source, you need:

• C++ compiler: g++ or clang++
• make: GNU Make
• cmake: Required for Glucose

On Ubuntu/Debian:

sudo apt install build-essential cmake

On macOS:

xcode-select --install
brew install cmake

On Arch Linux:

sudo pacman -S base-devel cmake

macOS Compatibility Note

MiniSat has C++ compatibility issues with the default macOS clang compiler. All other solvers (CaDiCaL, Glucose, Kissat, Lingeling) work correctly on macOS.

If you need MiniSat on macOS, you can try installing GCC via Homebrew and setting the CXX environment variable:

brew install gcc@14
CXX=g++-14 cargo build --features minisat

Comparison with Alternatives

Crate	Approach	Pros	Cons
sat-solvers	Builds solvers from source at build time	Self-contained, reproducible, no system deps	Longer build times
rustsat	FFI bindings to C/C++ code	Zero-overhead, full API access	Complex build, tight coupling
exec-sat	Executes pre-installed binaries	Simple, flexible	Requires manual binary installation
splr	Pure Rust implementation	No native dependencies	Single solver, may differ from C versions

Choose sat-solvers when you want:

• Reproducible builds without system dependencies
• Easy switching between multiple established solvers
• Simple integration with timeout support

License

Licensed under the MIT license (LICENSE).

Bundled Solver Licenses

The bundled SAT solver source code is subject to their respective licenses:

• CaDiCaL: MIT License
• MiniSat: MIT License
• Glucose: MIT License
• Lingeling: MIT License
• Kissat: MIT License

Contributing

Contributions are welcome! Please feel free to submit a Pull Request.