minisat 0.3.3

MiniSat Rust interface. Solves a boolean satisfiability problem given in conjunctive normal form.
docs.rs failed to build minisat-0.3.3
Please check the build logs for more information.
See Builds for ideas on how to fix a failed build, or Metadata for how to configure docs.rs builds.
If you believe this is docs.rs' fault, open an issue.
Visit the last successful build: minisat-0.4.4

MiniSat Rust interface. Solves a boolean satisfiability problem given in conjunctive normal form.

extern crate minisat;
use std::iter::once;
fn main() {
    let mut sat = minisat::Sat::new();
    let a = sat.new_lit();
    let b = sat.new_lit();

    // Solves ((a OR not b) AND b)
    sat.add_clause(vec![a, !b]);
    sat.add_clause(vec![b]);

    match sat.solve() {
        Ok(m) => {
            assert_eq!(m.value(&a), true);
            assert_eq!(m.value(&b), true);
        },
        Err(()) => panic!("UNSAT"),
    }
}

This crate compiles the MiniSat sources directly and binds through the minisat-c-bindings interface. The low-level C bindings are available through the sys module.

High-level features ported from satplus:

  • Traits for representing non-boolean values in the SAT problem:
    • Value trait (ModelValue)
    • Equality trait (ModelEq)
    • Ordering trait (ModelOrd)
  • Symbolic values (Symbolic<V>)
  • Non-negative integers with unary encoding (Unary)
  • Non-negative integers with binary encoding (Binary)

Graph coloring example:

extern crate minisat;
use std::iter::once;
fn main() {
    let mut coloring = minisat::Sat::new();

    #[derive(PartialEq, Eq, Debug, PartialOrd, Ord)]
    enum Color { Red, Green, Blue };

    let n_nodes = 5;
    let edges = vec![(0,1),(1,2),(2,3),(3,4),(3,1),(4,0),(4,2)];
    let colors = (0..n_nodes)
        .map(|_| coloring.new_symbolic(vec![Color::Red, Color::Green, Color::Blue]))
        .collect::<Vec<_>>();
    for (n1,n2) in edges {
        coloring.not_equal(&colors[n1],&colors[n2]);
    }
    match coloring.solve() {
        Ok(model) => {
            for i in 0..n_nodes {
                println!("Node {}: {:?}", i, model.value(&colors[i]));
            }
        },
        Err(()) => {
            println!("No solution.");
        }
    }
}

Factorization example:

extern crate minisat;

fn main() {
    let mut sat = minisat::Sat::new();
    let a = sat.new_binary(1000);
    let b = sat.new_binary(1000);
    let c = a.mul(&mut sat, &b);
    sat.equal(&c, &minisat::Binary::constant(36863));

    match sat.solve() {
        Ok(model) => {
            println!("{}*{}=36863", model.value(&a), model.value(&b));
        },
        Err(()) => {
            println!("No solution.");
        }
    }
}