From 10eb07972298470e77ff919a2e45f18ef7402cac Mon Sep 17 00:00:00 2001 From: Matthias Green Date: Tue, 22 Jul 2025 17:03:14 +0200 Subject: [PATCH 1/8] feat(col): Add graph coloring example to profile eq --- Cargo.lock | 7 ++++ Cargo.toml | 2 +- examples/coloring/.gitignore | 1 + examples/coloring/Cargo.toml | 7 ++++ examples/coloring/src/encode.rs | 57 ++++++++++++++++++++++++++ examples/coloring/src/main.rs | 42 +++++++++++++++++++ examples/coloring/src/parse.rs | 71 +++++++++++++++++++++++++++++++++ solver/src/model/lang/expr.rs | 9 +++++ solver/src/model/lang/int.rs | 4 ++ 9 files changed, 199 insertions(+), 1 deletion(-) create mode 100644 examples/coloring/.gitignore create mode 100644 examples/coloring/Cargo.toml create mode 100644 examples/coloring/src/encode.rs create mode 100644 examples/coloring/src/main.rs create mode 100644 examples/coloring/src/parse.rs diff --git a/Cargo.lock b/Cargo.lock index 4cde4afd4..ad80f0efb 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -483,6 +483,13 @@ version = "1.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b05b61dc5112cbb17e4b6cd61790d9845d13888356391624cbe7e41efeac1e75" +[[package]] +name = "coloring" +version = "0.1.0" +dependencies = [ + "aries", +] + [[package]] name = "crc32fast" version = "1.4.2" diff --git a/Cargo.toml b/Cargo.toml index a455327e8..82566675a 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -13,7 +13,7 @@ members = [ "examples/smt", "examples/gg", "examples/knapsack", - "validator", + "validator", "examples/coloring", ] resolver = "2" diff --git a/examples/coloring/.gitignore b/examples/coloring/.gitignore new file mode 100644 index 000000000..fda65cd8e --- /dev/null +++ b/examples/coloring/.gitignore @@ -0,0 +1 @@ +problems/* diff --git a/examples/coloring/Cargo.toml b/examples/coloring/Cargo.toml new file mode 100644 index 000000000..9d71586fe --- /dev/null +++ b/examples/coloring/Cargo.toml @@ -0,0 +1,7 @@ +[package] +name = "coloring" +version = "0.1.0" +edition = "2024" + +[dependencies] +aries = { path = "../../solver", features = ["cpu_cycles"] } diff --git a/examples/coloring/src/encode.rs b/examples/coloring/src/encode.rs new file mode 100644 index 000000000..ceb548fd8 --- /dev/null +++ b/examples/coloring/src/encode.rs @@ -0,0 +1,57 @@ +use aries::core::state::Cause; +use aries::model::Model; +use aries::model::lang::IVar; +use aries::model::lang::expr::{eq, leq, neq}; + +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 } + } +} + +pub struct Encoding { + pub n_colors: IVar, + pub nodes: Vec, +} + +impl Encoding { + pub fn new(problem: &Problem, model: &mut Model) -> Self { + // Color int representation + let min_col = 1; + let max_col = problem.nodes.len().try_into().unwrap(); + + // 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 maybe 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)) { + let lit = model.reify(neq(n1.color, n2.color)); + model.state.set(lit, Cause::Encoding).unwrap(); + } else { + model.reify(eq(n1.color, n2.color)); + } + } + } + + Encoding { n_colors, nodes } + } +} diff --git a/examples/coloring/src/main.rs b/examples/coloring/src/main.rs new file mode 100644 index 000000000..57f8a693e --- /dev/null +++ b/examples/coloring/src/main.rs @@ -0,0 +1,42 @@ +use std::{env, path::Path}; + +use aries::{ + model::Model, + solver::{ + Solver, + search::activity::{ActivityBrancher, Heuristic}, + }, +}; +use encode::Encoding; +use parse::Problem; + +mod encode; +mod parse; + +pub struct LiteralFavoringHeuristic; + +impl Heuristic for LiteralFavoringHeuristic { + fn decision_stage(&self, var: aries::core::VarRef, _: Option<&L>, model: &Model) -> u8 { + if model.state.bounds(var) == (0, 1) { 0 } else { 1 } + } +} + +fn main() { + let mut args = env::args(); + args.next().unwrap(); + 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); + solver.set_brancher(ActivityBrancher::new_with_heuristic(LiteralFavoringHeuristic {})); + 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!(); + } +} diff --git a/examples/coloring/src/parse.rs b/examples/coloring/src/parse.rs new file mode 100644 index 000000000..f8b1b184c --- /dev/null +++ b/examples/coloring/src/parse.rs @@ -0,0 +1,71 @@ +use std::{ + collections::HashSet, + fs::File, + io::{self, BufRead}, + num::ParseIntError, + path::Path, +}; + +fn read_lines(filename: &Path) -> io::Result>> { + let file = File::open(filename)?; + Ok(io::BufReader::new(file).lines()) +} + +#[derive(Default)] +pub struct Problem { + pub edges: HashSet<(Node, Node)>, + pub nodes: HashSet, + pub solution: Option, +} + +impl Problem { + fn add_edge(&mut self, node1: Node, node2: Node) { + self.nodes.insert(node1); + self.nodes.insert(node2); + self.edges.insert((node1, node2)); + } + pub fn from_file(path: &Path) -> Self { + let mut res: Problem = Default::default(); + assert!(path.is_file()); + let lines = read_lines(path).unwrap(); + 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 + } + + 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 for usize { + fn from(value: Node) -> Self { + value.0 + } +} + +impl From for Node { + fn from(value: usize) -> Self { + Node(value) + } +} + +impl TryFrom<&str> for Node { + type Error = ParseIntError; + + fn try_from(value: &str) -> Result { + usize::from_str_radix(value, 10).map(|u| u.into()) + } +} diff --git a/solver/src/model/lang/expr.rs b/solver/src/model/lang/expr.rs index 204409dce..15ff3ed11 100644 --- a/solver/src/model/lang/expr.rs +++ b/solver/src/model/lang/expr.rs @@ -196,6 +196,15 @@ impl Reifiable for Eq { } fn int_eq(a: IAtom, b: IAtom, model: &mut Model) -> 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() diff --git a/solver/src/model/lang/int.rs b/solver/src/model/lang/int.rs index cbb9d414f..ad1793917 100644 --- a/solver/src/model/lang/int.rs +++ b/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. From 453708b1dbf56b88bf9c942b987a83ffb413c0c3 Mon Sep 17 00:00:00 2001 From: Matthias Green Date: Wed, 23 Jul 2025 17:06:02 +0200 Subject: [PATCH 2/8] fix(col): Lint coloring --- examples/coloring/src/encode.rs | 1 + examples/coloring/src/main.rs | 6 +++--- examples/coloring/src/parse.rs | 3 ++- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/examples/coloring/src/encode.rs b/examples/coloring/src/encode.rs index ceb548fd8..64c7b9f3b 100644 --- a/examples/coloring/src/encode.rs +++ b/examples/coloring/src/encode.rs @@ -18,6 +18,7 @@ impl EncodedNode { pub struct Encoding { pub n_colors: IVar, + #[allow(unused)] pub nodes: Vec, } diff --git a/examples/coloring/src/main.rs b/examples/coloring/src/main.rs index 57f8a693e..bbf01037d 100644 --- a/examples/coloring/src/main.rs +++ b/examples/coloring/src/main.rs @@ -13,9 +13,9 @@ use parse::Problem; mod encode; mod parse; -pub struct LiteralFavoringHeuristic; +pub struct BooleanFavoringHeuristic; -impl Heuristic for LiteralFavoringHeuristic { +impl Heuristic for BooleanFavoringHeuristic { fn decision_stage(&self, var: aries::core::VarRef, _: Option<&L>, model: &Model) -> u8 { if model.state.bounds(var) == (0, 1) { 0 } else { 1 } } @@ -29,7 +29,7 @@ fn main() { let mut model = Model::new(); let encoding = Encoding::new(&problem, &mut model); let mut solver = Solver::new(model); - solver.set_brancher(ActivityBrancher::new_with_heuristic(LiteralFavoringHeuristic {})); + solver.set_brancher(ActivityBrancher::new_with_heuristic(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(); diff --git a/examples/coloring/src/parse.rs b/examples/coloring/src/parse.rs index f8b1b184c..6c487aaae 100644 --- a/examples/coloring/src/parse.rs +++ b/examples/coloring/src/parse.rs @@ -40,6 +40,7 @@ impl Problem { res } + #[allow(unused)] pub fn check_solution(&self, proposed_solution: u32) { if let Some(solution) = self.solution { assert_eq!(solution, proposed_solution) @@ -66,6 +67,6 @@ impl TryFrom<&str> for Node { type Error = ParseIntError; fn try_from(value: &str) -> Result { - usize::from_str_radix(value, 10).map(|u| u.into()) + value.parse::().map(|u| u.into()) } } From 0ead8d2577b786fefa5d7ed694bcd25e75203391 Mon Sep 17 00:00:00 2001 From: Matthias Green Date: Thu, 24 Jul 2025 11:36:12 +0200 Subject: [PATCH 3/8] doc(col): Add Readme to coloring --- examples/coloring/README.md | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 examples/coloring/README.md diff --git a/examples/coloring/README.md b/examples/coloring/README.md new file mode 100644 index 000000000..0dc5ce23e --- /dev/null +++ b/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). + From 01af24fcdc9a4c2cf33dc728173574f3ea00ac0a Mon Sep 17 00:00:00 2001 From: Matthias Green Date: Wed, 20 Aug 2025 16:20:20 +0200 Subject: [PATCH 4/8] perf(col): Improve graph coloring branching params --- examples/coloring/src/encode.rs | 4 ++-- examples/coloring/src/main.rs | 11 +++++++++-- examples/coloring/src/parse.rs | 13 ++++++++++++- 3 files changed, 23 insertions(+), 5 deletions(-) diff --git a/examples/coloring/src/encode.rs b/examples/coloring/src/encode.rs index 64c7b9f3b..2af1e88b5 100644 --- a/examples/coloring/src/encode.rs +++ b/examples/coloring/src/encode.rs @@ -26,7 +26,7 @@ impl Encoding { pub fn new(problem: &Problem, model: &mut Model) -> Self { // Color int representation let min_col = 1; - let max_col = problem.nodes.len().try_into().unwrap(); + let max_col = problem.upper_bound() as i32; // Total number of colros to minimize let n_colors = model.new_ivar(min_col, max_col, "n_colors"); @@ -45,7 +45,7 @@ impl Encoding { 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)) { - let lit = model.reify(neq(n1.color, n2.color)); + let lit = model.half_reify(neq(n1.color, n2.color)); model.state.set(lit, Cause::Encoding).unwrap(); } else { model.reify(eq(n1.color, n2.color)); diff --git a/examples/coloring/src/main.rs b/examples/coloring/src/main.rs index bbf01037d..63fb921e9 100644 --- a/examples/coloring/src/main.rs +++ b/examples/coloring/src/main.rs @@ -4,7 +4,7 @@ use aries::{ model::Model, solver::{ Solver, - search::activity::{ActivityBrancher, Heuristic}, + search::activity::{ActivityBrancher, BranchingParams, Heuristic}, }, }; use encode::Encoding; @@ -29,7 +29,14 @@ fn main() { let mut model = Model::new(); let encoding = Encoding::new(&problem, &mut model); let mut solver = Solver::new(model); - solver.set_brancher(ActivityBrancher::new_with_heuristic(BooleanFavoringHeuristic {})); + solver.set_brancher(ActivityBrancher::new_with( + BranchingParams { + prefer_min_value: false, + ..Default::default() + }, + BooleanFavoringHeuristic {}, + // DefaultHeuristic {}, + )); let res = solver.minimize_with_callback(encoding.n_colors, |n, _| println!("Found solution {n}")); if let Ok(Some((n_cols, _))) = res { solver.print_stats(); diff --git a/examples/coloring/src/parse.rs b/examples/coloring/src/parse.rs index 6c487aaae..438489bb9 100644 --- a/examples/coloring/src/parse.rs +++ b/examples/coloring/src/parse.rs @@ -1,5 +1,5 @@ use std::{ - collections::HashSet, + collections::{HashMap, HashSet}, fs::File, io::{self, BufRead}, num::ParseIntError, @@ -19,11 +19,22 @@ pub struct Problem { } impl Problem { + 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)); } + pub fn from_file(path: &Path) -> Self { let mut res: Problem = Default::default(); assert!(path.is_file()); From 3b9eab9f9eaf52f6bab8eb35ef75bb3225265def Mon Sep 17 00:00:00 2001 From: Matthias Green Date: Wed, 20 Aug 2025 17:46:56 +0200 Subject: [PATCH 5/8] feat(col): Add env vars to toggle options in coloring example --- Cargo.lock | 1 + examples/coloring/Cargo.toml | 1 + examples/coloring/src/encode.rs | 5 ++++- examples/coloring/src/main.rs | 22 ++++++++++++++-------- 4 files changed, 20 insertions(+), 9 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index ad80f0efb..a6ce688d5 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -488,6 +488,7 @@ name = "coloring" version = "0.1.0" dependencies = [ "aries", + "env_param", ] [[package]] diff --git a/examples/coloring/Cargo.toml b/examples/coloring/Cargo.toml index 9d71586fe..8e3cb34c5 100644 --- a/examples/coloring/Cargo.toml +++ b/examples/coloring/Cargo.toml @@ -5,3 +5,4 @@ edition = "2024" [dependencies] aries = { path = "../../solver", features = ["cpu_cycles"] } +env_param = { version = "0.1.0", path = "../../env_param" } diff --git a/examples/coloring/src/encode.rs b/examples/coloring/src/encode.rs index 2af1e88b5..36f59078b 100644 --- a/examples/coloring/src/encode.rs +++ b/examples/coloring/src/encode.rs @@ -3,6 +3,7 @@ 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 { @@ -47,8 +48,10 @@ impl Encoding { if problem.edges.contains(&(n1.node, n2.node)) || problem.edges.contains(&(n2.node, n1.node)) { let lit = model.half_reify(neq(n1.color, n2.color)); model.state.set(lit, Cause::Encoding).unwrap(); - } else { + } else if REIFY_EQ.get() { model.reify(eq(n1.color, n2.color)); + } else { + model.half_reify(eq(n1.color, n2.color)); } } } diff --git a/examples/coloring/src/main.rs b/examples/coloring/src/main.rs index 63fb921e9..3dbef92d9 100644 --- a/examples/coloring/src/main.rs +++ b/examples/coloring/src/main.rs @@ -8,11 +8,15 @@ use aries::{ }, }; use encode::Encoding; +use env_param::EnvParam; use parse::Problem; mod encode; mod parse; +pub static SPECIAL_BRANCHER: EnvParam = EnvParam::new("ARIES_COLORING_SPECIAL_BRANCHER", "true"); +pub static REIFY_EQ: EnvParam = EnvParam::new("ARIES_COLORING_REIFY_EQ", "false"); + pub struct BooleanFavoringHeuristic; impl Heuristic for BooleanFavoringHeuristic { @@ -29,14 +33,16 @@ fn main() { let mut model = Model::new(); let encoding = Encoding::new(&problem, &mut model); let mut solver = Solver::new(model); - solver.set_brancher(ActivityBrancher::new_with( - BranchingParams { - prefer_min_value: false, - ..Default::default() - }, - BooleanFavoringHeuristic {}, - // DefaultHeuristic {}, - )); + if SPECIAL_BRANCHER.get() { + solver.set_brancher(ActivityBrancher::new_with( + BranchingParams { + prefer_min_value: false, + ..Default::default() + }, + BooleanFavoringHeuristic {}, + // DefaultHeuristic {}, + )); + } let res = solver.minimize_with_callback(encoding.n_colors, |n, _| println!("Found solution {n}")); if let Ok(Some((n_cols, _))) = res { solver.print_stats(); From 6ec80c25d881a3372e40edee960c3bc8311eb44f Mon Sep 17 00:00:00 2001 From: Matthias Green Date: Mon, 25 Aug 2025 14:42:55 +0200 Subject: [PATCH 6/8] feat(col): Add script to download coloring problems --- examples/coloring/download-problems.sh | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 examples/coloring/download-problems.sh diff --git a/examples/coloring/download-problems.sh b/examples/coloring/download-problems.sh new file mode 100644 index 000000000..8197cd100 --- /dev/null +++ b/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 From a67a7e50d9f34473aa13c8777bbc0747338e79c1 Mon Sep 17 00:00:00 2001 From: Matthias Green Date: Wed, 27 Aug 2025 10:00:52 +0200 Subject: [PATCH 7/8] fix(col): Better default for env var --- examples/coloring/src/main.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/examples/coloring/src/main.rs b/examples/coloring/src/main.rs index 3dbef92d9..c4291bbf6 100644 --- a/examples/coloring/src/main.rs +++ b/examples/coloring/src/main.rs @@ -15,7 +15,7 @@ mod encode; mod parse; pub static SPECIAL_BRANCHER: EnvParam = EnvParam::new("ARIES_COLORING_SPECIAL_BRANCHER", "true"); -pub static REIFY_EQ: EnvParam = EnvParam::new("ARIES_COLORING_REIFY_EQ", "false"); +pub static REIFY_EQ: EnvParam = EnvParam::new("ARIES_COLORING_REIFY_EQ", "true"); pub struct BooleanFavoringHeuristic; @@ -40,7 +40,6 @@ fn main() { ..Default::default() }, BooleanFavoringHeuristic {}, - // DefaultHeuristic {}, )); } let res = solver.minimize_with_callback(encoding.n_colors, |n, _| println!("Found solution {n}")); From f15a3073c99d18edeabbd6772098e384f17e9e91 Mon Sep 17 00:00:00 2001 From: Matthias Green Date: Fri, 12 Sep 2025 14:32:43 +0200 Subject: [PATCH 8/8] doc(col): Document and clean up coloring --- examples/coloring/src/encode.rs | 14 +++++++++----- examples/coloring/src/main.rs | 7 ++++++- examples/coloring/src/parse.rs | 12 +++++++++++- 3 files changed, 26 insertions(+), 7 deletions(-) diff --git a/examples/coloring/src/encode.rs b/examples/coloring/src/encode.rs index 36f59078b..78251dcdf 100644 --- a/examples/coloring/src/encode.rs +++ b/examples/coloring/src/encode.rs @@ -1,3 +1,4 @@ +use aries::core::IntCst; use aries::core::state::Cause; use aries::model::Model; use aries::model::lang::IVar; @@ -17,17 +18,22 @@ impl EncodedNode { } } +/// 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, } impl Encoding { + /// Create a new encoding for a coloring problem pub fn new(problem: &Problem, model: &mut Model) -> Self { // Color int representation let min_col = 1; - let max_col = problem.upper_bound() as i32; + 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"); @@ -41,13 +47,11 @@ impl Encoding { nodes.push(EncodedNode::new(node, node_color)) } - // Mark node_color != neighbors and maybe node_color == non-neighbor - + // 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)) { - let lit = model.half_reify(neq(n1.color, n2.color)); - model.state.set(lit, Cause::Encoding).unwrap(); + model.enforce(neq(n1.color, n2.color), []); } else if REIFY_EQ.get() { model.reify(eq(n1.color, n2.color)); } else { diff --git a/examples/coloring/src/main.rs b/examples/coloring/src/main.rs index c4291bbf6..71b23a8b3 100644 --- a/examples/coloring/src/main.rs +++ b/examples/coloring/src/main.rs @@ -17,6 +17,7 @@ mod parse; pub static SPECIAL_BRANCHER: EnvParam = EnvParam::new("ARIES_COLORING_SPECIAL_BRANCHER", "true"); pub static REIFY_EQ: EnvParam = 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 Heuristic for BooleanFavoringHeuristic { @@ -27,12 +28,14 @@ impl Heuristic for BooleanFavoringHeuristic { fn main() { let mut args = env::args(); - args.next().unwrap(); + 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 { @@ -42,7 +45,9 @@ fn main() { 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!("========================="); diff --git a/examples/coloring/src/parse.rs b/examples/coloring/src/parse.rs index 438489bb9..63f42d0d9 100644 --- a/examples/coloring/src/parse.rs +++ b/examples/coloring/src/parse.rs @@ -11,6 +11,8 @@ fn read_lines(filename: &Path) -> io::Result>> { 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)>, @@ -19,6 +21,7 @@ pub struct Problem { } 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() { @@ -35,10 +38,17 @@ impl Problem { 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).unwrap(); + 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();