petersen/
petersen.rs

1//! 3-coloring the [Petersen graph].
2//!
3//! Outputs a colored graph in GraphViz format.
4//!
5//! [Petersen graph]: https://en.wikipedia.org/wiki/Petersen_graph
6
7use std::iter;
8use std::mem;
9use std::process::{self, Command};
10
11use sat::solver::Solver;
12
13extern crate sat;
14
15const VERTICES: usize = 10;
16const COLORS: usize = 3;
17
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}
petersen/petersen.rs

petersen/
petersen.rs
