#satisfiability #compiler #boolean #form #minisat

minisat

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

12 unstable releases (3 breaking)

0.4.2 Jan 29, 2019
0.4.1 Jan 3, 2019
0.4.0 Nov 22, 2018
0.3.4 Nov 21, 2018
0.1.1 Oct 21, 2018

#55 in Science

Download history 16/week @ 2018-11-12 56/week @ 2018-11-19 78/week @ 2018-11-26 66/week @ 2018-12-03 16/week @ 2018-12-10 13/week @ 2018-12-17 30/week @ 2018-12-24 19/week @ 2018-12-31 28/week @ 2019-01-07 22/week @ 2019-01-14 1/week @ 2019-01-21 16/week @ 2019-01-28 3/week @ 2019-02-04 1/week @ 2019-02-18

129 downloads per month

MIT license

150KB
3K SLoC

C++ 1.5K SLoC // 0.2% comments Rust 1.5K SLoC // 0.1% comments

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.");
        }
    }
}

Dependencies

~2MB
~35K SLoC