From 36f05d0656487aff9d031e82658025af2ee9be61 Mon Sep 17 00:00:00 2001 From: Trevor Hansen Date: Thu, 28 Dec 2023 16:37:01 +1100 Subject: [PATCH 01/10] better ilp extractor --- src/extract/ilp_cbc.rs | 232 ++++++++++++++--------------------------- src/main.rs | 2 + 2 files changed, 78 insertions(+), 156 deletions(-) diff --git a/src/extract/ilp_cbc.rs b/src/extract/ilp_cbc.rs index c48b04b..90e7462 100644 --- a/src/extract/ilp_cbc.rs +++ b/src/extract/ilp_cbc.rs @@ -1,11 +1,17 @@ -use core::panic; +/* An ILP extractor that returns the optimal DAG-extraction. + +This extractor is simple so that it's easy to see that it's correct. + +If the timeout is reached, it will return the result of the faster-greedy-dag extractor. +*/ + +// Without a timeout, some will take > 10 hours to finish. +const SOLVING_TIME_LIMIT_SECONDS: u64 = 10; use super::*; use coin_cbc::{Col, Model, Sense}; use indexmap::IndexSet; -const INITIALISE_WITH_BOTTOM_UP: bool = false; - struct ClassVars { active: Col, nodes: Vec, @@ -17,20 +23,14 @@ impl Extractor for CbcExtractor { fn extract(&self, egraph: &EGraph, roots: &[ClassId]) -> ExtractionResult { let mut model = Model::default(); - let true_literal = model.add_binary(); - model.set_col_lower(true_literal, 1.0); + model.set_parameter("seconds", &SOLVING_TIME_LIMIT_SECONDS.to_string()); let vars: IndexMap = egraph .classes() .values() .map(|class| { let cvars = ClassVars { - active: if roots.contains(&class.id) { - // Roots must be active. - true_literal - } else { - model.add_binary() - }, + active: model.add_binary(), nodes: class.nodes.iter().map(|_| model.add_binary()).collect(), }; (class.id.clone(), cvars) @@ -56,60 +56,24 @@ impl Extractor for CbcExtractor { .collect::>() }; - let mut intersection: IndexSet = - childrens_classes_var(egraph[class_id].nodes[0].clone()); - - for node in &egraph[class_id].nodes[1..] { - intersection = intersection - .intersection(&childrens_classes_var(node.clone())) - .cloned() - .collect(); - } - - // A class being active implies that all in the intersection - // of it's children are too. - for c in &intersection { - let row = model.add_row(); - model.set_row_upper(row, 0.0); - model.set_weight(row, class.active, 1.0); - model.set_weight(row, *c, -1.0); - } - for (node_id, &node_active) in egraph[class_id].nodes.iter().zip(&class.nodes) { for child_active in childrens_classes_var(node_id.clone()) { // node active implies child active, encoded as: // node_active <= child_active // node_active - child_active <= 0 - if !intersection.contains(&child_active) { - let row = model.add_row(); - model.set_row_upper(row, 0.0); - model.set_weight(row, node_active, 1.0); - model.set_weight(row, child_active, -1.0); - } + let row = model.add_row(); + model.set_row_upper(row, 0.0); + model.set_weight(row, node_active, 1.0); + model.set_weight(row, child_active, -1.0); } } } model.set_obj_sense(Sense::Minimize); for class in egraph.classes().values() { - let min_cost = class - .nodes - .iter() - .map(|n_id| egraph[n_id].cost) - .min() - .unwrap_or(Cost::default()) - .into_inner(); - - // Most helpful when the members of the class all have the same cost. - // For example if the members' costs are [1,1,1], three terms get - // replaced by one in the objective function. - if min_cost != 0.0 { - model.set_obj_coeff(vars[&class.id].active, min_cost); - } - for (node_id, &node_active) in class.nodes.iter().zip(&vars[&class.id].nodes) { let node = &egraph[node_id]; - let node_cost = node.cost.into_inner() - min_cost; + let node_cost = node.cost.into_inner(); assert!(node_cost >= 0.0); if node_cost != 0.0 { @@ -118,36 +82,11 @@ impl Extractor for CbcExtractor { } } - // set initial solution based on bottom up extractor - if INITIALISE_WITH_BOTTOM_UP { - let initial_result = super::bottom_up::BottomUpExtractor.extract(egraph, roots); - for (class, class_vars) in egraph.classes().values().zip(vars.values()) { - if let Some(node_id) = initial_result.choices.get(&class.id) { - model.set_col_initial_solution(class_vars.active, 1.0); - for col in &class_vars.nodes { - model.set_col_initial_solution(*col, 0.0); - } - let node_idx = class.nodes.iter().position(|n| n == node_id).unwrap(); - model.set_col_initial_solution(class_vars.nodes[node_idx], 1.0); - } else { - model.set_col_initial_solution(class_vars.active, 0.0); - } - } + for root in roots { + model.set_col_lower(vars[root].active, 1.0); } - let mut banned_cycles: IndexSet<(ClassId, usize)> = Default::default(); - find_cycles(egraph, |id, i| { - banned_cycles.insert((id, i)); - }); - for (class_id, class_vars) in &vars { - for (i, &node_active) in class_vars.nodes.iter().enumerate() { - if banned_cycles.contains(&(class_id.clone(), i)) { - model.set_col_upper(node_active, 0.0); - model.set_col_lower(node_active, 0.0); - } - } - } - log::info!("@blocked {}", banned_cycles.len()); + block_cycles(&mut model, &vars, &egraph); let solution = model.solve(); log::info!( @@ -157,6 +96,13 @@ impl Extractor for CbcExtractor { solution.raw().obj_value(), ); + if solution.raw().status() != coin_cbc::raw::Status::Finished { + let initial_result = + super::faster_greedy_dag::FasterGreedyDagExtractor.extract(egraph, roots); + log::info!("Unfinished CBC solution"); + return initial_result; + } + let mut result = ExtractionResult::default(); for (id, var) in &vars { @@ -172,96 +118,70 @@ impl Extractor for CbcExtractor { } } - let cycles = result.find_cycles(egraph, roots); - assert!(cycles.is_empty()); return result; } } -// from @khaki3 -// fixes bug in egg 0.9.4's version -// https://github.com/egraphs-good/egg/issues/207#issuecomment-1264737441 -fn find_cycles(egraph: &EGraph, mut f: impl FnMut(ClassId, usize)) { - let mut pending: IndexMap> = IndexMap::default(); - - let mut order: IndexMap = IndexMap::default(); - - let mut memo: IndexMap<(ClassId, usize), bool> = IndexMap::default(); - - let mut stack: Vec<(ClassId, usize)> = vec![]; - - let n2c = |nid: &NodeId| egraph.nid_to_cid(nid); - - for class in egraph.classes().values() { - let id = &class.id; - for (i, node_id) in egraph[id].nodes.iter().enumerate() { - let node = &egraph[node_id]; - for child in &node.children { - let child = n2c(child).clone(); - pending - .entry(child) - .or_insert_with(Vec::new) - .push((id.clone(), i)); - } +fn block_cycles(model: &mut Model, vars: &IndexMap, egraph: &EGraph) { + let mut levels: IndexMap = Default::default(); + for c in vars.keys() { + levels.insert(c.clone(), model.add_integer()); + } - if node.is_leaf() { - stack.push((id.clone(), i)); - } + // If n.variable is true, opposite_col will be false and vice versa. + let mut opposite: IndexMap = Default::default(); + for c in vars.values() { + for n in &c.nodes { + let opposite_col = model.add_binary(); + opposite.insert(*n, opposite_col); + let row = model.add_row(); + model.set_row_equal(row, 1.0); + model.set_weight(row, opposite_col, 1.0); + model.set_weight(row, *n, 1.0); } } - let mut count = 0; + for (class_id, c) in vars { + model.set_col_lower(*levels.get(class_id).unwrap(), 0.0); + model.set_col_upper(*levels.get(class_id).unwrap(), vars.len() as f64); - while let Some((id, i)) = stack.pop() { - if memo.get(&(id.clone(), i)).is_some() { - continue; - } + for i in 0..c.nodes.len() { + let n_id = &egraph[class_id].nodes[i]; + let n = &egraph[n_id]; + let var = c.nodes[i]; - let node_id = &egraph[&id].nodes[i]; - let node = &egraph[node_id]; - let mut update = false; - - if node.is_leaf() { - update = true; - } else if node.children.iter().all(|x| order.get(n2c(x)).is_some()) { - if let Some(ord) = order.get(&id) { - update = node.children.iter().all(|x| &order[n2c(x)] < ord); - if !update { - memo.insert((id, i), false); - continue; - } - } else { - update = true; + let children_classes = n + .children + .iter() + .map(|n| egraph[n].eclass.clone()) + .collect::>(); + + if children_classes.contains(class_id) { + // Self loop - disable this node. + // This is clumsier than calling set_col_lower(var,0.0), + // but means it'll be infeasible (rather than producing an + // incorrect solution) if var corresponds to a root node. + let row = model.add_row(); + model.set_weight(row, var, 1.0); + model.set_row_equal(row, 0.0); + continue; } - } - if update { - if order.get(&id).is_none() { - if egraph[node_id].is_leaf() { - order.insert(id.clone(), 0); - } else { - order.insert(id.clone(), count); - count += 1; - } - } - memo.insert((id.clone(), i), true); - if let Some(mut v) = pending.remove(&id) { - stack.append(&mut v); - stack.sort(); - stack.dedup(); - }; - } - } + for cc in children_classes { + assert!(*levels.get(class_id).unwrap() != *levels.get(&cc).unwrap()); - for class in egraph.classes().values() { - let id = &class.id; - for (i, node) in class.nodes.iter().enumerate() { - if let Some(true) = memo.get(&(id.clone(), i)) { - continue; + let row = model.add_row(); + model.set_row_upper(row, -1.0); + model.set_weight(row, *levels.get(class_id).unwrap(), 1.0); + model.set_weight(row, *levels.get(&cc).unwrap(), -1.0); + + // If n.variable is 0, then disable the contraint. + model.set_weight( + row, + *opposite.get(&var).unwrap(), + -((vars.len() + 1) as f64), + ); } - assert!(!egraph[node].is_leaf()); - f(id.clone(), i); } } - assert!(pending.is_empty()); } diff --git a/src/main.rs b/src/main.rs index bddc552..ddaed2f 100644 --- a/src/main.rs +++ b/src/main.rs @@ -36,6 +36,8 @@ fn main() { "global-greedy-dag", extract::global_greedy_dag::GlobalGreedyDagExtractor.boxed(), ), + #[cfg(feature = "ilp-cbc")] + ("ilp-cbc", extract::ilp_cbc::CbcExtractor.boxed()), ] .into_iter() .collect(); From 8c1f9d7fb203a2df932d37f876cb11f62332ca9a Mon Sep 17 00:00:00 2001 From: Trevor Hansen Date: Mon, 1 Jan 2024 13:30:21 +1100 Subject: [PATCH 02/10] Separate extractor with timeout and without timeout --- src/extract/ilp_cbc.rs | 188 ++++++++++++++++++++++------------------- 1 file changed, 100 insertions(+), 88 deletions(-) diff --git a/src/extract/ilp_cbc.rs b/src/extract/ilp_cbc.rs index 90e7462..cfbe6c0 100644 --- a/src/extract/ilp_cbc.rs +++ b/src/extract/ilp_cbc.rs @@ -5,9 +5,6 @@ This extractor is simple so that it's easy to see that it's correct. If the timeout is reached, it will return the result of the faster-greedy-dag extractor. */ -// Without a timeout, some will take > 10 hours to finish. -const SOLVING_TIME_LIMIT_SECONDS: u64 = 10; - use super::*; use coin_cbc::{Col, Model, Sense}; use indexmap::IndexSet; @@ -18,108 +15,123 @@ struct ClassVars { } pub struct CbcExtractor; +pub struct CbcExtractorWithTimeout; + +impl Extractor for CbcExtractorWithTimeout { + fn extract(egraph: &EGraph, roots: &[ClassId]) -> ExtractionResult { + // Without a timeout, some will take > 10 hours to finish. + const SOLVING_TIME_LIMIT_SECONDS: u32 = 10; + return extract(egraph, roots, SOLVING_TIME_LIMIT_SECONDS); + } +} impl Extractor for CbcExtractor { fn extract(&self, egraph: &EGraph, roots: &[ClassId]) -> ExtractionResult { - let mut model = Model::default(); - - model.set_parameter("seconds", &SOLVING_TIME_LIMIT_SECONDS.to_string()); - - let vars: IndexMap = egraph - .classes() - .values() - .map(|class| { - let cvars = ClassVars { - active: model.add_binary(), - nodes: class.nodes.iter().map(|_| model.add_binary()).collect(), - }; - (class.id.clone(), cvars) - }) - .collect(); - - for (class_id, class) in &vars { - // class active == some node active - // sum(for node_active in class) == class_active - let row = model.add_row(); - model.set_row_equal(row, 0.0); - model.set_weight(row, class.active, -1.0); - for &node_active in &class.nodes { - model.set_weight(row, node_active, 1.0); - } + return extract(egraph, roots, std::u32::MAX); + } +} + +fn extract(egraph: &EGraph, roots: &[ClassId], timeout_seconds: u32) -> ExtractionResult { + let mut model = Model::default(); - let childrens_classes_var = |nid: NodeId| { - egraph[&nid] - .children - .iter() - .map(|n| egraph[n].eclass.clone()) - .map(|n| vars[&n].active) - .collect::>() + model.set_parameter("seconds", &timeout_seconds.to_string()); + + let vars: IndexMap = egraph + .classes() + .values() + .map(|class| { + let cvars = ClassVars { + active: model.add_binary(), + nodes: class.nodes.iter().map(|_| model.add_binary()).collect(), }; + (class.id.clone(), cvars) + }) + .collect(); + + for (class_id, class) in &vars { + // class active == some node active + // sum(for node_active in class) == class_active + let row = model.add_row(); + model.set_row_equal(row, 0.0); + model.set_weight(row, class.active, -1.0); + for &node_active in &class.nodes { + model.set_weight(row, node_active, 1.0); + } - for (node_id, &node_active) in egraph[class_id].nodes.iter().zip(&class.nodes) { - for child_active in childrens_classes_var(node_id.clone()) { - // node active implies child active, encoded as: - // node_active <= child_active - // node_active - child_active <= 0 - let row = model.add_row(); - model.set_row_upper(row, 0.0); - model.set_weight(row, node_active, 1.0); - model.set_weight(row, child_active, -1.0); - } + let childrens_classes_var = |nid: NodeId| { + egraph[&nid] + .children + .iter() + .map(|n| egraph[n].eclass.clone()) + .map(|n| vars[&n].active) + .collect::>() + }; + + for (node_id, &node_active) in egraph[class_id].nodes.iter().zip(&class.nodes) { + for child_active in childrens_classes_var(node_id.clone()) { + // node active implies child active, encoded as: + // node_active <= child_active + // node_active - child_active <= 0 + let row = model.add_row(); + model.set_row_upper(row, 0.0); + model.set_weight(row, node_active, 1.0); + model.set_weight(row, child_active, -1.0); } } + } - model.set_obj_sense(Sense::Minimize); - for class in egraph.classes().values() { - for (node_id, &node_active) in class.nodes.iter().zip(&vars[&class.id].nodes) { - let node = &egraph[node_id]; - let node_cost = node.cost.into_inner(); - assert!(node_cost >= 0.0); + model.set_obj_sense(Sense::Minimize); + for class in egraph.classes().values() { + for (node_id, &node_active) in class.nodes.iter().zip(&vars[&class.id].nodes) { + let node = &egraph[node_id]; + let node_cost = node.cost.into_inner(); + assert!(node_cost >= 0.0); - if node_cost != 0.0 { - model.set_obj_coeff(node_active, node_cost); - } + if node_cost != 0.0 { + model.set_obj_coeff(node_active, node_cost); } } + } - for root in roots { - model.set_col_lower(vars[root].active, 1.0); - } + for root in roots { + model.set_col_lower(vars[root].active, 1.0); + } - block_cycles(&mut model, &vars, &egraph); - - let solution = model.solve(); - log::info!( - "CBC status {:?}, {:?}, obj = {}", - solution.raw().status(), - solution.raw().secondary_status(), - solution.raw().obj_value(), - ); - - if solution.raw().status() != coin_cbc::raw::Status::Finished { - let initial_result = - super::faster_greedy_dag::FasterGreedyDagExtractor.extract(egraph, roots); - log::info!("Unfinished CBC solution"); - return initial_result; - } + block_cycles(&mut model, &vars, &egraph); - let mut result = ExtractionResult::default(); - - for (id, var) in &vars { - let active = solution.col(var.active) > 0.0; - if active { - let node_idx = var - .nodes - .iter() - .position(|&n| solution.col(n) > 0.0) - .unwrap(); - let node_id = egraph[id].nodes[node_idx].clone(); - result.choose(id.clone(), node_id); - } - } + let solution = model.solve(); + log::info!( + "CBC status {:?}, {:?}, obj = {}", + solution.raw().status(), + solution.raw().secondary_status(), + solution.raw().obj_value(), + ); - return result; + if solution.raw().status() != coin_cbc::raw::Status::Finished { + assert(timeout != std::u32::MAX); + + let initial_result = + super::faster_greedy_dag::FasterGreedyDagExtractor.extract(egraph, roots); + log::info!("Unfinished CBC solution"); + return initial_result; } + + let mut result = ExtractionResult::default(); + + for (id, var) in &vars { + let active = solution.col(var.active) > 0.0; + if active { + let node_idx = var + .nodes + .iter() + .position(|&n| solution.col(n) > 0.0) + .unwrap(); + let node_id = egraph[id].nodes[node_idx].clone(); + result.choose(id.clone(), node_id); + } + } + + return result; } fn block_cycles(model: &mut Model, vars: &IndexMap, egraph: &EGraph) { From a2e2b6deddc3b73659539f038ecd6911407979e9 Mon Sep 17 00:00:00 2001 From: Trevor Hansen Date: Mon, 1 Jan 2024 13:46:24 +1100 Subject: [PATCH 03/10] fix build. enable ilp-cbc by default --- Cargo.toml | 1 + src/extract/ilp_cbc.rs | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 367fb50..3463ca1 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -7,6 +7,7 @@ version = "0.1.0" [features] ilp-cbc = ["coin_cbc"] +default = ["ilp-cbc"] [dependencies] env_logger = { version = "0.10.0", default-features = false } diff --git a/src/extract/ilp_cbc.rs b/src/extract/ilp_cbc.rs index cfbe6c0..7941e68 100644 --- a/src/extract/ilp_cbc.rs +++ b/src/extract/ilp_cbc.rs @@ -18,7 +18,7 @@ pub struct CbcExtractor; pub struct CbcExtractorWithTimeout; impl Extractor for CbcExtractorWithTimeout { - fn extract(egraph: &EGraph, roots: &[ClassId]) -> ExtractionResult { + fn extract(&self, egraph: &EGraph, roots: &[ClassId]) -> ExtractionResult { // Without a timeout, some will take > 10 hours to finish. const SOLVING_TIME_LIMIT_SECONDS: u32 = 10; return extract(egraph, roots, SOLVING_TIME_LIMIT_SECONDS); @@ -108,7 +108,7 @@ fn extract(egraph: &EGraph, roots: &[ClassId], timeout_seconds: u32) -> Extracti ); if solution.raw().status() != coin_cbc::raw::Status::Finished { - assert(timeout != std::u32::MAX); + assert!(timeout_seconds != std::u32::MAX); let initial_result = super::faster_greedy_dag::FasterGreedyDagExtractor.extract(egraph, roots); From af94572ea61937f4cb17c7ac52b0be2e2f8f311a Mon Sep 17 00:00:00 2001 From: Trevor Hansen Date: Mon, 1 Jan 2024 13:51:22 +1100 Subject: [PATCH 04/10] fix to use ilp-cbc with timeout --- src/main.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/main.rs b/src/main.rs index ddaed2f..c0e5e0c 100644 --- a/src/main.rs +++ b/src/main.rs @@ -37,7 +37,10 @@ fn main() { extract::global_greedy_dag::GlobalGreedyDagExtractor.boxed(), ), #[cfg(feature = "ilp-cbc")] - ("ilp-cbc", extract::ilp_cbc::CbcExtractor.boxed()), + ( + "ilp-cbc-timeout", + extract::ilp_cbc::CbcExtractorWithTimeout.boxed(), + ), ] .into_iter() .collect(); From 9486d8e916876340d55fa573fd8ca18271b9c195 Mon Sep 17 00:00:00 2001 From: Trevor Hansen Date: Mon, 1 Jan 2024 14:13:37 +1100 Subject: [PATCH 05/10] Move the timeout to the caller --- src/extract/ilp_cbc.rs | 11 +++++------ src/main.rs | 6 +++--- 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/src/extract/ilp_cbc.rs b/src/extract/ilp_cbc.rs index 7941e68..db1acc9 100644 --- a/src/extract/ilp_cbc.rs +++ b/src/extract/ilp_cbc.rs @@ -14,17 +14,16 @@ struct ClassVars { nodes: Vec, } -pub struct CbcExtractor; -pub struct CbcExtractorWithTimeout; +pub struct CbcExtractorWithTimeout; -impl Extractor for CbcExtractorWithTimeout { +impl Extractor for CbcExtractorWithTimeout { fn extract(&self, egraph: &EGraph, roots: &[ClassId]) -> ExtractionResult { - // Without a timeout, some will take > 10 hours to finish. - const SOLVING_TIME_LIMIT_SECONDS: u32 = 10; - return extract(egraph, roots, SOLVING_TIME_LIMIT_SECONDS); + return extract(egraph, roots, TIMEOUT_IN_SECONDS); } } +pub struct CbcExtractor; + impl Extractor for CbcExtractor { fn extract(&self, egraph: &EGraph, roots: &[ClassId]) -> ExtractionResult { return extract(egraph, roots, std::u32::MAX); diff --git a/src/main.rs b/src/main.rs index c0e5e0c..8e8a1d5 100644 --- a/src/main.rs +++ b/src/main.rs @@ -32,14 +32,14 @@ fn main() { "faster-greedy-dag", extract::faster_greedy_dag::FasterGreedyDagExtractor.boxed(), ), - ( + /*( "global-greedy-dag", extract::global_greedy_dag::GlobalGreedyDagExtractor.boxed(), - ), + ),*/ #[cfg(feature = "ilp-cbc")] ( "ilp-cbc-timeout", - extract::ilp_cbc::CbcExtractorWithTimeout.boxed(), + extract::ilp_cbc::CbcExtractorWithTimeout::<10>.boxed(), ), ] .into_iter() From 0a36b035a7074abcb4a39c5a20c52d20d48bf2b6 Mon Sep 17 00:00:00 2001 From: Trevor Hansen Date: Mon, 1 Jan 2024 14:22:06 +1100 Subject: [PATCH 06/10] Removing cbc because I don't have permission to install cbc during github workflow --- Cargo.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cargo.toml b/Cargo.toml index 3463ca1..dc565cf 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -7,7 +7,7 @@ version = "0.1.0" [features] ilp-cbc = ["coin_cbc"] -default = ["ilp-cbc"] + [dependencies] env_logger = { version = "0.10.0", default-features = false } From af2eeaa96dc50349e4bebd69a72d49bb45f94f51 Mon Sep 17 00:00:00 2001 From: Trevor Hansen Date: Mon, 1 Jan 2024 15:07:10 +1100 Subject: [PATCH 07/10] re-enable global-greedy-dag --- src/main.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main.rs b/src/main.rs index 8e8a1d5..fab1624 100644 --- a/src/main.rs +++ b/src/main.rs @@ -32,10 +32,10 @@ fn main() { "faster-greedy-dag", extract::faster_greedy_dag::FasterGreedyDagExtractor.boxed(), ), - /*( + ( "global-greedy-dag", extract::global_greedy_dag::GlobalGreedyDagExtractor.boxed(), - ),*/ + ), #[cfg(feature = "ilp-cbc")] ( "ilp-cbc-timeout", From 8619f7fc891236970fea57fcd81690950e791f28 Mon Sep 17 00:00:00 2001 From: Trevor Hansen Date: Tue, 2 Jan 2024 09:42:28 +1100 Subject: [PATCH 08/10] add description of how cycles are blocked --- Cargo.lock | 7 +++++++ Cargo.toml | 1 - src/extract/ilp_cbc.rs | 13 +++++++++++++ 3 files changed, 20 insertions(+), 1 deletion(-) diff --git a/Cargo.lock b/Cargo.lock index 46f2e35..707fbcd 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -93,6 +93,7 @@ dependencies = [ "ordered-float", "pico-args", "rpds", + "rustc-hash", ] [[package]] @@ -237,6 +238,12 @@ dependencies = [ "archery", ] +[[package]] +name = "rustc-hash" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "08d43f7aa6b08d49f382cde6a7982047c3426db949b1424bc4b7ec9ae12c6ce2" + [[package]] name = "ryu" version = "1.0.14" diff --git a/Cargo.toml b/Cargo.toml index dc565cf..367fb50 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -8,7 +8,6 @@ version = "0.1.0" [features] ilp-cbc = ["coin_cbc"] - [dependencies] env_logger = { version = "0.10.0", default-features = false } indexmap = "2.0.0" diff --git a/src/extract/ilp_cbc.rs b/src/extract/ilp_cbc.rs index db1acc9..eb2697b 100644 --- a/src/extract/ilp_cbc.rs +++ b/src/extract/ilp_cbc.rs @@ -133,6 +133,19 @@ fn extract(egraph: &EGraph, roots: &[ClassId], timeout_seconds: u32) -> Extracti return result; } +/* + + To block cycles, we enforce that a topological ordering exists on the extraction. + Each class is mapped to an integer variable (called its level). Then for each node, + we add a constraint that if a node is active, then the level of the class the node + belongs to must be less than than the level of each of the node's children. + + To create a cycle, the levels would need to decrease, so they're blocked. For example, + given a two class cycle: if class A, has level 'l', and class B has level 'm', then + 'l' must be less than 'm', but because there is also an active node in class B that + has class A as a child, 'm' must be less than 'l', which is a contradiction. +*/ + fn block_cycles(model: &mut Model, vars: &IndexMap, egraph: &EGraph) { let mut levels: IndexMap = Default::default(); for c in vars.keys() { From 4be170de653967cfef863046cc7828690683208f Mon Sep 17 00:00:00 2001 From: Trevor Hansen Date: Thu, 4 Jan 2024 01:06:49 +1100 Subject: [PATCH 09/10] Following the suggestion of @mwillsey to use floats rather than integers for the levels --- src/extract/ilp_cbc.rs | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/src/extract/ilp_cbc.rs b/src/extract/ilp_cbc.rs index eb2697b..ef3a2ec 100644 --- a/src/extract/ilp_cbc.rs +++ b/src/extract/ilp_cbc.rs @@ -136,9 +136,9 @@ fn extract(egraph: &EGraph, roots: &[ClassId], timeout_seconds: u32) -> Extracti /* To block cycles, we enforce that a topological ordering exists on the extraction. - Each class is mapped to an integer variable (called its level). Then for each node, + Each class is mapped to a variable (called its level). Then for each node, we add a constraint that if a node is active, then the level of the class the node - belongs to must be less than than the level of each of the node's children. + belongs to must be less than than the level of each of the node's children. To create a cycle, the levels would need to decrease, so they're blocked. For example, given a two class cycle: if class A, has level 'l', and class B has level 'm', then @@ -149,7 +149,11 @@ fn extract(egraph: &EGraph, roots: &[ClassId], timeout_seconds: u32) -> Extracti fn block_cycles(model: &mut Model, vars: &IndexMap, egraph: &EGraph) { let mut levels: IndexMap = Default::default(); for c in vars.keys() { - levels.insert(c.clone(), model.add_integer()); + let var = model.add_col(); + levels.insert(c.clone(), var); + //model.set_col_lower(var, 0.0); + // It solves the benchmarks about 5% faster without this + //model.set_col_upper(var, vars.len() as f64); } // If n.variable is true, opposite_col will be false and vice versa. @@ -166,9 +170,6 @@ fn block_cycles(model: &mut Model, vars: &IndexMap, egraph: } for (class_id, c) in vars { - model.set_col_lower(*levels.get(class_id).unwrap(), 0.0); - model.set_col_upper(*levels.get(class_id).unwrap(), vars.len() as f64); - for i in 0..c.nodes.len() { let n_id = &egraph[class_id].nodes[i]; let n = &egraph[n_id]; @@ -195,15 +196,15 @@ fn block_cycles(model: &mut Model, vars: &IndexMap, egraph: assert!(*levels.get(class_id).unwrap() != *levels.get(&cc).unwrap()); let row = model.add_row(); - model.set_row_upper(row, -1.0); - model.set_weight(row, *levels.get(class_id).unwrap(), 1.0); - model.set_weight(row, *levels.get(&cc).unwrap(), -1.0); + model.set_row_lower(row, 1.0); + model.set_weight(row, *levels.get(class_id).unwrap(), -1.0); + model.set_weight(row, *levels.get(&cc).unwrap(), 1.0); // If n.variable is 0, then disable the contraint. model.set_weight( row, *opposite.get(&var).unwrap(), - -((vars.len() + 1) as f64), + (vars.len() +1) as f64, ); } } From 931c3b5c4e8e840b9af4972bf3067832d411bd79 Mon Sep 17 00:00:00 2001 From: Trevor Hansen Date: Thu, 4 Jan 2024 01:25:42 +1100 Subject: [PATCH 10/10] fix layout --- src/extract/ilp_cbc.rs | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/extract/ilp_cbc.rs b/src/extract/ilp_cbc.rs index ef3a2ec..82522bd 100644 --- a/src/extract/ilp_cbc.rs +++ b/src/extract/ilp_cbc.rs @@ -201,11 +201,7 @@ fn block_cycles(model: &mut Model, vars: &IndexMap, egraph: model.set_weight(row, *levels.get(&cc).unwrap(), 1.0); // If n.variable is 0, then disable the contraint. - model.set_weight( - row, - *opposite.get(&var).unwrap(), - (vars.len() +1) as f64, - ); + model.set_weight(row, *opposite.get(&var).unwrap(), (vars.len() + 1) as f64); } } }