diff --git a/explainability/src/musmcs_enumeration/marco/mod.rs b/explainability/src/musmcs_enumeration/marco/mod.rs index 99c853cc..3061110a 100644 --- a/explainability/src/musmcs_enumeration/marco/mod.rs +++ b/explainability/src/musmcs_enumeration/marco/mod.rs @@ -8,6 +8,14 @@ use aries::model::{Label, Model}; use aries::reif::Reifiable; use std::collections::BTreeSet; +/// A trait describing the basic functions needed to implement the MARCO algorithm, +/// and providing an abstract implementation based on them. +/// +/// NOTE: For now, we only have one concrete implementation (SimpleMarco), +/// so we could remove the trait and only use that concrete implementation. +/// However, this trait may become useful later if we try to implement parallel MARCO. +/// Additionally, one could argue this trait helps with readability / understanding the +/// correspondence between the code and the pseudo-code. pub trait Marco { fn new_with_soft_constrs_reif_lits( model: Model, @@ -54,8 +62,6 @@ trait MapSolver { fn block_down(&mut self, sat_subset: &BTreeSet); fn block_up(&mut self, unsat_subset: &BTreeSet); - - // fn get_internal_solver(&mut self) -> &mut Solver; } trait SubsetSolver { @@ -64,8 +70,6 @@ trait SubsetSolver { fn grow(&mut self, seed: &BTreeSet) -> (BTreeSet, Option>); fn shrink(&mut self, seed: &BTreeSet) -> BTreeSet; - - // fn get_internal_solver(&mut self) -> &mut Solver; } #[cfg(test)] diff --git a/explainability/src/musmcs_enumeration/marco/simple_marco.rs b/explainability/src/musmcs_enumeration/marco/simple_marco.rs index 4c1feb99..349b40df 100644 --- a/explainability/src/musmcs_enumeration/marco/simple_marco.rs +++ b/explainability/src/musmcs_enumeration/marco/simple_marco.rs @@ -1,12 +1,15 @@ use aries::backtrack::Backtrack; -use aries::core::{Lit, INT_CST_MAX}; -use aries::model::extensions::AssignmentExt; +use aries::core::{Lit, SignedVar, VarRef, INT_CST_MAX, INT_CST_MIN}; +use aries::model::extensions::{AssignmentExt, SavedAssignment}; use aries::model::lang::expr::or; use aries::model::lang::linear::LinearSum; use aries::model::lang::IAtom; use aries::model::{Label, Model}; use aries::reasoners::stn::theory::{StnConfig, TheoryPropagationLevel}; use aries::reif::Reifiable; +use aries::solver::search::combinators::CombinatorExt; +use aries::solver::search::lexical::Lexical; +use aries::solver::search::SearchControl; use aries::solver::Solver; use itertools::Itertools; @@ -18,52 +21,183 @@ use std::sync::Arc; struct SimpleMapSolver { s: Solver, + /// Maps the variables of the literals representing the soft constraints in the subset solver to those of the map solver (self). + vars_translate_in: BTreeMap, + /// Maps the variables of the literals representing the soft constraints in the map solver (self) to those of the subset solver. + vars_translate_out: BTreeMap, literals: BTreeSet, - to_max: IAtom, - 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. + solve_fn: Box) -> Option>>, +} + +fn signed_var_of_same_sign(var: VarRef, svar: SignedVar) -> SignedVar { + if svar.is_plus() { + SignedVar::plus(var) + } else if svar.is_minus() { + SignedVar::minus(var) + } else { + panic!() + } } 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(); - - for literal in literals { - let lit = model.state.new_var(0, 1).geq(1); - lits_translate_in.insert(literal, lit); - lits_translate_out.insert(lit, literal); - } - - 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()); - model.enforce(literals_sum.clone().leq(to_max), []); - model.enforce(literals_sum.geq(to_max), []); - - model.enforce(or(literals.iter().cloned().collect_vec()), []); + let mut vars_translate_in = BTreeMap::::new(); + let mut vars_translate_out = BTreeMap::::new(); + + // Literals representing the soft constraints + let literals = literals + .into_iter() + .map(|lit| { + let v = model.state.new_var(INT_CST_MIN, INT_CST_MAX); + + vars_translate_in.insert(lit.variable(), v); + vars_translate_out.insert(v, lit.variable()); + + Lit::new(signed_var_of_same_sign(v, lit.svar()), lit.ub_value()) + }) + .collect::>(); + + // TODO do preferred values instead of maximize. + // TODO option to use minimize. (for "low bias") + // TODO cardinality-like constraints ? (another of possible liffiton optimizations) + + let mut s = Solver::::new(model); + + // FIXME usage of strings is dirty / temporary + let solving_mode = "PREFERRED_VALUES_HIGH"; + + // Approaches for finding / solving for unexplored seeds. + // + // "High" bias approaches are more likely to discover UNSAT seeds early (since they will be larger), thus favoring finding MUSes early. + // "Low" bias approaches are more likely to discover SAT seeds early (since they will be smaller), thus favoring finding MCSes early. + // + // This can be done by maximizing (high) or minimizing (low) the cardinality / sum of literals' indicator variables. + // Another functionally equivalent approach - expected to be more performant - is to inform the solver + // of our default / preferred values for the literals' indicator variables (0 - low, 1 - high). + let solve_fn: Box) -> Option>> = match solving_mode { + // Optimize the sum of the literals' indicator variables. (Maximize for high bias) + "OPTIMIZE_HIGH" => { + let sum = LinearSum::of( + literals + .iter() + .map(|&l| { + let v = s.model.state.new_var(0, 1); + s.model.bind(l, v.geq(1)); + + IAtom::from(v) + }) + .collect_vec(), + ); + let obj = IAtom::from(s.model.state.new_var(0, INT_CST_MAX)); + s.model.enforce(sum.geq(obj), []); + + Box::new( + move |_s: &mut Solver| { + (*_s).maximize(obj).expect("Solver interrupted").map(|(_, doms)| doms) + } + ) + } + // Optimize the sum of the literals' indicator variables. (Minimize for low bias) + "OPTIMIZE_LOW" => { + let sum = LinearSum::of( + literals + .iter() + .map(|&l| { + let v = s.model.state.new_var(0, 1); + s.model.bind(l, v.geq(1)); + + IAtom::from(v) + }) + .collect_vec(), + ); + let obj = IAtom::from(s.model.state.new_var(0, INT_CST_MAX)); + s.model.enforce(sum.leq(obj), []); + + Box::new( + move |_s: &mut Solver| { + (*_s).minimize(obj).expect("Solver interrupted").map(|(_, doms)| doms) + } + ) + } + // Ask the solver to, if possible, set the literals to true (high bias). + "PREFERRED_VALUES_HIGH" => { + let brancher = Lexical::with_vars( + literals.iter().map(|&l| { + let v = s.model.state.new_var(0, 1); + s.model.bind(l, v.geq(1)); + v + }), + aries::solver::search::lexical::PreferredValue::Max, + ) + .clone_to_box() + .and_then(s.brancher.clone_to_box()); + + s.set_brancher_boxed(brancher); + + Box::new(move |_s: &mut Solver| (*_s).solve().expect("Solver interrupted")) + } + // Ask the solver to, if possible, set the literals to false (low bias). + "PREFERRED_VALUES_LOW" => { + let brancher = Lexical::with_vars( + literals.iter().map(|&l| { + let v = s.model.state.new_var(0, 1); + s.model.bind(l, v.geq(1)); + v + }), + aries::solver::search::lexical::PreferredValue::Min, + ) + .clone_to_box() + .and_then(s.brancher.clone_to_box()); + + s.set_brancher_boxed(brancher); + + Box::new(move |_s: &mut Solver| (*_s).solve().expect("Solver interrupted")) + } + // Unoptimised approach, any solutions. + "NOTHING" => { + Box::new(move |_s: &mut Solver| (*_s).solve().expect("Solver interrupted")) + } + _ => panic!() + }; + // s.model.enforce(or(literals.iter().copied().collect_vec()), []); // Could adding this be any useful for performance ? SimpleMapSolver { - s: Solver::::new(model), + s, + vars_translate_in, + vars_translate_out, literals, - to_max, - lits_translate_in, - lits_translate_out, + solve_fn, } } + + /// Translates a soft constraint reification literal from its subset solver representation to its map solver representation. + fn translate_lit_in(&self, literal: Lit) -> Lit { + Lit::new( + signed_var_of_same_sign(self.vars_translate_in[&literal.variable()], literal.svar()), + literal.ub_value(), + ) + } + + /// Translates a soft constraint reification literal from its map solver representation to its subset solver representation. + fn translate_lit_out(&self, literal: Lit) -> Lit { + Lit::new( + signed_var_of_same_sign(self.vars_translate_out[&literal.variable()], literal.svar()), + literal.ub_value(), + ) + } } impl MapSolver for SimpleMapSolver { fn find_unexplored_seed(&mut self) -> Option> { - match self.s.maximize(self.to_max).unwrap() { - Some((_, best_assignment)) => { + match (self.solve_fn)(&mut self.s) { + Some(best_assignment) => { let seed = Some( self.literals .iter() .filter(|&&l| best_assignment.entails(l)) - .map(|&l| self.lits_translate_out[&l]) + .map(|&l| self.translate_lit_out(l)) .collect(), ); self.s.reset(); @@ -77,28 +211,25 @@ impl MapSolver for SimpleMapSolver { } fn block_down(&mut self, sat_subset: &BTreeSet) { - let complement = self - .literals - .difference(&sat_subset.iter().map(|&l| self.lits_translate_in[&l]).collect()) - .cloned() - .collect_vec(); - self.s.enforce(or(complement), []); + let translated_sat_subset = sat_subset.iter().map(|&l| self.translate_lit_in(l)).collect(); + let translated_sat_subset_complement = self.literals.difference(&translated_sat_subset).copied().collect_vec(); + self.s.enforce(or(translated_sat_subset_complement), []); } 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), []); + let translated_unsat_subset_negs = unsat_subset.iter().map(|&l| self.translate_lit_in(!l)).collect_vec(); + self.s.enforce(or(translated_unsat_subset_negs), []); } - - // fn get_internal_solver(&mut self) -> &mut Solver { - // &mut self.s - // } } struct SimpleSubsetSolver { s: Solver, soft_constrs_reif_lits: Arc>, + /// The latest unsat core computed in `check_seed_sat` (in the `false` return case). cached_unsat_core: BTreeSet, + /// Used for an optimization. Set of (soft constraint reification) literals + /// that have been found to constitute a singleton MCS, i.e. belonging to all MUSes. + necessarily_in_all_muses: BTreeSet, } impl SimpleSubsetSolver { @@ -114,6 +245,7 @@ impl SimpleSubsetSolver { s, soft_constrs_reif_lits, cached_unsat_core: BTreeSet::new(), + necessarily_in_all_muses: BTreeSet::new(), } } } @@ -123,12 +255,17 @@ impl SubsetSolver for SimpleSubsetSolver { // FIXME warm-start / solution hints optimization should go here... right ? let res = self .s - .solve_with_assumptions(seed.iter().cloned()) + .solve_with_assumptions(seed.iter().copied()) .expect("Solver interrupted..."); self.s.reset(); + if let Err(unsat_core) = res { - self.cached_unsat_core.clear(); - self.cached_unsat_core.extend(unsat_core.literals()); + self.cached_unsat_core = unsat_core + .literals() + .into_iter() + .chain(&self.necessarily_in_all_muses) + .copied() + .collect(); false } else { true @@ -143,7 +280,13 @@ impl SubsetSolver for SimpleSubsetSolver { mss.remove(&lit); } } - let mcs: BTreeSet = self.soft_constrs_reif_lits.difference(&mss).cloned().collect(); + let mcs: BTreeSet = self.soft_constrs_reif_lits.difference(&mss).copied().collect(); + + // If the found correction set only has 1 element, + // then that element is added to those that are known to be in all unsatisfiable sets. + if mcs.len() == 1 { + self.necessarily_in_all_muses.insert(mcs.first().unwrap().clone()); + } (mss, Some(mcs)) } @@ -153,6 +296,11 @@ impl SubsetSolver for SimpleSubsetSolver { if !mus.contains(&lit) { continue; } + // Optimization: if the literal has been determined to belong to all muses, + // no need to check if, without it, the set would be satisfiable (because it obviously would be). + if self.necessarily_in_all_muses.contains(&lit) { + continue; + } mus.remove(&lit); if !self.check_seed_sat(&mus) { mus = self.cached_unsat_core.clone(); @@ -163,14 +311,9 @@ impl SubsetSolver for SimpleSubsetSolver { } mus } - - // fn get_internal_solver(&mut self) -> &mut Solver { - // &mut self.s - // } } pub struct SimpleMarco { - // config: MusMcsEnumerationConfig, cached_result: MusMcsEnumerationResult, seed: BTreeSet, map_solver: SimpleMapSolver, @@ -201,11 +344,10 @@ impl Marco for SimpleMarco { 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 map_solver = SimpleMapSolver::new(soft_constrs_reif_lits.iter().copied()); let subset_solver = SimpleSubsetSolver::::new(model, soft_constrs_reif_lits.clone()); Self { - // config, cached_result, seed: BTreeSet::new(), map_solver, @@ -262,34 +404,7 @@ impl Marco for SimpleMarco { self.map_solver.block_down(&mss); mcses.push(mcs.unwrap()); } else { - // 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 - .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(); - 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(); + self.case_seed_sat_only_muses_optimization(); } } @@ -301,3 +416,60 @@ impl Marco for SimpleMarco { } } } + +impl SimpleMarco { + fn case_seed_sat_only_muses_optimization(&mut self) { + // 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). + // + // This can only be done when we only intend to return MUSes, not MCSes, + // because the correction sets we greedily discover with this optimization + // have no guarantee of being unique / not having been already discovered. + + let mut sat_subset = self.seed.clone(); + self.map_solver.block_down(&sat_subset); + + // Another optimization (*): + // If the found correction set only has 1 element, + // then that element is added to those that are known to be in all unsatisfiable sets. + if let Some(&lit) = self + .soft_constrs_reif_lits + .difference(&sat_subset) + .take(2) + .fold(None, |opt, item| opt.xor(Some(item))) + { + self.subset_solver.necessarily_in_all_muses.insert(lit); + } + + // Grow the sat subset as much as possible (i.e. until unsatisfiability + // by extending it with each correction set discovered. + while self + .subset_solver + .s + .solve_with_assumptions(sat_subset.iter().copied()) + .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)) + .copied() + .collect(); + self.map_solver.block_down(&new_sat_subset); + + let new_corr_subset = self.soft_constrs_reif_lits.difference(&new_sat_subset).into_iter(); + sat_subset.extend(new_corr_subset.clone()); + + // Same optimization as (*) above + if let Some(&lit) = new_corr_subset.take(2).fold(None, |opt, item| opt.xor(Some(item))) { + self.subset_solver.necessarily_in_all_muses.insert(lit); + } + + self.subset_solver.s.reset(); + } + self.subset_solver.s.reset(); + } +}