bddminisat-sys

FFI bindings to bdd_minisat_all, a BDD-based AllSAT solver.

Overview

bdd_minisat_all is a SAT solver that enumerates all satisfying assignments and compiles them into an Ordered Binary Decision Diagram (OBDD). It is built on top of MiniSat by Niklas Sorensson and developed by Takahisa Toda.

Features

• AllSAT solving: enumerate all satisfying assignments
• OBDD compilation: solutions are represented as an OBDD
• Efficient caching mechanisms (cutset/separator caching)
• Non-blocking and blocking modes

Usage

Add this to your Cargo.toml:

[dependencies]
bddminisat-sys = "0.1"

Basic Example

use bddminisat_sys::*;

fn main() {
    unsafe {
        // Create a new solver
        let solver = solver_new();

        // Set number of variables
        solver_setnvars(solver, 3);

        // Add clause: (x0 OR x1)
        let mut clause = [toLit(0), toLit(1)];
        solver_addclause(solver, clause.as_mut_ptr(), clause.as_mut_ptr().add(2));

        // Add clause: (NOT x0 OR x2)
        let mut clause2 = [lit_neg(toLit(0)), toLit(2)];
        solver_addclause(solver, clause2.as_mut_ptr(), clause2.as_mut_ptr().add(2));

        // Solve (enumerates all solutions and builds OBDD)
        let sat = solver_solve(solver, std::ptr::null_mut(), std::ptr::null_mut());

        if sat != 0 {
            // Get the OBDD root
            let root = (*solver).root;

            // Count solutions
            let num_solutions = obdd_nsols(solver_nvars(solver), root);
            println!("Number of solutions: {}", num_solutions);
        }

        // Clean up
        solver_delete(solver);
    }
}

API Reference

Constants

Literal Operations (Rust inline functions)

Solver API (FFI)

OBDD API (FFI)

OBDD Helper Functions (Rust inline)

Global Variables

Structures

Optional Features

GMP Support

For counting very large numbers of solutions, enable the gmp feature:

[dependencies]
bddminisat-sys = { version = "0.1", features = ["gmp"] }

This requires the GMP library to be installed on your system.

License

This project is licensed under the MIT License - see the LICENSE file for details.

• MiniSat: Copyright (c) 2005, Niklas Sorensson
• bdd_minisat_all: Copyright (c) 2015, Takahisa Toda

References

• bdd_minisat_all homepage
• MiniSat