[−][src]Crate minisat
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::Solver::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
)
- Value trait (
- 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; use minisat::symbolic::*; fn main() { let mut coloring = minisat::Solver::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(|_| Symbolic::new(&mut coloring, 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; use minisat::{*, binary::*}; fn main() { let mut sat = Solver::new(); let a = Binary::new(&mut sat, 1000); let b = Binary::new(&mut sat, 1000); let c = a.mul(&mut sat, &b); sat.equal(&c, &Binary::constant(36863)); match sat.solve() { Ok(model) => { println!("{}*{}=36863", model.value(&a), model.value(&b)); }, Err(()) => { println!("No solution."); } } }
Modules
binary | Binary encoding of non-negative integers (see |
symbolic | Symbolic values (see the struct |
sys | The FFI interface to MiniSat (imported from minisat-c-bindings). |
unary | Unary encoding of non-negative integers (see |
Structs
Lit | A literal is a boolean variable or its negation. |
Model | A model of a satisfiable instance, i.e. assignments to variables in the problem satisfying the asserted constraints. |
Solver | Solver object representing an instance of the boolean satisfiability problem. |
Enums
Bool | Boolean value, either a constant ( |
Traits
ModelEq | Object that can be compared and constrainted for equality. |
ModelOrd | Object that can be compared and constrained by ordering. |
ModelValue | Object that has a value in the |