sat 0.1.0

Interface for defining and solving SAT problems
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101

//! 3-coloring the [Petersen graph].
//!
//! Outputs a colored graph in GraphViz format.
//!
//! [Petersen graph]: https://en.wikipedia.org/wiki/Petersen_graph

use std::iter;
use std::mem;
use std::process::{self, Command};

use sat::solver::Solver;

extern crate sat;

const VERTICES: usize = 10;
const COLORS: usize = 3;

fn main() {
    // For each vertex, the list of adjacent vertices.
    let mut adj: Vec<_> = iter::repeat(vec![]).take(VERTICES).collect();

    // Inner 5 vertices
    for i in 0..5 {
        if i+2 < 5 {
            adj[i].push(i+2);
        }
        if i+3 < 5 {
            adj[i].push(i+3);
        }
    }

    // Outer 5 vertices
    for i in 5..VERTICES {
        adj[i].push(i-5);
        if i+1 < VERTICES {
            adj[i].push(i+1);
        }
    }
    adj[9].push(5);

    let mut instance = sat::Instance::new();

    // For each vertex, a vector of variables for the possible colors.
    let mut vars = vec![];
    for i in 0..VERTICES {
        vars.push(vec![instance.fresh_var(), instance.fresh_var(), instance.fresh_var()]);

        // Assert that each vertex has at least one color.
        // red OR green OR blue
        instance.assert_any(&[vars[i][0], vars[i][1], vars[i][2]]);

        // Assert that each vertex has at most one color.
        // (red IMPLIES !green) =equiv= (!green OR !red)
        for c1 in 0..COLORS {
            for c2 in 0..c1 {
                instance.assert_any(&[!vars[i][c1], !vars[i][c2]]);
            }
        }
    }

    // Assert that adjacent vertices don't have the same color.
    for (i, js) in adj.iter().enumerate() {
        for &j in js {
            for c in 0..COLORS {
                instance.assert_any(&[!vars[i][c], !vars[j][c]]);
            }
        }
    }

    // Solve using minisat.
    let solver = sat::solver::Dimacs::new(|| {
        let mut c = Command::new("minisat");
        c.stdout(process::Stdio::null());
        c
    });

    let solution = solver.solve(&instance).unwrap();

    // Extract the colors.
    // Make sure there's only one color per vertex.
    let mut colors: Vec<_> = iter::repeat(None).take(VERTICES).collect();
    for i in 0..VERTICES {
        for c in 0..COLORS {
            if solution.get(vars[i][c]) {
                assert!(mem::replace(&mut colors[i], Some(c)).is_none());
            }
        }
    }

    // Output in GraphViz format.
    println!("graph {{");
    for (i, js) in adj.iter().enumerate() {
        println!("    {} [color=\"{}\"];", i,
            ["red", "green", "blue"][colors[i].unwrap()]);

        for j in js {
            println!("    {} -- {};", i, j);
        }
    }
    println!("}}");
}