Struct Instance

Source

pub struct Instance { /* private fields */ }

Expand description

An instance of the SAT problem.

Implementations§

Source §

impl Instance

Source

pub fn new() -> Instance

Create a new, empty SAT instance.

Examples found in repository ?

examples/print_dimacs.rs (line 6)

5fn main() {
6    let mut i = sat::Instance::new();
7    let x = i.fresh_var();
8    let y = i.fresh_var();
9    i.assert_any(&[x, y]);
10    i.assert_any(&[!x, !y]);
11
12    let s = sat::solver::dimacs::Dimacs::new(|| panic!());
13    s.write_instance(&mut io::stdout(), &i);
14}

More examples

Hide additional examples

examples/petersen.rs (line 41)

18fn main() {
19    // For each vertex, the list of adjacent vertices.
20    let mut adj: Vec<_> = iter::repeat(vec![]).take(VERTICES).collect();
21
22    // Inner 5 vertices
23    for i in 0..5 {
24        if i+2 < 5 {
25            adj[i].push(i+2);
26        }
27        if i+3 < 5 {
28            adj[i].push(i+3);
29        }
30    }
31
32    // Outer 5 vertices
33    for i in 5..VERTICES {
34        adj[i].push(i-5);
35        if i+1 < VERTICES {
36            adj[i].push(i+1);
37        }
38    }
39    adj[9].push(5);
40
41    let mut instance = sat::Instance::new();
42
43    // For each vertex, a vector of variables for the possible colors.
44    let mut vars = vec![];
45    for i in 0..VERTICES {
46        vars.push(vec![instance.fresh_var(), instance.fresh_var(), instance.fresh_var()]);
47
48        // Assert that each vertex has at least one color.
49        // red OR green OR blue
50        instance.assert_any(&[vars[i][0], vars[i][1], vars[i][2]]);
51
52        // Assert that each vertex has at most one color.
53        // (red IMPLIES !green) =equiv= (!green OR !red)
54        for c1 in 0..COLORS {
55            for c2 in 0..c1 {
56                instance.assert_any(&[!vars[i][c1], !vars[i][c2]]);
57            }
58        }
59    }
60
61    // Assert that adjacent vertices don't have the same color.
62    for (i, js) in adj.iter().enumerate() {
63        for &j in js {
64            for c in 0..COLORS {
65                instance.assert_any(&[!vars[i][c], !vars[j][c]]);
66            }
67        }
68    }
69
70    // Solve using minisat.
71    let solver = sat::solver::Dimacs::new(|| {
72        let mut c = Command::new("minisat");
73        c.stdout(process::Stdio::null());
74        c
75    });
76
77    let solution = solver.solve(&instance).unwrap();
78
79    // Extract the colors.
80    // Make sure there's only one color per vertex.
81    let mut colors: Vec<_> = iter::repeat(None).take(VERTICES).collect();
82    for i in 0..VERTICES {
83        for c in 0..COLORS {
84            if solution.get(vars[i][c]) {
85                assert!(mem::replace(&mut colors[i], Some(c)).is_none());
86            }
87        }
88    }
89
90    // Output in GraphViz format.
91    println!("graph {{");
92    for (i, js) in adj.iter().enumerate() {
93        println!("    {} [color=\"{}\"];", i,
94            ["red", "green", "blue"][colors[i].unwrap()]);
95
96        for j in js {
97            println!("    {} -- {};", i, j);
98        }
99    }
100    println!("}}");
101}

Source

pub fn fresh_var(&mut self) -> Literal

Create a fresh variable.

Examples found in repository ?

examples/print_dimacs.rs (line 7)

5fn main() {
6    let mut i = sat::Instance::new();
7    let x = i.fresh_var();
8    let y = i.fresh_var();
9    i.assert_any(&[x, y]);
10    i.assert_any(&[!x, !y]);
11
12    let s = sat::solver::dimacs::Dimacs::new(|| panic!());
13    s.write_instance(&mut io::stdout(), &i);
14}

More examples

Hide additional examples

examples/petersen.rs (line 46)

