Graph coloring example

Cargo.toml

@@ -13,7 +13,7 @@ members = [
     "examples/smt",
     "examples/gg",
     "examples/knapsack",
-    "validator",
+    "validator", "examples/coloring",
 ]
 resolver = "2"
 

examples/coloring/.gitignore

@@ -0,0 +1 @@
+problems/*

examples/coloring/Cargo.toml

@@ -0,0 +1,8 @@
+[package]
+name = "coloring"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]
+aries = { path = "../../solver", features = ["cpu_cycles"] }
+env_param = { version = "0.1.0", path = "../../env_param" }

examples/coloring/README.md

@@ -0,0 +1,23 @@
+# Graph coloring
+
+This crate reads a graph as a .col file and determines it's chromatic number.
+
+The input file must contain newline seperated edge declarations in the following format:
+
+e 0 1 (Declare an edge between nodes 0 and 1)
+
+Lines starting with anything other than e will be ignored.
+
+## Encoding
+
+The model contains a variable representing the chromatic number,
+a variable for each node representing it's color,
+enforced neq constraints between each pair of adjacent edges,
+and reified eq constraints between each pair of non-adjacent edges.
+
+## Brancher
+
+The default activity brancher is used with a simple heuristic which favours boolean variables.
+This favors branching on node color equality, which causes the eq reasoner to work a lot more.
+This is also very inneffective (\~200 000 decisions for FullIns3, compared to \~5 000 with no heuristic and \~100 with the opposite heuristic, branching on node color).
+

examples/coloring/download-problems.sh

@@ -0,0 +1,6 @@
+#!/usr/bin/env bash
+cd "$(dirname "$0")"
+mkdir problems
+git clone https://github.com/Cyril-Grelier/gc_instances.git
+mv gc_instances/original_graphs/* problems/
+rm -rf gc_instances

examples/coloring/src/encode.rs

@@ -0,0 +1,65 @@
+use aries::core::IntCst;
+use aries::core::state::Cause;
+use aries::model::Model;
+use aries::model::lang::IVar;
+use aries::model::lang::expr::{eq, leq, neq};
+
+use super::REIFY_EQ;
+use crate::parse::{Node, Problem};
+
+pub struct EncodedNode {
+    node: Node,
+    color: IVar,
+}
+
+impl EncodedNode {
+    pub fn new(node: Node, color: IVar) -> Self {
+        Self { node, color }
+    }
+}
+
+/// An encoding for a graph coloring problem.
+pub struct Encoding {
+    /// The chromatic number of the graph, variable to minimize.
+    pub n_colors: IVar,
+
+    /// A vec of nodes and their color
+    #[allow(unused)]
+    pub nodes: Vec<EncodedNode>,
+}
+
+impl Encoding {
+    /// Create a new encoding for a coloring problem
+    pub fn new(problem: &Problem, model: &mut Model<String>) -> Self {
+        // Color int representation
+        let min_col = 1;
+        let max_col = problem.upper_bound() as IntCst;
+
+        // Total number of colros to minimize
+        let n_colors = model.new_ivar(min_col, max_col, "n_colors");
+
+        // Mark node color <= n_colors
+        let mut nodes = vec![];
+        for node in problem.nodes.clone() {
+            let node_color = model.new_ivar(min_col, max_col, format!("Node {} col", usize::from(node)));
+            let lit = model.reify(leq(node_color, n_colors));
+            model.state.set(lit, Cause::Encoding).unwrap();
+            nodes.push(EncodedNode::new(node, node_color))
+        }
+
+        // Mark node_color != neighbors and node_color == non-neighbor
+        for (i, n1) in nodes.iter().enumerate() {
+            for n2 in &nodes[i + 1..] {
+                if problem.edges.contains(&(n1.node, n2.node)) || problem.edges.contains(&(n2.node, n1.node)) {
+                    model.enforce(neq(n1.color, n2.color), []);
+                } else if REIFY_EQ.get() {
+                    model.reify(eq(n1.color, n2.color));
+                } else {
+                    model.half_reify(eq(n1.color, n2.color));
+                }
+            }
+        }
+
+        Encoding { n_colors, nodes }
+    }
+}

examples/coloring/src/main.rs

@@ -0,0 +1,59 @@
+use std::{env, path::Path};
+
+use aries::{
+    model::Model,
+    solver::{
+        Solver,
+        search::activity::{ActivityBrancher, BranchingParams, Heuristic},
+    },
+};
+use encode::Encoding;
+use env_param::EnvParam;
+use parse::Problem;
+
+mod encode;
+mod parse;
+
+pub static SPECIAL_BRANCHER: EnvParam<bool> = EnvParam::new("ARIES_COLORING_SPECIAL_BRANCHER", "true");
+pub static REIFY_EQ: EnvParam<bool> = EnvParam::new("ARIES_COLORING_REIFY_EQ", "true");
+
+/// A heuristic to be used by the ActivityBrancher which favours decisions on "boolean" variables
+pub struct BooleanFavoringHeuristic;
+
+impl<L> Heuristic<L> for BooleanFavoringHeuristic {
+    fn decision_stage(&self, var: aries::core::VarRef, _: Option<&L>, model: &Model<L>) -> u8 {
+        if model.state.bounds(var) == (0, 1) { 0 } else { 1 }
+    }
+}
+
+fn main() {
+    let mut args = env::args();
+    args.next().expect("Provide a file path as an argument.");
+    let path = args.next().unwrap();
+
+    let problem = Problem::from_file(Path::new(&path));
+    let mut model = Model::new();
+    let encoding = Encoding::new(&problem, &mut model);
+    let mut solver = Solver::new(model);
+
+    if SPECIAL_BRANCHER.get() {
+        solver.set_brancher(ActivityBrancher::new_with(
+            BranchingParams {
+                prefer_min_value: false,
+                ..Default::default()
+            },
+            BooleanFavoringHeuristic {},
+        ));
+    }
+
+    let res = solver.minimize_with_callback(encoding.n_colors, |n, _| println!("Found solution {n}"));
+
+    if let Ok(Some((n_cols, _))) = res {
+        solver.print_stats();
+        println!("=========================");
+        println!("Found solution: {} colors", n_cols);
+        println!("=========================");
+    } else {
+        panic!();
+    }
+}

examples/coloring/src/parse.rs

@@ -0,0 +1,93 @@
+use std::{
+    collections::{HashMap, HashSet},
+    fs::File,
+    io::{self, BufRead},
+    num::ParseIntError,
+    path::Path,
+};
+
+fn read_lines(filename: &Path) -> io::Result<io::Lines<io::BufReader<File>>> {
+    let file = File::open(filename)?;
+    Ok(io::BufReader::new(file).lines())
+}
+
+/// A graph represented as a set of nodes and a set of edges.
+/// May optionally be have a know chromatic number.
+#[derive(Default)]
+pub struct Problem {
+    pub edges: HashSet<(Node, Node)>,
+    pub nodes: HashSet<Node>,
+    pub solution: Option<u32>,
+}
+
+impl Problem {
+    /// Get an upper bound on the number of colors.
+    pub fn upper_bound(&self) -> u32 {
+        let mut n_edges = HashMap::new();
+        for (source, target) in self.edges.iter() {
+            n_edges.entry(source).and_modify(|x| *x += 1).or_insert(1);
+            n_edges.entry(target).and_modify(|x| *x += 1).or_insert(1);
+        }
+        n_edges.into_values().max().unwrap() + 1
+    }
+
+    fn add_edge(&mut self, node1: Node, node2: Node) {
+        assert!(!self.edges.contains(&(node2, node1)));
+        self.nodes.insert(node1);
+        self.nodes.insert(node2);
+        self.edges.insert((node1, node2));
+    }
+
+    /// Load a problem from a .col file
+    ///
+    /// The file must contain a newline seperated list of edges, e.g.:
+    /// e 0 1
+    /// e 1 2
+    ///
+    /// Everything else is ignored
+    pub fn from_file(path: &Path) -> Self {
+        let mut res: Problem = Default::default();
+        assert!(path.is_file());
+        let lines = read_lines(path).expect("File provided was not able to be read.");
+        for line in lines.map_while(Result::ok) {
+            if line.starts_with("e") {
+                let mut split = line.split_whitespace();
+                split.next().unwrap();
+                let node1 = split.next().unwrap().try_into().unwrap();
+                let node2 = split.next().unwrap().try_into().unwrap();
+                res.add_edge(node1, node2);
+            }
+        }
+        res
+    }
+
+    #[allow(unused)]
+    pub fn check_solution(&self, proposed_solution: u32) {
+        if let Some(solution) = self.solution {
+            assert_eq!(solution, proposed_solution)
+        }
+    }
+}
+
+#[derive(Debug, PartialEq, Eq, Hash, Copy, Clone)]
+pub struct Node(usize);
+
+impl From<Node> for usize {
+    fn from(value: Node) -> Self {
+        value.0
+    }
+}
+
+impl From<usize> for Node {
+    fn from(value: usize) -> Self {
+        Node(value)
+    }
+}
+
+impl TryFrom<&str> for Node {
+    type Error = ParseIntError;
+
+    fn try_from(value: &str) -> Result<Self, Self::Error> {
+        value.parse::<usize>().map(|u| u.into())
+    }
+}

solver/src/model/lang/expr.rs

@@ -196,6 +196,15 @@ impl<Lbl: Label> Reifiable<Lbl> for Eq {
 }
 
 fn int_eq<Lbl: Label>(a: IAtom, b: IAtom, model: &mut Model<Lbl>) -> ReifExpr {
+    if USE_EQUALITY_LOGIC.get() {
+        if a.is_const() && !b.is_const() && b.shift == 0 {
+            return ReifExpr::EqVal(b.var.into(), a.shift);
+        } else if b.is_const() && !a.is_const() && a.shift == 0 {
+            return ReifExpr::EqVal(a.var.into(), b.shift);
+        } else if !b.is_const() && !a.is_const() && a.shift == 0 && b.shift == 0 {
+            return ReifExpr::Eq(a.var.into(), b.var.into());
+        }
+    }
     let lr = model.reify(leq(a, b));
     let rl = model.reify(leq(b, a));
     and([lr, rl]).into()

solver/src/model/lang/int.rs

@@ -113,6 +113,10 @@ impl IAtom {
     pub fn ge_lit(self, value: IntCst) -> Lit {
         self.gt_lit(value - 1)
     }
+
+    pub fn is_const(&self) -> bool {
+        self.var == IVar::ZERO
+    }
 }
 
 /// Comparison on the values that can be taken for two atoms.