rssat

rssat is a Rust library that provides Rust bindings for multiple popular SAT solvers. Currently supported solvers include:

• MiniSat (2.2.0)
• Glucose (4.2.1)
• CaDiCaL (2.0.0)

We thank the contributors of these excellent projects.

Features

• Unified Rust interface for different SAT solvers

• Support for adding clauses

• Solving SAT problems and returning results

• Access to native bindings for advanced functionality

• Support reading formulas from files

Build Requirements

To build RSsat, you need the following tools and libraries:

• C++ compiler (e.g., GCC, Clang)
• CMake
• patch command
• Other standard build tools (make, etc.)

Installation

[dependencies]
rssat = "0.1.2"

Usage Example

Here's a simple example using the CaDiCaL solver:

use rssat::solver::{CaDiCaLSolver, Status,Solver};

fn main() {
    let mut solver = CaDiCaLSolver::new();
    
    solver.add_clause(&vec![1, 2]);
    solver.add_clause(&vec![-1, -2]);
    solver.add_clause(&vec![3]);
    
    
    match solver.solve() {
        Status::SATISFIABLE(vec) => {
            println!("Satisfiable solution: {:?}", vec);
        },
        Status::UNSATISFIABLE => {
            println!("Unsatisfiable");
        },
        Status::UNKNOWN => {
            println!("Unknown");
        },
    }
}

Native Bindings

For advanced usage, you can access the native bindings of each solver. This allows you to use solver-specific features that are not part of the unified interface.

Future Work

• Improve documentation to enhance user experience

Contributing

Issue reports and pull requests are welcome!

License

MIT License