Crate sat_solvers 

SAT Solvers

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

This crate 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.

Features

• Self-contained: 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

Quick Start

Add sat-solvers to your Cargo.toml:

[dependencies]
sat-solvers = "0.1"

By default, CaDiCaL and MiniSat are enabled. To use other solvers, enable their features:

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

Example

Solve a simple SAT problem using CaDiCaL:

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

use sat_solvers::solvers::cadical::CaDiCaLExecutor;

// Define a simple 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";

let executor = CaDiCaLExecutor;
let result = executor.execute(dimacs, Some(Duration::from_secs(30))).unwrap();

match result {
    SATResult::Satisfiable(assignment) => {
        println!("Satisfiable! Assignment: {:?}", assignment);
    }
    SATResult::Unsatisfiable => {
        println!("Unsatisfiable");
    }
    SATResult::Unknown => {
        println!("Unknown (timeout or resource limit)");
    }
}

Available Solvers

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

Build Requirements

Since solvers are compiled from source, you need:

• A C++ compiler (g++ or clang++)
• make
• cmake (for Glucose)

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

Re-exports

pub use solvers::SolverExecutor;

Modules

solvers

SAT solver executors and utilities.

Enums

SATResult

The result of a SAT solver execution.

SATSolverKind

Identifies which SAT solver to use.

SATSolversError

Errors that can occur when working with SAT solvers.

Functions

cadical_path

Returns the path to the CaDiCaL binary.

ensure_solver_exists

Ensures that the specified solver binary exists at its expected path.

minisat_path

Returns the path to the MiniSat binary.

run_solver

Runs the specified solver with the given command-line arguments.

solver_path

Returns the path to the specified solver’s binary.