# sat-solvers
[](https://crates.io/crates/sat-solvers)
[](https://docs.rs/sat-solvers)
[](LICENSE)
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`:
```toml
[dependencies]
sat-solvers = "0.1"
```
By default, CaDiCaL and MiniSat are enabled. To use specific solvers:
```toml
[dependencies]
sat-solvers = { version = "0.1", default-features = false, features = ["cadical", "kissat"] }
```
### Available Features
| `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
```rust
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:
```text
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)`:
```text
p cnf 3 3
1 2 0
-1 3 0
-2 -3 0
```
### Using Different Solvers
All solver executors implement the same `SolverExecutor` trait:
```rust
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:
```bash
sudo apt install build-essential cmake
```
On macOS:
```bash
xcode-select --install
brew install cmake
```
On Arch Linux:
```bash
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:
```bash
brew install gcc@14
CXX=g++-14 cargo build --features minisat
```
## Comparison with Alternatives
| **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](LICENSE)).
### Bundled Solver Licenses
The bundled SAT solver source code is subject to their respective licenses:
- [**CaDiCaL**: MIT License](https://github.com/arminbiere/cadical)
- [**MiniSat**: MIT License](https://github.com/niklasso/minisat)
- [**Glucose**: MIT License](https://github.com/audemard/glucose)
- [**Lingeling**: MIT License](https://github.com/arminbiere/lingeling)
- [**Kissat**: MIT License](https://github.com/arminbiere/kissat)
## Contributing
Contributions are welcome! Please feel free to submit a Pull Request.