18fn main() {
19    // For each vertex, the list of adjacent vertices.
20    let mut adj: Vec<_> = iter::repeat(vec![]).take(VERTICES).collect();
21
22    // Inner 5 vertices
23    for i in 0..5 {
24        if i+2 < 5 {
25            adj[i].push(i+2);
26        }
27        if i+3 < 5 {
28            adj[i].push(i+3);
29        }
30    }
31
32    // Outer 5 vertices
33    for i in 5..VERTICES {
34        adj[i].push(i-5);
35        if i+1 < VERTICES {
36            adj[i].push(i+1);
37        }
38    }
39    adj[9].push(5);
40
41    let mut instance = sat::Instance::new();
42
43    // For each vertex, a vector of variables for the possible colors.
44    let mut vars = vec![];
45    for i in 0..VERTICES {
46        vars.push(vec![instance.fresh_var(), instance.fresh_var(), instance.fresh_var()]);
47
48        // Assert that each vertex has at least one color.
49        // red OR green OR blue
50        instance.assert_any(&[vars[i][0], vars[i][1], vars[i][2]]);
51
52        // Assert that each vertex has at most one color.
53        // (red IMPLIES !green) =equiv= (!green OR !red)
54        for c1 in 0..COLORS {
55            for c2 in 0..c1 {
56                instance.assert_any(&[!vars[i][c1], !vars[i][c2]]);
57            }
58        }
59    }
60
61    // Assert that adjacent vertices don't have the same color.
62    for (i, js) in adj.iter().enumerate() {
63        for &j in js {
64            for c in 0..COLORS {
65                instance.assert_any(&[!vars[i][c], !vars[j][c]]);
66            }
67        }
68    }
69
70    // Solve using minisat.
71    let solver = sat::solver::Dimacs::new(|| {
72        let mut c = Command::new("minisat");
73        c.stdout(process::Stdio::null());
74        c
75    });
76
77    let solution = solver.solve(&instance).unwrap();
78
79    // Extract the colors.
80    // Make sure there's only one color per vertex.
81    let mut colors: Vec<_> = iter::repeat(None).take(VERTICES).collect();
82    for i in 0..VERTICES {
83        for c in 0..COLORS {
84            if solution.get(vars[i][c]) {
85                assert!(mem::replace(&mut colors[i], Some(c)).is_none());
86            }
87        }
88    }
89
90    // Output in GraphViz format.
91    println!("graph {{");
92    for (i, js) in adj.iter().enumerate() {
93        println!("    {} [color=\"{}\"];", i,
94            ["red", "green", "blue"][colors[i].unwrap()]);
95
96        for j in js {
97            println!("    {} -- {};", i, j);
98        }
99    }
100    println!("}}");
101}

Source

pub fn assert_any<'a, I>(&mut self, lits: I)
where I: IntoIterator<Item = &'a Literal>,

Assert that at least one of the provided literals must evaluate to true.

This is a CNF (conjunctive normal form) constraint, which is the basic type of constraint in most solvers.

Examples found in repository ?

examples/print_dimacs.rs (line 9)

5fn main() {
6    let mut i = sat::Instance::new();
7    let x = i.fresh_var();
8    let y = i.fresh_var();
9    i.assert_any(&[x, y]);
10    i.assert_any(&[!x, !y]);
11
12    let s = sat::solver::dimacs::Dimacs::new(|| panic!());
13    s.write_instance(&mut io::stdout(), &i);
14}

More examples

Hide additional examples

examples/petersen.rs (line 50)

18fn main() {
19    // For each vertex, the list of adjacent vertices.
20    let mut adj: Vec<_> = iter::repeat(vec![]).take(VERTICES).collect();
21
22    // Inner 5 vertices
23    for i in 0..5 {
24        if i+2 < 5 {
25            adj[i].push(i+2);
26        }
27        if i+3 < 5 {
28            adj[i].push(i+3);
29        }
30    }
31
32    // Outer 5 vertices
33    for i in 5..VERTICES {
34        adj[i].push(i-5);
35        if i+1 < VERTICES {
36            adj[i].push(i+1);
37        }
38    }
39    adj[9].push(5);
40
41    let mut instance = sat::Instance::new();
42
43    // For each vertex, a vector of variables for the possible colors.
44    let mut vars = vec![];
45    for i in 0..VERTICES {
46        vars.push(vec![instance.fresh_var(), instance.fresh_var(), instance.fresh_var()]);
47
48        // Assert that each vertex has at least one color.
49        // red OR green OR blue
50        instance.assert_any(&[vars[i][0], vars[i][1], vars[i][2]]);
51
52        // Assert that each vertex has at most one color.
53        // (red IMPLIES !green) =equiv= (!green OR !red)
54        for c1 in 0..COLORS {
55            for c2 in 0..c1 {
56                instance.assert_any(&[!vars[i][c1], !vars[i][c2]]);
57            }
58        }
59    }
60
61    // Assert that adjacent vertices don't have the same color.
62    for (i, js) in adj.iter().enumerate() {
63        for &j in js {
64            for c in 0..COLORS {
65                instance.assert_any(&[!vars[i][c], !vars[j][c]]);
66            }
67        }
68    }
69
70    // Solve using minisat.
71    let solver = sat::solver::Dimacs::new(|| {
72        let mut c = Command::new("minisat");
73        c.stdout(process::Stdio::null());
74        c
75    });
76
77    let solution = solver.solve(&instance).unwrap();
78
79    // Extract the colors.
80    // Make sure there's only one color per vertex.
81    let mut colors: Vec<_> = iter::repeat(None).take(VERTICES).collect();
82    for i in 0..VERTICES {
83        for c in 0..COLORS {
84            if solution.get(vars[i][c]) {
85                assert!(mem::replace(&mut colors[i], Some(c)).is_none());
86            }
87        }
88    }
89
90    // Output in GraphViz format.
91    println!("graph {{");
92    for (i, js) in adj.iter().enumerate() {
93        println!("    {} [color=\"{}\"];", i,
94            ["red", "green", "blue"][colors[i].unwrap()]);
95
96        for j in js {
97            println!("    {} -- {};", i, j);
98        }
99    }
100    println!("}}");
101}