From d0c5f0722eedc0fae4b86c81d15473c1c7f41b06 Mon Sep 17 00:00:00 2001 From: Nika Beriachvili Date: Wed, 1 Jan 2025 02:52:22 +0100 Subject: [PATCH 1/6] refactor(model): change return type `Result` (no custom error) to `Option` --- solver/src/model/model_impl.rs | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/solver/src/model/model_impl.rs b/solver/src/model/model_impl.rs index d46e5ab8..e97bec56 100644 --- a/solver/src/model/model_impl.rs +++ b/solver/src/model/model_impl.rs @@ -454,14 +454,10 @@ impl Model { } } - pub fn check_reified>(&mut self, expr: Expr) -> Result { + pub fn check_reified>(&mut self, expr: Expr) -> Option { let decomposed = &mut expr.decompose(self); self.simplify(decomposed); - if let Some(l) = self.shape.expressions.interned(&decomposed) { - Ok(l) - } else { - Err(()) - } + self.shape.expressions.interned(decomposed) } /// Enforce the given expression to be true whenever all literals of the scope are true. From 4288f00e2bcbf6b445f126646febc504f5096450 Mon Sep 17 00:00:00 2001 From: Nika Beriachvili Date: Fri, 3 Jan 2025 13:21:52 +0100 Subject: [PATCH 2/6] refactor(expl): change `Vec` parameters in MARCO to `impl IntoIterator` --- .../src/musmcs_enumeration/marco/mod.rs | 4 ++-- .../musmcs_enumeration/marco/simple_marco.rs | 21 +++++++------------ 2 files changed, 9 insertions(+), 16 deletions(-) diff --git a/explainability/src/musmcs_enumeration/marco/mod.rs b/explainability/src/musmcs_enumeration/marco/mod.rs index a7cba001..8b8dd480 100644 --- a/explainability/src/musmcs_enumeration/marco/mod.rs +++ b/explainability/src/musmcs_enumeration/marco/mod.rs @@ -11,13 +11,13 @@ use std::collections::BTreeSet; pub trait Marco { fn new_with_soft_constrs_reif_lits( model: Model, - soft_constrs_reif_lits: Vec, + soft_constrs_reif_lits: impl IntoIterator, config: MusMcsEnumerationConfig, ) -> Self; fn new_with_soft_constrs>( model: Model, - soft_constrs: Vec, + soft_constrs: impl IntoIterator, config: MusMcsEnumerationConfig, ) -> Self; diff --git a/explainability/src/musmcs_enumeration/marco/simple_marco.rs b/explainability/src/musmcs_enumeration/marco/simple_marco.rs index a63e9bce..3e7c04b4 100644 --- a/explainability/src/musmcs_enumeration/marco/simple_marco.rs +++ b/explainability/src/musmcs_enumeration/marco/simple_marco.rs @@ -25,7 +25,7 @@ struct SimpleMapSolver { } impl SimpleMapSolver { - fn new(literals: Vec) -> Self { + fn new(literals: impl IntoIterator) -> Self { let mut model = Model::new(); let mut lits_translate_in = BTreeMap::::new(); let mut lits_translate_out = BTreeMap::::new(); @@ -128,7 +128,7 @@ impl SubsetSolver for SimpleSubsetSolver { // FIXME warm-start / solution hints optimization should go here... right ? let res = self .s - .solve_with_assumptions(seed.into_iter().cloned()) + .solve_with_assumptions(seed.iter().cloned()) .expect("Solver interrupted..."); self.s.reset(); if let Err(unsat_core) = res { @@ -186,7 +186,7 @@ pub struct SimpleMarco { impl Marco for SimpleMarco { fn new_with_soft_constrs_reif_lits( model: Model, - soft_constrs_reifs_lits: Vec, + soft_constrs_reif_lits: impl IntoIterator, config: MusMcsEnumerationConfig, ) -> Self { @@ -205,12 +205,9 @@ impl Marco for SimpleMarco { debug_assert_eq!(cached_result.muses.is_some(), config.return_muses); debug_assert_eq!(cached_result.mcses.is_some(), config.return_mcses); - let map_solver = SimpleMapSolver::new(soft_constrs_reifs_lits.clone()); - - let soft_constrs_reif_lits = Arc::new( - BTreeSet::from_iter(soft_constrs_reifs_lits.into_iter()) - ); + let soft_constrs_reif_lits = Arc::new(BTreeSet::from_iter(soft_constrs_reif_lits)); + let map_solver = SimpleMapSolver::new(soft_constrs_reif_lits.iter().cloned()); let subset_solver = SimpleSubsetSolver::::new(model, soft_constrs_reif_lits.clone()); Self { @@ -225,15 +222,11 @@ impl Marco for SimpleMarco { fn new_with_soft_constrs>( model: Model, - soft_constrs: Vec, + soft_constrs: impl IntoIterator, config: MusMcsEnumerationConfig, ) -> Self { - let mut model = model.clone(); - let soft_constrs_reif_lits = soft_constrs - .into_iter() - .map(|expr| model.reify(expr)) - .collect_vec(); + let soft_constrs_reif_lits = soft_constrs.into_iter().map(|expr| model.reify(expr)).collect_vec(); Self::new_with_soft_constrs_reif_lits(model, soft_constrs_reif_lits, config) } From 92aa36a2da630fbe0d9f70fda42f05469053c030 Mon Sep 17 00:00:00 2001 From: Nika Beriachvili Date: Fri, 3 Jan 2025 13:25:15 +0100 Subject: [PATCH 3/6] chore: fix signature refactor of `get_expr_reif_lit` --- explainability/src/musmcs_enumeration/marco/mod.rs | 2 +- explainability/src/musmcs_enumeration/marco/simple_marco.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/explainability/src/musmcs_enumeration/marco/mod.rs b/explainability/src/musmcs_enumeration/marco/mod.rs index 8b8dd480..9b319bd2 100644 --- a/explainability/src/musmcs_enumeration/marco/mod.rs +++ b/explainability/src/musmcs_enumeration/marco/mod.rs @@ -25,7 +25,7 @@ pub trait Marco { fn clone_result(&self) -> MusMcsEnumerationResult; - fn get_expr_reif_lit>(&mut self, soft_constr: Expr) -> Result; + fn get_expr_reif_lit>(&mut self, soft_constr: Expr) -> Option; fn find_unexplored_seed(&mut self) -> bool; diff --git a/explainability/src/musmcs_enumeration/marco/simple_marco.rs b/explainability/src/musmcs_enumeration/marco/simple_marco.rs index 3e7c04b4..00e2550b 100644 --- a/explainability/src/musmcs_enumeration/marco/simple_marco.rs +++ b/explainability/src/musmcs_enumeration/marco/simple_marco.rs @@ -244,7 +244,7 @@ impl Marco for SimpleMarco { self.cached_result.clone() } - fn get_expr_reif_lit>(&mut self, soft_constr: Expr) -> Result { + fn get_expr_reif_lit>(&mut self, soft_constr: Expr) -> Option { self.subset_solver.s.model.check_reified(soft_constr) } From 7fc2c065fe136bd3e9ebed39a52f626fba7a1353 Mon Sep 17 00:00:00 2001 From: Nika Beriachvili Date: Fri, 3 Jan 2025 13:26:09 +0100 Subject: [PATCH 4/6] chore: style and lits --- .../musmcs_enumeration/marco/simple_marco.rs | 24 +++++++------------ 1 file changed, 9 insertions(+), 15 deletions(-) diff --git a/explainability/src/musmcs_enumeration/marco/simple_marco.rs b/explainability/src/musmcs_enumeration/marco/simple_marco.rs index 00e2550b..643e1a8f 100644 --- a/explainability/src/musmcs_enumeration/marco/simple_marco.rs +++ b/explainability/src/musmcs_enumeration/marco/simple_marco.rs @@ -20,15 +20,15 @@ struct SimpleMapSolver { s: Solver, literals: BTreeSet, to_max: IAtom, - lits_translate_in: BTreeMap, // Needed to translate / map the soft constraint reification literals in - lits_translate_out: BTreeMap, // the subset solver to their counterparts in the map solver (this one). + lits_translate_in: BTreeMap, // Maps the soft constraint reification literals of the subset solver to those of the map solver (self). + lits_translate_out: BTreeMap, // Maps the soft constraint reification literals of the map solver (self) to those of the subset solver. } impl SimpleMapSolver { fn new(literals: impl IntoIterator) -> Self { let mut model = Model::new(); let mut lits_translate_in = BTreeMap::::new(); - let mut lits_translate_out = BTreeMap::::new(); + let mut lits_translate_out = BTreeMap::::new(); for literal in literals { let lit = model.state.new_var(0, 1).geq(1); @@ -37,14 +37,9 @@ impl SimpleMapSolver { } let literals: BTreeSet = lits_translate_out.keys().cloned().collect(); - + let to_max = IAtom::from(model.state.new_var(0, INT_CST_MAX)); - let literals_sum = LinearSum::of( - literals - .iter() - .map(|&l| IAtom::from(l.variable())) - .collect_vec(), - ); + let literals_sum = LinearSum::of(literals.iter().map(|&l| IAtom::from(l.variable())).collect_vec()); model.enforce(literals_sum.clone().leq(to_max), []); model.enforce(literals_sum.geq(to_max), []); @@ -67,8 +62,8 @@ impl MapSolver for SimpleMapSolver { let seed = Some( self.literals .iter() - .filter(|&l| best_assignment.entails(*l)) - .map(|l| self.lits_translate_out[l]) + .filter(|&&l| best_assignment.entails(l)) + .map(|&l| self.lits_translate_out[&l]) .collect(), ); self.s.reset(); @@ -175,7 +170,7 @@ impl SubsetSolver for SimpleSubsetSolver { } pub struct SimpleMarco { -// config: MusMcsEnumerationConfig, + // config: MusMcsEnumerationConfig, cached_result: MusMcsEnumerationResult, seed: BTreeSet, map_solver: SimpleMapSolver, @@ -189,7 +184,6 @@ impl Marco for SimpleMarco { soft_constrs_reif_lits: impl IntoIterator, config: MusMcsEnumerationConfig, ) -> Self { - let cached_result = MusMcsEnumerationResult { muses: if config.return_muses { Some(Vec::>::new()) @@ -211,7 +205,7 @@ impl Marco for SimpleMarco { let subset_solver = SimpleSubsetSolver::::new(model, soft_constrs_reif_lits.clone()); Self { -// config, + // config, cached_result, seed: BTreeSet::new(), map_solver, From 41b18d97ae44359b438c85ee10eb69b6954aac7a Mon Sep 17 00:00:00 2001 From: Nika Beriachvili Date: Fri, 3 Jan 2025 13:27:12 +0100 Subject: [PATCH 5/6] refactor(expl): change parameter names in `block_down` and `block_up` --- explainability/src/musmcs_enumeration/marco/mod.rs | 4 ++-- .../src/musmcs_enumeration/marco/simple_marco.rs | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/explainability/src/musmcs_enumeration/marco/mod.rs b/explainability/src/musmcs_enumeration/marco/mod.rs index 9b319bd2..99c853cc 100644 --- a/explainability/src/musmcs_enumeration/marco/mod.rs +++ b/explainability/src/musmcs_enumeration/marco/mod.rs @@ -51,9 +51,9 @@ pub trait Marco { trait MapSolver { fn find_unexplored_seed(&mut self) -> Option>; - fn block_down(&mut self, frompoint: &BTreeSet); + fn block_down(&mut self, sat_subset: &BTreeSet); - fn block_up(&mut self, frompoint: &BTreeSet); + fn block_up(&mut self, unsat_subset: &BTreeSet); // fn get_internal_solver(&mut self) -> &mut Solver; } diff --git a/explainability/src/musmcs_enumeration/marco/simple_marco.rs b/explainability/src/musmcs_enumeration/marco/simple_marco.rs index 643e1a8f..0db63bde 100644 --- a/explainability/src/musmcs_enumeration/marco/simple_marco.rs +++ b/explainability/src/musmcs_enumeration/marco/simple_marco.rs @@ -76,17 +76,17 @@ impl MapSolver for SimpleMapSolver { } } - fn block_down(&mut self, frompoint: &BTreeSet) { + fn block_down(&mut self, sat_subset: &BTreeSet) { let complement = self .literals - .difference(&frompoint.iter().map(|&l| self.lits_translate_in[&l]).collect()) + .difference(&sat_subset.iter().map(|&l| self.lits_translate_in[&l]).collect()) .cloned() .collect_vec(); self.s.enforce(or(complement), []); } - fn block_up(&mut self, frompoint: &BTreeSet) { - let neg = frompoint.iter().map(|&l| !self.lits_translate_in[&l]).collect_vec(); + fn block_up(&mut self, unsat_subset: &BTreeSet) { + let neg = unsat_subset.iter().map(|&l| !self.lits_translate_in[&l]).collect_vec(); self.s.enforce(or(neg), []); } From c2137d85b82580839679d17528763d9b6f831c1b Mon Sep 17 00:00:00 2001 From: Nika Beriachvili Date: Fri, 3 Jan 2025 13:28:56 +0100 Subject: [PATCH 6/6] fix(expl): fix bug in an optional optimization in MARCO (greedy correction sets) --- .../musmcs_enumeration/marco/simple_marco.rs | 46 ++++++++----------- 1 file changed, 20 insertions(+), 26 deletions(-) diff --git a/explainability/src/musmcs_enumeration/marco/simple_marco.rs b/explainability/src/musmcs_enumeration/marco/simple_marco.rs index 0db63bde..4c1feb99 100644 --- a/explainability/src/musmcs_enumeration/marco/simple_marco.rs +++ b/explainability/src/musmcs_enumeration/marco/simple_marco.rs @@ -262,40 +262,34 @@ impl Marco for SimpleMarco { self.map_solver.block_down(&mss); mcses.push(mcs.unwrap()); } else { - // from Ignace Bleukx's implementation: - // find more MCSes, **disjoint** from this one, similar to "optimal_mus" in mus.py - // can only be done when MCSes do not have to be returned as there is no guarantee - // the MCSes encountered during enumeration are "new" MCSes - let mut sat_subset_lits: BTreeSet = self.soft_constrs_reif_lits - .iter() - .filter(|&&l| self.subset_solver.s.model.entails(!l)) - .cloned() - .collect(); - self.map_solver + // Small optimization inspired by the implementation of Ignace Bleukx (in python). + // If we are not going to return MCSes, we can try to greedily search for + // more correction subsets, disjoint from this one (the seed). + + let mut sat_subset = self.seed.clone(); + self.map_solver.block_down(&sat_subset); + + while self + .subset_solver .s - .enforce(or( - sat_subset_lits - .iter() - .map(|&l| self.map_solver.lits_translate_in[&l]) - .collect_vec() - ), []); - while self.subset_solver.check_seed_sat(&sat_subset_lits) { - let s2: BTreeSet = self + .solve_with_assumptions(sat_subset.iter().cloned()) + .expect("Solver interrupted...") + .is_ok() + { + let new_sat_subset: BTreeSet = self .soft_constrs_reif_lits .iter() .filter(|&&l| self.subset_solver.s.model.entails(l)) .cloned() .collect(); - let new_mcs = self.soft_constrs_reif_lits.difference(&s2).cloned(); - sat_subset_lits.extend(new_mcs.clone()); - self.map_solver.s - .enforce(or( - new_mcs - .map(|l| self.map_solver.lits_translate_in[&l]) - .collect_vec() - ), []); + self.map_solver.block_down(&new_sat_subset); + + let new_corr_subset = self.soft_constrs_reif_lits.difference(&new_sat_subset); + sat_subset.extend(new_corr_subset); + self.subset_solver.s.reset(); } + self.subset_solver.s.reset(); } }