From 957f11f818133e148ceb558be6b7c8ea752c9445 Mon Sep 17 00:00:00 2001 From: Nika Beriachvili Date: Sat, 21 Dec 2024 23:11:31 +0100 Subject: [PATCH 01/16] feat(solver): add "assumption" cause type --- solver/src/core/state/cause.rs | 6 ++++++ solver/src/core/state/domains.rs | 6 +++--- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/solver/src/core/state/cause.rs b/solver/src/core/state/cause.rs index 8241e4ff..57c98d75 100644 --- a/solver/src/core/state/cause.rs +++ b/solver/src/core/state/cause.rs @@ -8,6 +8,8 @@ use crate::reasoners::ReasonerId; pub enum Cause { /// Event caused by a decision. Decision, + /// Event caused by an assumption. + Assumption, /// Event that resulted from the encoding of a constraint. /// This should only occur at the root decision level. Encoding, @@ -32,6 +34,7 @@ impl From for DirectOrigin { fn from(c: Cause) -> Self { match c { Cause::Decision => DirectOrigin::Decision, + Cause::Assumption => DirectOrigin::Assumption, Cause::Encoding => DirectOrigin::Encoding, Cause::Inference(i) => DirectOrigin::ExternalInference(i), } @@ -42,6 +45,7 @@ impl From for Origin { fn from(c: Cause) -> Self { match c { Cause::Decision => Origin::Direct(DirectOrigin::Decision), + Cause::Assumption => Origin::Direct(DirectOrigin::Assumption), Cause::Encoding => Origin::Direct(DirectOrigin::Encoding), Cause::Inference(i) => Origin::Direct(DirectOrigin::ExternalInference(i)), } @@ -75,6 +79,7 @@ pub enum Origin { } impl Origin { pub const DECISION: Origin = Origin::Direct(DirectOrigin::Decision); + pub const ASSUMPTION: Origin = Origin::Direct(DirectOrigin::Assumption); pub const fn implication_propagation(lit: Lit) -> Origin { Origin::Direct(DirectOrigin::ImplicationPropagation(lit)) @@ -91,6 +96,7 @@ impl Origin { #[derive(Copy, Clone, Debug, Eq, PartialEq)] pub enum DirectOrigin { Decision, + Assumption, /// Result of encoding a constraint at the root decision level. Encoding, /// The event is due to an inference. diff --git a/solver/src/core/state/domains.rs b/solver/src/core/state/domains.rs index df8ba905..e6c71899 100644 --- a/solver/src/core/state/domains.rs +++ b/solver/src/core/state/domains.rs @@ -568,7 +568,7 @@ impl Domains { // we should be in a state where the literal is not true yet, but immediately implied debug_assert!(!state.entails(literal)); match cause { - Origin::Direct(DirectOrigin::Decision | DirectOrigin::Encoding) => panic!(), + Origin::Direct(DirectOrigin::Decision | DirectOrigin::Assumption | DirectOrigin::Encoding) => panic!(), Origin::Direct(DirectOrigin::ExternalInference(cause)) => { // ask for a clause (l1 & l2 & ... & ln) => lit explainer.explain(cause, literal, state, explanation); @@ -579,7 +579,7 @@ impl Domains { debug_assert!(state.entails(!invalid_lit)); explanation.push(!invalid_lit); match cause { - DirectOrigin::Decision | DirectOrigin::Encoding => { + DirectOrigin::Decision | DirectOrigin::Assumption | DirectOrigin::Encoding => { explanation.push(invalid_lit); } DirectOrigin::ExternalInference(cause) => { @@ -615,7 +615,7 @@ impl Domains { if matches!( event.cause, - Origin::Direct(DirectOrigin::Decision | DirectOrigin::Encoding) + Origin::Direct(DirectOrigin::Decision | DirectOrigin::Assumption | DirectOrigin::Encoding) ) { None } else { From 6d1fde15d30e1e6a77f687c8b79273301f84b7b1 Mon Sep 17 00:00:00 2001 From: Nika Beriachvili Date: Sat, 21 Dec 2024 23:18:58 +0100 Subject: [PATCH 02/16] feat(solver): change function signatures (and implementation, slightly) to prepare dealing with assumptions and unsat cores --- examples/smt/tests/smt.rs | 28 +++++++++--------- solver/src/solver/solver_impl.rs | 49 ++++++++++++++++---------------- 2 files changed, 38 insertions(+), 39 deletions(-) diff --git a/examples/smt/tests/smt.rs b/examples/smt/tests/smt.rs index 3156b4c0..301ae943 100644 --- a/examples/smt/tests/smt.rs +++ b/examples/smt/tests/smt.rs @@ -1,4 +1,4 @@ -use aries::backtrack::Backtrack; +use aries::backtrack::{Backtrack, DecLvl}; use aries::core::state::OptDomain; use aries::core::Lit; use aries::model::extensions::AssignmentExt; @@ -120,7 +120,7 @@ fn int_bounds() { let mut solver = Solver::new(model); solver.enforce_all(constraints, []); - assert!(solver.propagate_and_backtrack_to_consistent()); + assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); let check_dom = |v, lb, ub| { assert_eq!(solver.model.domain_of(v), (lb, ub)); }; @@ -148,7 +148,7 @@ fn bools_as_ints() { let mut solver = Solver::new(model); - assert!(solver.propagate_and_backtrack_to_consistent()); + assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); assert_eq!(solver.model.boolean_value_of(a), None); assert_eq!(solver.model.domain_of(ia), (0, 1)); assert_eq!(solver.model.boolean_value_of(a), None); @@ -183,25 +183,25 @@ fn ints_and_bools() { let mut solver = Solver::new(model); - assert!(solver.propagate_and_backtrack_to_consistent()); + assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); assert_eq!(solver.model.domain_of(i), (-10, 10)); assert_eq!(solver.model.domain_of(ia), (0, 1)); assert_eq!(solver.model.boolean_value_of(a), None); solver.enforce(leq(i, ia), []); - assert!(solver.propagate_and_backtrack_to_consistent()); + assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); assert_eq!(solver.model.domain_of(i), (-10, 1)); assert_eq!(solver.model.domain_of(ia), (0, 1)); assert_eq!(solver.model.boolean_value_of(a), None); solver.enforce(gt(ia, i), []); - assert!(solver.propagate_and_backtrack_to_consistent()); + assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); assert_eq!(solver.model.domain_of(i), (-10, 0)); assert_eq!(solver.model.domain_of(ia), (0, 1)); assert_eq!(solver.model.boolean_value_of(a), None); solver.enforce(geq(i, 0), []); - assert!(solver.propagate_and_backtrack_to_consistent()); + assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); assert_eq!(solver.model.domain_of(i), (0, 0)); assert_eq!(solver.model.domain_of(ia), (1, 1)); assert_eq!(solver.model.boolean_value_of(a), Some(true)); @@ -237,7 +237,7 @@ fn optional_hierarchy() { // solver.model.print_state(); - assert!(solver.propagate_and_backtrack_to_consistent()); + assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); // solver.model.print_state(); @@ -247,7 +247,7 @@ fn optional_hierarchy() { assert_eq!(solver.model.opt_domain_of(vars[2]), Unknown(5, 10)); solver.decide(Lit::leq(i, 9)); - assert!(solver.propagate_and_backtrack_to_consistent()); + assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); assert_eq!(solver.model.opt_domain_of(i), Unknown(-10, 9)); assert_eq!(solver.model.opt_domain_of(vars[0]), Unknown(0, 8)); @@ -258,7 +258,7 @@ fn optional_hierarchy() { // solver.model.state.print(); solver.decide(Lit::leq(i, 4)); - assert!(solver.propagate_and_backtrack_to_consistent()); + assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); // println!(); // solver.model.state.print(); @@ -271,7 +271,7 @@ fn optional_hierarchy() { solver.save_state(); solver.decide(p); - assert!(solver.propagate_and_backtrack_to_consistent()); + assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); assert_eq!(solver.model.opt_domain_of(i), Present(-10, 4)); assert_eq!(solver.model.opt_domain_of(vars[0]), Unknown(0, 4)); assert_eq!(solver.model.opt_domain_of(vars[1]), Unknown(-10, -5)); @@ -280,21 +280,21 @@ fn optional_hierarchy() { println!("======================"); solver.decide(Lit::leq(i, -1)); - assert!(solver.propagate_and_backtrack_to_consistent()); + assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); assert_eq!(solver.model.opt_domain_of(i), Present(-10, -1)); assert_eq!(solver.model.opt_domain_of(vars[0]), Absent); assert_eq!(solver.model.opt_domain_of(vars[1]), Unknown(-10, -5)); assert_eq!(solver.model.opt_domain_of(vars[2]), Absent); solver.decide(scopes[1]); - assert!(solver.propagate_and_backtrack_to_consistent()); + assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); assert_eq!(solver.model.opt_domain_of(i), Present(-10, -5)); assert_eq!(solver.model.opt_domain_of(vars[0]), Absent); assert_eq!(solver.model.opt_domain_of(vars[1]), Present(-10, -5)); assert_eq!(solver.model.opt_domain_of(vars[2]), Absent); // solver.decide(!p); - // assert!(matches!(solver.propagate_and_backtrack_to_consistent(), Ok(true)); + // assert!(matches!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok(), Ok(true)); // solver.model.discrete.print(); // assert_eq!(solver.model.opt_domain_of(i), Absent); diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs index d1ddc90c..02e45fed 100644 --- a/solver/src/solver/solver_impl.rs +++ b/solver/src/solver/solver_impl.rs @@ -47,8 +47,9 @@ enum SolveResult { /// The solver was made aware of a solution from its input channel. ExternalSolution(Arc), /// The solver has exhausted its search space. - Unsat, + Unsat(Conflict), } +pub type UnsatCore = Explanation; #[derive(Debug)] pub enum Exit { @@ -509,10 +510,10 @@ impl Solver { /// Searches for the first satisfying assignment, returning none if the search /// space was exhausted without encountering a solution. pub fn solve(&mut self) -> Result>, Exit> { - match self._solve()? { + match self._solve(DecLvl::ROOT)? { SolveResult::AtSolution => Ok(Some(Arc::new(self.model.state.clone()))), SolveResult::ExternalSolution(s) => Ok(Some(s)), - SolveResult::Unsat => Ok(None), + SolveResult::Unsat(_) => Ok(None), } } @@ -532,8 +533,8 @@ impl Solver { let mut valid_assignments = Vec::with_capacity(64); loop { - match self._solve()? { - SolveResult::Unsat => return Ok(valid_assignments), + match self._solve(DecLvl::ROOT)? { + SolveResult::Unsat(_) => return Ok(valid_assignments), SolveResult::AtSolution => { // found a solution. record the corresponding assignment and add a clause forbidding it in future solutions let mut assignment = Vec::with_capacity(variables.len()); @@ -546,7 +547,7 @@ impl Solver { } valid_assignments.push(assignment); - if let Some(dl) = self.backtrack_level_for_clause(&clause) { + if let Some(dl) = self.backtrack_level_for_clause(&clause, DecLvl::ROOT) { self.restore(dl); self.reasoners.sat.add_clause(clause); } else { @@ -561,7 +562,7 @@ impl Solver { /// Implementation of the public facing `solve()` method that provides more control. /// In particular, the output distinguishes between whether the solution was found by this /// solver or another one (i.e. was read from the input channel). - fn _solve(&mut self) -> Result { + fn _solve(&mut self, last_assumption_dec_lvl: DecLvl) -> Result { // make sure brancher has knowledge of all variables. self.brancher.import_vars(&self.model); @@ -586,11 +587,11 @@ impl Solver { } } - if !self.propagate_and_backtrack_to_consistent() { + if let Err(conflict) = self.propagate_and_backtrack_to_consistent(last_assumption_dec_lvl) { // UNSAT self.stats.solve_time += start_time.elapsed(); self.stats.solve_cycles += start_cycles.elapsed(); - return Ok(SolveResult::Unsat); + return Ok(SolveResult::Unsat(conflict)); } match self.brancher.next_decision(&self.stats, &self.model) { Some(Decision::SetLiteral(lit)) => { @@ -598,7 +599,7 @@ impl Solver { self.decide(lit); } Some(Decision::Restart) => { - self.reset(); + self.restore(last_assumption_dec_lvl); self.stats.add_restart(); } None => { @@ -723,12 +724,12 @@ impl Solver { /// /// If there is more that one violated literal at the latest level, then no literal is asserted /// and the bactrack level is set to the ante-last level (might occur with clause sharing). - fn backtrack_level_for_clause(&self, clause: &[Lit]) -> Option { + fn backtrack_level_for_clause(&self, clause: &[Lit], last_assumption_dec_lvl: DecLvl) -> Option { debug_assert_eq!(self.model.state.value_of_clause(clause.iter().copied()), Some(false)); // level of the two latest set element of the clause - let mut max = DecLvl::ROOT; - let mut max_next = DecLvl::ROOT; + let mut max = last_assumption_dec_lvl; + let mut max_next = last_assumption_dec_lvl; for &lit in clause { debug_assert!(self.model.state.entails(!lit)); @@ -742,8 +743,8 @@ impl Solver { } } } - - if max == DecLvl::ROOT { + debug_assert!(max >= last_assumption_dec_lvl); + if max == last_assumption_dec_lvl { None } else if max == max_next { Some(max - 1) @@ -757,7 +758,7 @@ impl Solver { /// As a side effect, the activity of the variables in the clause will be increased. /// Returns `false` if the clause is conflicting at the root and thus constitutes a contradiction. #[must_use] - fn add_conflicting_clause_and_backtrack(&mut self, expl: Conflict) -> bool { + fn add_conflicting_clause_and_backtrack(&mut self, expl: &Conflict, last_assumption_dec_lvl: DecLvl) -> bool { // // print the clause before analysis // println!("conflict ({}) :", expl.literals().len()); // for &l in expl.literals() { @@ -781,10 +782,9 @@ impl Solver { // // println!("]"); // } // println!(); - - if let Some(dl) = self.backtrack_level_for_clause(expl.literals()) { + if let Some(dl) = self.backtrack_level_for_clause(expl.literals(), last_assumption_dec_lvl) { // inform the brancher that we are in a conflict state - self.brancher.conflict(&expl, &self.model, &mut self.reasoners, dl); + self.brancher.conflict(expl, &self.model, &mut self.reasoners, dl); // backtrack self.restore(dl); // println!("conflict:"); @@ -800,7 +800,7 @@ impl Solver { self.reasoners.tautologies.add_tautology(expl.clause.literals()[0]) } else { // add clause to sat solver, making sure the asserted literal is set to true - self.reasoners.sat.add_learnt_clause(expl.clause); + self.reasoners.sat.add_learnt_clause(&expl.clause); } true @@ -816,11 +816,10 @@ impl Solver { /// - propagating in the current state /// - return if no conflict was detected /// - otherwise: learn a conflicting clause, backtrack up the decision tree and repeat the process. - #[must_use] - pub fn propagate_and_backtrack_to_consistent(&mut self) -> bool { + pub fn propagate_and_backtrack_to_consistent(&mut self, last_assumption_dec_lvl: DecLvl) -> Result<(), Conflict> { loop { match self.propagate() { - Ok(()) => return true, + Ok(()) => return Ok(()), Err(conflict) => { log_dec!( " CONFLICT {:?} (size: {}) > {}", @@ -829,11 +828,11 @@ impl Solver { conflict.literals().iter().map(|l| self.model.fmt(*l)).format(" | ") ); self.sync.notify_learnt(&conflict.clause); - if self.add_conflicting_clause_and_backtrack(conflict) { + if self.add_conflicting_clause_and_backtrack(&conflict, last_assumption_dec_lvl) { // we backtracked, loop again to propagate } else { // could not backtrack to a non-conflicting state, UNSAT - return false; + return Err(conflict); } } } From 0c33513d5c92dab3bfe884458e9033146d2683cf Mon Sep 17 00:00:00 2001 From: Nika Beriachvili Date: Sat, 21 Dec 2024 23:21:54 +0100 Subject: [PATCH 03/16] feat(solver): add unsat core extraction --- solver/src/core/state/domains.rs | 245 +++++++++++++++++++++- solver/src/core/state/domains/minimize.rs | 4 +- 2 files changed, 241 insertions(+), 8 deletions(-) diff --git a/solver/src/core/state/domains.rs b/solver/src/core/state/domains.rs index e6c71899..23a5d83e 100644 --- a/solver/src/core/state/domains.rs +++ b/solver/src/core/state/domains.rs @@ -199,6 +199,10 @@ impl Domains { self.set(lit, Cause::Decision) } + pub fn assume(&mut self, lit: Lit) -> Result { + self.set(lit, Cause::Assumption) + } + /// Modifies the lower bound of a variable. /// The module that made this modification should be identified in the `cause` parameter, which can /// be used to query it for an explanation of the change. @@ -409,6 +413,8 @@ impl Domains { /// /// The update of `l` must not directly originate from a decision as it is necessarily the case that /// `!l` holds in the current state. It is thus considered a logic error to impose an obviously wrong decision. + /// + /// It can, however, directly originate from an assumption (in which case we are necessarily UNSAT, by the way). pub fn clause_for_invalid_update(&mut self, failed: InvalidUpdate, explainer: &mut impl Explainer) -> Conflict { let InvalidUpdate(literal, cause) = failed; debug_assert!(!self.entails(literal)); @@ -423,17 +429,22 @@ impl Domains { explanation.push(!literal); explanation.push(self.presence(literal)); - // However, `literal` does not hold in the current state and we need to replace it. - // Thus we replace it with a set of literals `x_1 & ... & x_m` such that - // `x_1 & ... & x_m -> literal` - - self.add_implying_literals_to_explanation(literal, cause, &mut explanation, explainer); + if cause != Origin::ASSUMPTION { + // However, `literal` does not hold in the current state and we need to replace it. + // Thus we replace it with a set of literals `x_1 & ... & x_m` such that + // `x_1 & ... & x_m -> literal` + self.add_implying_literals_to_explanation(literal, cause, &mut explanation, explainer); + } debug_assert!(explanation.lits.iter().copied().all(|l| self.entails(l))); // now all disjuncts hold in the current state // we then transform this clause to be in the first unique implication point (1UIP) form. + let mut conflict = self.refine_explanation(explanation, explainer); - self.refine_explanation(explanation, explainer) + if cause == Origin::ASSUMPTION { + conflict.clause.literals.push(!literal); + } + conflict } /// Refines an explanation into an asserting clause. @@ -526,6 +537,53 @@ impl Domains { Conflict { clause, resolved } } + pub fn extract_unsat_core(&mut self, conflict: &Conflict, explainer: &mut impl Explainer) -> Explanation { + + let mut explanation = Explanation::new(); + let mut result = Explanation::new(); // FIXME: use a (conjunctive) litset to avoid duplicates ? tests seem to show no difference... + + for &lit in conflict.clause.literals() { // explanation.push(!lit); + if self.entails(!lit) { + explanation.push(!lit); + } else { + // This case happens when `lit` is an assumption literal whose + // attempted entailment resulted in an invalid update and + // was put in `conflict` in `clause_for_invalid_update` + // (see `if Origin::ASSUMPTION`). + // An immediate consequence of this is that there is at most one such literal in `conflict`. + result.push(!lit); + } + } + debug_assert!(explanation.literals().iter().all(|&l| self.entails(l))); + debug_assert!(result.literals().len() <= 1); + + self.queue.clear(); + + loop { + for l in explanation.lits.drain(..) { + if let Some(loc) = self.implying_event(l) { + if self.trail().get_event(loc).cause == Origin::ASSUMPTION { + result.lits.push(l); + } else { + debug_assert!(self.entails(l)); + self.queue.push(loc, l); + } + } + } + debug_assert!(explanation.lits.is_empty()); + + if self.queue.is_empty() { + break; + } + let (lit, _) = self.queue.pop().unwrap(); + + if let Some(implying_lits) = self.implying_literals(lit, explainer) { + for l in implying_lits { explanation.push(l); } + } + }; + result + } + /// Returns all decisions that were taken since the root decision level. pub fn decisions(&self) -> Vec<(DecLvl, Lit)> { let mut decs = Vec::new(); @@ -945,4 +1003,179 @@ mod tests { model.save_state(); assert!(model.set_lb(i, 6, Cause::Decision).is_err()); } + + #[test] + fn test_unsat_core_extraction() { + let mut model = Domains::new(); + let a = Lit::geq(model.new_var(0, 1), 1); + let b = Lit::geq(model.new_var(0, 1), 1); + let c = Lit::geq(model.new_var(0, 1), 1); + let d = Lit::geq(model.new_var(0, 1), 1); + let e = Lit::geq(model.new_var(0, 1), 1); + let f = Lit::geq(model.new_var(0, 1), 1); + let g = Lit::geq(model.new_var(0, 1), 1); + let h = Lit::geq(model.new_var(0, 1), 1); + + // assumptions: a, b, d + // expected core: a, b + + // constraint 0: "a => c" + // constraint 1: "b & c => f" + // constraint 2: "f => !h" + // constraint 3: "d => e" + // constraint 4: "g => h" + + // a => c | b => f => !h | d => e | g => h | + // '========^ + + let writer = ReasonerId::Sat; + + let cause_a = Cause::inference(writer, 0u32); + let cause_bc = Cause::inference(writer, 1u32); + let cause_f = Cause::inference(writer, 2u32); + let cause_e = Cause::inference(writer, 3u32); + let cause_g = Cause::inference(writer, 4u32); + + #[allow(unused_must_use)] + let propagate = |model: &mut Domains| -> Result { + if model.entails(a) { + model.set(c, cause_a)?; + } + if model.entails(b) & model.entails(c) { + model.set(f, cause_bc)?; + } + if model.entails(f) { + model.set(h.not(), cause_f)?; + } + if model.entails(d) { + model.set(e, cause_e)?; + } + if model.entails(g) { + model.set(h, cause_g)?; + } + Ok(true) + }; + + struct Expl { + a: Lit, + b: Lit, + c: Lit, + d: Lit, + e: Lit, + f: Lit, + g: Lit, + h: Lit, + } + impl Explainer for Expl { + fn explain( + &mut self, + cause: InferenceCause, + literal: Lit, + _model: &DomainsSnapshot, + explanation: &mut Explanation, + ) { + assert_eq!(cause.writer, ReasonerId::Sat); + match cause.payload { + 0 => { + assert_eq!(literal, self.c); + explanation.push(self.a); + } + 1 => { + assert_eq!(literal, self.f); + explanation.push(self.b); + explanation.push(self.c); + } + 2 => { + assert_eq!(literal, self.h.not()); + explanation.push(self.f); + } + 3 => { + assert_eq!(literal, self.e); + explanation.push(self.d); + } + 4 => { + assert_eq!(literal, self.h); + explanation.push(self.g); + } + _ => panic!("unexpected payload"), + } + } + } + + let mut network = Expl { a, b, c, d, e, f, g, h }; + + propagate(&mut model).unwrap(); + + model.save_state(); + assert!(model.assume(a).unwrap()); + assert_eq!(model.bounds(a.variable()), (1, 1)); + propagate(&mut model).unwrap(); + assert_eq!(model.bounds(c.variable()), (1, 1)); + + model.save_state(); + assert!(model.assume(b).unwrap()); + assert_eq!(model.bounds(b.variable()), (1, 1)); + propagate(&mut model).unwrap(); + assert_eq!(model.bounds(f.variable()), (1, 1)); + assert_eq!(model.bounds(h.variable()), (0, 0)); + + model.save_state(); + assert!(model.assume(d).unwrap()); + assert_eq!(model.bounds(d.variable()), (1, 1)); + propagate(&mut model).unwrap(); + assert_eq!(model.bounds(e.variable()), (1, 1)); + + model.save_state(); + model.decide(g).unwrap(); + assert_eq!(model.bounds(g.variable()), (1, 1)); + let err = match propagate(&mut model) { + Err(err) => err, + _ => panic!(), + }; + + let conflict = model.clause_for_invalid_update(err, &mut network); + let unsat_core = model.extract_unsat_core(&conflict, &mut network).lits; + let unsat_core_set: HashSet:: = unsat_core.iter().copied().collect(); + + let mut expected = HashSet::new(); + expected.insert(a); + expected.insert(b); + assert_eq!(unsat_core_set, expected); + + model.restore_last(); + + model.save_state(); + model.assume(g).unwrap(); + assert_eq!(model.bounds(g.variable()), (1, 1)); + let err = match propagate(&mut model) { + Err(err) => err, + _ => panic!(), + }; + + let conflict = model.clause_for_invalid_update(err, &mut network); + let unsat_core = model.extract_unsat_core(&conflict, &mut network).lits; + let unsat_core_set: HashSet:: = unsat_core.iter().copied().collect(); + + let mut expected = HashSet::new(); + expected.insert(a); + expected.insert(b); + expected.insert(g); + assert_eq!(unsat_core_set, expected); + + model.restore_last(); + + model.save_state(); + let err = model.assume(h).unwrap_err(); + + let conflict = model.clause_for_invalid_update(err, &mut network); + let unsat_core = model.extract_unsat_core(&conflict, &mut network).lits; + let unsat_core_set: HashSet:: = unsat_core.iter().copied().collect(); + + let mut expected = HashSet::new(); + expected.insert(a); + expected.insert(b); + expected.insert(h); + assert_eq!(unsat_core_set, expected); + + } } diff --git a/solver/src/core/state/domains/minimize.rs b/solver/src/core/state/domains/minimize.rs index 694c9d2b..dced08f3 100644 --- a/solver/src/core/state/domains/minimize.rs +++ b/solver/src/core/state/domains/minimize.rs @@ -180,8 +180,8 @@ impl State { unreachable!() }; let event = doms.get_event(event); - if event.cause == Origin::DECISION { - // decision => not redundant + if matches!(event.cause, Origin::DECISION | Origin::ASSUMPTION) { + // decision or assumption => not redundant self.mark_not_redundant(cur); Some(false) } else { From 517ed330bd675a2226589fce72a07cbfbff5fa58 Mon Sep 17 00:00:00 2001 From: Nika Beriachvili Date: Sat, 21 Dec 2024 23:24:01 +0100 Subject: [PATCH 04/16] feat(solver): add solving with assumptions --- solver/src/solver/solver_impl.rs | 53 ++++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs index 02e45fed..a66c2a68 100644 --- a/solver/src/solver/solver_impl.rs +++ b/solver/src/solver/solver_impl.rs @@ -559,6 +559,50 @@ impl Solver { } } + pub fn solve_with_assumptions( + &mut self, + assumption_lits: impl IntoIterator, + ) -> Result, UnsatCore>, Exit> { + // make sure brancher has knowledge of all variables. + self.brancher.import_vars(&self.model); + + // TODO? let start_time = Instant::now(); + // TODO? let start_cycles = StartCycleCount::now(); + + match self.propagate_and_backtrack_to_consistent(DecLvl::ROOT) { + Ok(()) => (), + Err(conflict) => { + debug_assert!(conflict.is_empty()); + return Ok(Err(Explanation::new())); + } + }; + + for lit in assumption_lits { + match self.assume(lit) { + Ok(_) => { + if let Err(conflict) = self.propagate_and_backtrack_to_consistent(self.current_decision_level()) { + let unsat_core = self.model.state.extract_unsat_core(&conflict, &mut self.reasoners); + return Ok(Err(unsat_core)); + } + }, + Err(failed) => { + let conflict = self.model.state.clause_for_invalid_update(failed, &mut self.reasoners); + let unsat_core = self.model.state.extract_unsat_core(&conflict, &mut self.reasoners); + return Ok(Err(unsat_core)); + }, + } + } + let last_assumption_dec_lvl = self.current_decision_level(); + match self._solve(last_assumption_dec_lvl)? { + SolveResult::AtSolution => Ok(Ok(Arc::new(self.model.state.clone()))), + SolveResult::ExternalSolution(s) => Ok(Ok(s)), + SolveResult::Unsat(conflict) => { + let unsat_core = self.model.state.extract_unsat_core(&conflict, &mut self.reasoners); + Ok(Err(unsat_core)) + } + } + } + /// Implementation of the public facing `solve()` method that provides more control. /// In particular, the output distinguishes between whether the solution was found by this /// solver or another one (i.e. was read from the input channel). @@ -715,6 +759,15 @@ impl Solver { self.stats.add_decision(decision) } + pub fn assume(&mut self, assumption: Lit) -> Result { + assert!( + self.model.state.decisions().is_empty(), // FIXME: find a more efficient way to check ?.. + "Not allowed to make assumptions after solver already started making decisions (i.e. started solving) !", + ); + self.save_state(); + self.model.state.assume(assumption) + } + /// Determines the appropriate backtrack level for this clause and returns the literal that /// is asserted at this level. /// From 3ab1c0d4af6e0b746e36fe31110207bcd5dcd482 Mon Sep 17 00:00:00 2001 From: Nika Beriachvili Date: Sat, 21 Dec 2024 23:25:57 +0100 Subject: [PATCH 05/16] feat(solver): change `optimize_with` to use assumption solving --- solver/src/solver/solver_impl.rs | 25 +++++++++++++++---------- 1 file changed, 15 insertions(+), 10 deletions(-) diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs index a66c2a68..19c291ad 100644 --- a/solver/src/solver/solver_impl.rs +++ b/solver/src/solver/solver_impl.rs @@ -693,11 +693,11 @@ impl Solver { ) -> Result)>, Exit> { // best solution found so far let mut best = None; + let mut must_improve_lits = Vec::new(); loop { - let sol = match self._solve()? { - SolveResult::AtSolution => { + let sol = match self.solve_with_assumptions(must_improve_lits.clone())? { + Ok(sol) => { // solver stopped at a solution, this is necessarily an improvement on the best solution found so far - let sol = Arc::new(self.model.state.clone()); // notify other solvers that we have found a new solution self.sync.notify_solution_found(sol.clone()); let objective_value = sol.var_domain(objective).lb; @@ -706,10 +706,13 @@ impl Solver { println!("********* New sol: {objective_value} *********"); self.print_stats(); } + self.restore(DecLvl::new(must_improve_lits.len().try_into().unwrap())); sol } - SolveResult::ExternalSolution(sol) => sol, // a solution was handed out to us by another solver - SolveResult::Unsat => return Ok(best), // exhausted search space, return the best result found so far + Err(_) => { + // exhausted search space, return the best result found so far + return Ok(best); + } }; // determine whether the solution found is an improvement on the previous one (might not be the case if sent by another solver) @@ -736,12 +739,14 @@ impl Solver { best = Some((objective_value, sol)); // force future solutions to improve on this one - let must_improve_lit = if minimize { - objective.lt_lit(objective_value) + if minimize { +// must_improve_lits = vec![objective.lt_lit(objective_value)]; + must_improve_lits.push(objective.lt_lit(objective_value)); } else { - objective.gt_lit(objective_value) - }; - self.reasoners.tautologies.add_tautology(must_improve_lit); +// must_improve_lits = vec![objective.gt_lit(objective_value)]; + must_improve_lits.push(objective.gt_lit(objective_value)); + } + } } } From e8a1153daf0789c6b1ed7504730b71d9d241d05c Mon Sep 17 00:00:00 2001 From: Nika Beriachvili Date: Mon, 23 Dec 2024 19:25:18 +0100 Subject: [PATCH 06/16] chore: fix clippy lints and remove useless comments --- solver/src/core/state/domains.rs | 18 ++++++++---------- solver/src/solver/solver_impl.rs | 9 +++------ 2 files changed, 11 insertions(+), 16 deletions(-) diff --git a/solver/src/core/state/domains.rs b/solver/src/core/state/domains.rs index 23a5d83e..1f5bbcf3 100644 --- a/solver/src/core/state/domains.rs +++ b/solver/src/core/state/domains.rs @@ -413,7 +413,7 @@ impl Domains { /// /// The update of `l` must not directly originate from a decision as it is necessarily the case that /// `!l` holds in the current state. It is thus considered a logic error to impose an obviously wrong decision. - /// + /// /// It can, however, directly originate from an assumption (in which case we are necessarily UNSAT, by the way). pub fn clause_for_invalid_update(&mut self, failed: InvalidUpdate, explainer: &mut impl Explainer) -> Conflict { let InvalidUpdate(literal, cause) = failed; @@ -538,11 +538,10 @@ impl Domains { } pub fn extract_unsat_core(&mut self, conflict: &Conflict, explainer: &mut impl Explainer) -> Explanation { - let mut explanation = Explanation::new(); - let mut result = Explanation::new(); // FIXME: use a (conjunctive) litset to avoid duplicates ? tests seem to show no difference... + let mut result = Explanation::new(); // FIXME: use a (conjunctive) litset to avoid duplicates ? tests seem to show no difference... - for &lit in conflict.clause.literals() { // explanation.push(!lit); + for &lit in conflict.clause.literals() { if self.entails(!lit) { explanation.push(!lit); } else { @@ -578,9 +577,9 @@ impl Domains { let (lit, _) = self.queue.pop().unwrap(); if let Some(implying_lits) = self.implying_literals(lit, explainer) { - for l in implying_lits { explanation.push(l); } + explanation.lits.extend(implying_lits); } - }; + } result } @@ -1135,7 +1134,7 @@ mod tests { let conflict = model.clause_for_invalid_update(err, &mut network); let unsat_core = model.extract_unsat_core(&conflict, &mut network).lits; - let unsat_core_set: HashSet:: = unsat_core.iter().copied().collect(); + let unsat_core_set: HashSet = unsat_core.iter().copied().collect(); let mut expected = HashSet::new(); expected.insert(a); @@ -1154,7 +1153,7 @@ mod tests { let conflict = model.clause_for_invalid_update(err, &mut network); let unsat_core = model.extract_unsat_core(&conflict, &mut network).lits; - let unsat_core_set: HashSet:: = unsat_core.iter().copied().collect(); + let unsat_core_set: HashSet = unsat_core.iter().copied().collect(); let mut expected = HashSet::new(); expected.insert(a); @@ -1169,13 +1168,12 @@ mod tests { let conflict = model.clause_for_invalid_update(err, &mut network); let unsat_core = model.extract_unsat_core(&conflict, &mut network).lits; - let unsat_core_set: HashSet:: = unsat_core.iter().copied().collect(); + let unsat_core_set: HashSet = unsat_core.iter().copied().collect(); let mut expected = HashSet::new(); expected.insert(a); expected.insert(b); expected.insert(h); assert_eq!(unsat_core_set, expected); - } } diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs index 19c291ad..c28e3b06 100644 --- a/solver/src/solver/solver_impl.rs +++ b/solver/src/solver/solver_impl.rs @@ -584,12 +584,12 @@ impl Solver { let unsat_core = self.model.state.extract_unsat_core(&conflict, &mut self.reasoners); return Ok(Err(unsat_core)); } - }, + } Err(failed) => { let conflict = self.model.state.clause_for_invalid_update(failed, &mut self.reasoners); let unsat_core = self.model.state.extract_unsat_core(&conflict, &mut self.reasoners); return Ok(Err(unsat_core)); - }, + } } } let last_assumption_dec_lvl = self.current_decision_level(); @@ -740,13 +740,10 @@ impl Solver { // force future solutions to improve on this one if minimize { -// must_improve_lits = vec![objective.lt_lit(objective_value)]; must_improve_lits.push(objective.lt_lit(objective_value)); } else { -// must_improve_lits = vec![objective.gt_lit(objective_value)]; must_improve_lits.push(objective.gt_lit(objective_value)); } - } } } @@ -766,7 +763,7 @@ impl Solver { pub fn assume(&mut self, assumption: Lit) -> Result { assert!( - self.model.state.decisions().is_empty(), // FIXME: find a more efficient way to check ?.. + self.model.state.decisions().is_empty(), "Not allowed to make assumptions after solver already started making decisions (i.e. started solving) !", ); self.save_state(); From ea8084e4ad4312849b92a20540e8a42434a5e6a1 Mon Sep 17 00:00:00 2001 From: Nika Beriachvili Date: Thu, 26 Dec 2024 15:53:04 +0100 Subject: [PATCH 07/16] refactor(solver): refactor unsat core extraction into 2 functions (for 2 different cases) --- solver/src/core/state/domains.rs | 73 +++++++++++++++++++------------- solver/src/solver/solver_impl.rs | 16 +++++-- 2 files changed, 56 insertions(+), 33 deletions(-) diff --git a/solver/src/core/state/domains.rs b/solver/src/core/state/domains.rs index 1f5bbcf3..37da5567 100644 --- a/solver/src/core/state/domains.rs +++ b/solver/src/core/state/domains.rs @@ -439,12 +439,7 @@ impl Domains { // now all disjuncts hold in the current state // we then transform this clause to be in the first unique implication point (1UIP) form. - let mut conflict = self.refine_explanation(explanation, explainer); - - if cause == Origin::ASSUMPTION { - conflict.clause.literals.push(!literal); - } - conflict + self.refine_explanation(explanation, explainer) } /// Refines an explanation into an asserting clause. @@ -537,24 +532,13 @@ impl Domains { Conflict { clause, resolved } } - pub fn extract_unsat_core(&mut self, conflict: &Conflict, explainer: &mut impl Explainer) -> Explanation { - let mut explanation = Explanation::new(); - let mut result = Explanation::new(); // FIXME: use a (conjunctive) litset to avoid duplicates ? tests seem to show no difference... - - for &lit in conflict.clause.literals() { - if self.entails(!lit) { - explanation.push(!lit); - } else { - // This case happens when `lit` is an assumption literal whose - // attempted entailment resulted in an invalid update and - // was put in `conflict` in `clause_for_invalid_update` - // (see `if Origin::ASSUMPTION`). - // An immediate consequence of this is that there is at most one such literal in `conflict`. - result.push(!lit); - } - } - debug_assert!(explanation.literals().iter().all(|&l| self.entails(l))); - debug_assert!(result.literals().len() <= 1); + fn extract_assumptions_implying( + &mut self, + explanation: &mut Explanation, + explainer: &mut impl Explainer, + ) -> Explanation { + debug_assert!(explanation.lits.iter().all(|&l| self.entails(l))); + let mut result = Explanation::new(); self.queue.clear(); @@ -583,6 +567,39 @@ impl Domains { result } + pub fn extract_unsat_core_after_invalid_update( + &mut self, + failed: InvalidUpdate, + explainer: &mut impl Explainer, + ) -> Explanation { + let InvalidUpdate(literal, cause) = failed; + debug_assert!(!self.entails(literal)); + let mut explanation = Explanation::new(); + explanation.lits = self + .clause_for_invalid_update(failed, explainer) + .clause + .literals() + .iter() + .map(|&l| !l) + .collect(); + + let mut unsat_core = self.extract_assumptions_implying(&mut explanation, explainer); + if cause == Origin::ASSUMPTION { + unsat_core.lits.push(literal); + } + unsat_core + } + + pub fn extract_unsat_core_after_conflict( + &mut self, + conflict: Conflict, + explainer: &mut impl Explainer, + ) -> Explanation { + let mut explanation = Explanation::new(); + explanation.lits = conflict.clause.literals().iter().map(|&l| !l).collect(); + self.extract_assumptions_implying(&mut explanation, explainer) + } + /// Returns all decisions that were taken since the root decision level. pub fn decisions(&self) -> Vec<(DecLvl, Lit)> { let mut decs = Vec::new(); @@ -1133,7 +1150,7 @@ mod tests { }; let conflict = model.clause_for_invalid_update(err, &mut network); - let unsat_core = model.extract_unsat_core(&conflict, &mut network).lits; + let unsat_core = model.extract_unsat_core_after_conflict(conflict, &mut network).lits; let unsat_core_set: HashSet = unsat_core.iter().copied().collect(); let mut expected = HashSet::new(); @@ -1151,8 +1168,7 @@ mod tests { _ => panic!(), }; - let conflict = model.clause_for_invalid_update(err, &mut network); - let unsat_core = model.extract_unsat_core(&conflict, &mut network).lits; + let unsat_core = model.extract_unsat_core_after_invalid_update(err, &mut network).lits; let unsat_core_set: HashSet = unsat_core.iter().copied().collect(); let mut expected = HashSet::new(); @@ -1166,8 +1182,7 @@ mod tests { model.save_state(); let err = model.assume(h).unwrap_err(); - let conflict = model.clause_for_invalid_update(err, &mut network); - let unsat_core = model.extract_unsat_core(&conflict, &mut network).lits; + let unsat_core = model.extract_unsat_core_after_invalid_update(err, &mut network).lits; let unsat_core_set: HashSet = unsat_core.iter().copied().collect(); let mut expected = HashSet::new(); diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs index c28e3b06..4edb098f 100644 --- a/solver/src/solver/solver_impl.rs +++ b/solver/src/solver/solver_impl.rs @@ -581,13 +581,18 @@ impl Solver { match self.assume(lit) { Ok(_) => { if let Err(conflict) = self.propagate_and_backtrack_to_consistent(self.current_decision_level()) { - let unsat_core = self.model.state.extract_unsat_core(&conflict, &mut self.reasoners); + let unsat_core = self + .model + .state + .extract_unsat_core_after_conflict(conflict, &mut self.reasoners); return Ok(Err(unsat_core)); } } Err(failed) => { - let conflict = self.model.state.clause_for_invalid_update(failed, &mut self.reasoners); - let unsat_core = self.model.state.extract_unsat_core(&conflict, &mut self.reasoners); + let unsat_core = self + .model + .state + .extract_unsat_core_after_invalid_update(failed, &mut self.reasoners); return Ok(Err(unsat_core)); } } @@ -597,7 +602,10 @@ impl Solver { SolveResult::AtSolution => Ok(Ok(Arc::new(self.model.state.clone()))), SolveResult::ExternalSolution(s) => Ok(Ok(s)), SolveResult::Unsat(conflict) => { - let unsat_core = self.model.state.extract_unsat_core(&conflict, &mut self.reasoners); + let unsat_core = self + .model + .state + .extract_unsat_core_after_conflict(conflict, &mut self.reasoners); Ok(Err(unsat_core)) } } From 1bfa0550bc3389d4afdbdb35af583fbdfe6d443e Mon Sep 17 00:00:00 2001 From: Nika Beriachvili Date: Fri, 27 Dec 2024 17:15:27 +0100 Subject: [PATCH 08/16] fix(solver): correct latest assumption dec level for initial propagation in `solve_with_assumptions` --- solver/src/solver/solver_impl.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs index 4edb098f..641c0c46 100644 --- a/solver/src/solver/solver_impl.rs +++ b/solver/src/solver/solver_impl.rs @@ -569,7 +569,7 @@ impl Solver { // TODO? let start_time = Instant::now(); // TODO? let start_cycles = StartCycleCount::now(); - match self.propagate_and_backtrack_to_consistent(DecLvl::ROOT) { + match self.propagate_and_backtrack_to_consistent(self.current_decision_level()) { Ok(()) => (), Err(conflict) => { debug_assert!(conflict.is_empty()); From d5f38a7f8f90bd9ff11539a73ece0b455a997d06 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Tue, 7 Jan 2025 10:59:41 +0100 Subject: [PATCH 09/16] fix(solver): In restore_last, the decision level was decremented twice --- solver/src/solver/solver_impl.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs index 641c0c46..f37c82b2 100644 --- a/solver/src/solver/solver_impl.rs +++ b/solver/src/solver/solver_impl.rs @@ -1029,7 +1029,6 @@ impl Backtrack for Solver { fn restore_last(&mut self) { assert!(self.decision_level > DecLvl::ROOT); self.restore(self.decision_level - 1); - self.decision_level -= 1; } fn restore(&mut self, saved_id: DecLvl) { From dccd9b3625b1f2f495c218163a311dedfaf50756 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Tue, 7 Jan 2025 15:33:54 +0100 Subject: [PATCH 10/16] chore(assumption): Refactor assumption, allowing for a more incremental API --- examples/smt/tests/smt.rs | 30 ++-- planning/planners/src/encode.rs | 8 +- solver/src/model/extensions/assignments.rs | 7 +- solver/src/model/extensions/mod.rs | 3 +- solver/src/model/model_impl.rs | 2 +- solver/src/solver/solver_impl.rs | 165 ++++++++++++++------- 6 files changed, 138 insertions(+), 77 deletions(-) diff --git a/examples/smt/tests/smt.rs b/examples/smt/tests/smt.rs index 301ae943..4f31e5f9 100644 --- a/examples/smt/tests/smt.rs +++ b/examples/smt/tests/smt.rs @@ -1,4 +1,4 @@ -use aries::backtrack::{Backtrack, DecLvl}; +use aries::backtrack::Backtrack; use aries::core::state::OptDomain; use aries::core::Lit; use aries::model::extensions::AssignmentExt; @@ -62,6 +62,7 @@ fn minimize() { let mut solver = Solver::new(model); assert!(solver.solve().unwrap().is_some()); + solver.reset(); match solver.minimize(c).unwrap() { None => panic!(), Some((val, _)) => assert_eq!(val, 7), @@ -80,6 +81,7 @@ fn minimize_small() { let mut solver = Solver::new(model); assert!(solver.solve().unwrap().is_some()); + solver.reset(); match solver.minimize(a).unwrap() { None => panic!(), Some((val, _)) => assert_eq!(val, 6), @@ -120,7 +122,7 @@ fn int_bounds() { let mut solver = Solver::new(model); solver.enforce_all(constraints, []); - assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); + assert!(solver.propagate_and_backtrack_to_consistent().is_ok()); let check_dom = |v, lb, ub| { assert_eq!(solver.model.domain_of(v), (lb, ub)); }; @@ -148,7 +150,7 @@ fn bools_as_ints() { let mut solver = Solver::new(model); - assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); + assert!(solver.propagate_and_backtrack_to_consistent().is_ok()); assert_eq!(solver.model.boolean_value_of(a), None); assert_eq!(solver.model.domain_of(ia), (0, 1)); assert_eq!(solver.model.boolean_value_of(a), None); @@ -183,25 +185,25 @@ fn ints_and_bools() { let mut solver = Solver::new(model); - assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); + assert!(solver.propagate_and_backtrack_to_consistent().is_ok()); assert_eq!(solver.model.domain_of(i), (-10, 10)); assert_eq!(solver.model.domain_of(ia), (0, 1)); assert_eq!(solver.model.boolean_value_of(a), None); solver.enforce(leq(i, ia), []); - assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); + assert!(solver.propagate_and_backtrack_to_consistent().is_ok()); assert_eq!(solver.model.domain_of(i), (-10, 1)); assert_eq!(solver.model.domain_of(ia), (0, 1)); assert_eq!(solver.model.boolean_value_of(a), None); solver.enforce(gt(ia, i), []); - assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); + assert!(solver.propagate_and_backtrack_to_consistent().is_ok()); assert_eq!(solver.model.domain_of(i), (-10, 0)); assert_eq!(solver.model.domain_of(ia), (0, 1)); assert_eq!(solver.model.boolean_value_of(a), None); solver.enforce(geq(i, 0), []); - assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); + assert!(solver.propagate_and_backtrack_to_consistent().is_ok()); assert_eq!(solver.model.domain_of(i), (0, 0)); assert_eq!(solver.model.domain_of(ia), (1, 1)); assert_eq!(solver.model.boolean_value_of(a), Some(true)); @@ -237,7 +239,7 @@ fn optional_hierarchy() { // solver.model.print_state(); - assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); + assert!(solver.propagate_and_backtrack_to_consistent().is_ok()); // solver.model.print_state(); @@ -247,7 +249,7 @@ fn optional_hierarchy() { assert_eq!(solver.model.opt_domain_of(vars[2]), Unknown(5, 10)); solver.decide(Lit::leq(i, 9)); - assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); + assert!(solver.propagate_and_backtrack_to_consistent().is_ok()); assert_eq!(solver.model.opt_domain_of(i), Unknown(-10, 9)); assert_eq!(solver.model.opt_domain_of(vars[0]), Unknown(0, 8)); @@ -258,7 +260,7 @@ fn optional_hierarchy() { // solver.model.state.print(); solver.decide(Lit::leq(i, 4)); - assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); + assert!(solver.propagate_and_backtrack_to_consistent().is_ok()); // println!(); // solver.model.state.print(); @@ -271,7 +273,7 @@ fn optional_hierarchy() { solver.save_state(); solver.decide(p); - assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); + assert!(solver.propagate_and_backtrack_to_consistent().is_ok()); assert_eq!(solver.model.opt_domain_of(i), Present(-10, 4)); assert_eq!(solver.model.opt_domain_of(vars[0]), Unknown(0, 4)); assert_eq!(solver.model.opt_domain_of(vars[1]), Unknown(-10, -5)); @@ -280,21 +282,21 @@ fn optional_hierarchy() { println!("======================"); solver.decide(Lit::leq(i, -1)); - assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); + assert!(solver.propagate_and_backtrack_to_consistent().is_ok()); assert_eq!(solver.model.opt_domain_of(i), Present(-10, -1)); assert_eq!(solver.model.opt_domain_of(vars[0]), Absent); assert_eq!(solver.model.opt_domain_of(vars[1]), Unknown(-10, -5)); assert_eq!(solver.model.opt_domain_of(vars[2]), Absent); solver.decide(scopes[1]); - assert!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok()); + assert!(solver.propagate_and_backtrack_to_consistent().is_ok()); assert_eq!(solver.model.opt_domain_of(i), Present(-10, -5)); assert_eq!(solver.model.opt_domain_of(vars[0]), Absent); assert_eq!(solver.model.opt_domain_of(vars[1]), Present(-10, -5)); assert_eq!(solver.model.opt_domain_of(vars[2]), Absent); // solver.decide(!p); - // assert!(matches!(solver.propagate_and_backtrack_to_consistent(DecLvl::ROOT).is_ok(), Ok(true)); + // assert!(matches!(solver.propagate_and_backtrack_to_consistent().is_ok(), Ok(true)); // solver.model.discrete.print(); // assert_eq!(solver.model.opt_domain_of(i), Absent); diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index 721bd32d..6da98dc7 100644 --- a/planning/planners/src/encode.rs +++ b/planning/planners/src/encode.rs @@ -381,7 +381,7 @@ fn enforce_refinement(t: TaskRef, supporters: Vec, model: &mut Model) { /// Multiply an integer atom with a literal. /// The result is a linear sum evaluated to the atom if the literal is true, and to 0 otherwise. fn iatom_mul_lit(model: &mut Model, atom: IAtom, lit: Lit) -> LinearSum { - debug_assert!(model.state.implies(lit, model.presence_literal(atom.var.into()))); + debug_assert!(model.state.implies(lit, model.presence_literal(atom.var))); if atom.var == IVar::ZERO { // Constant variable if atom.shift == 0 { @@ -892,7 +892,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result } // each term of the increase value is present for term in inc_val.terms() { - let p = solver.model.presence_literal(term.var().into()); + let p = solver.model.presence_literal(term.var()); active_inc_conjunction.push(p); } // compute wether the increase is active in the condition value @@ -903,7 +903,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result inc_support.entry(inc_id).or_default().push(active_inc); for term in inc_val.terms() { // compute some static implication for better propagation - let p = solver.model.presence_literal(term.var().into()); + let p = solver.model.presence_literal(term.var()); if !solver.model.entails(p) { solver.model.state.add_implication(active_inc, p); } @@ -914,7 +914,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result // enforce the condition value to be the sum of the assignment values and the increase values for term in cond_val_sum.terms() { // compute some static implication for better propagation - let p = solver.model.presence_literal(term.var().into()); + let p = solver.model.presence_literal(term.var()); if !solver.model.entails(p) { solver.model.state.add_implication(supported_by, p); } diff --git a/solver/src/model/extensions/assignments.rs b/solver/src/model/extensions/assignments.rs index b3973faf..a5366ff0 100644 --- a/solver/src/model/extensions/assignments.rs +++ b/solver/src/model/extensions/assignments.rs @@ -6,6 +6,7 @@ use crate::model::lang::{Atom, Cst, IAtom, IVar, SAtom}; use crate::model::symbols::SymId; use crate::model::symbols::{ContiguousSymbols, TypedSym}; use num_rational::Rational32; +use state::Term; /// Extension methods for an object containing a partial or total assignment to a problem. pub trait AssignmentExt { @@ -13,7 +14,7 @@ pub trait AssignmentExt { fn var_domain(&self, var: impl Into) -> IntDomain; - fn presence_literal(&self, variable: VarRef) -> Lit; + fn presence_literal(&self, variable: impl Term) -> Lit; fn value_of_literal(&self, literal: Lit) -> Option { if self.entails(literal) { @@ -37,7 +38,7 @@ pub trait AssignmentExt { fn sym_present(&self, atom: impl Into) -> Option { let atom = atom.into(); match atom { - SAtom::Var(v) => self.boolean_value_of(self.presence_literal(v.into())), + SAtom::Var(v) => self.boolean_value_of(self.presence_literal(v)), SAtom::Cst(_) => Some(true), } } @@ -66,7 +67,7 @@ pub trait AssignmentExt { fn opt_domain_of(&self, atom: impl Into) -> OptDomain { let atom = atom.into(); let (lb, ub) = self.domain_of(atom); - let prez = self.presence_literal(atom.var.into()); + let prez = self.presence_literal(atom.var); match self.value_of_literal(prez) { Some(true) => OptDomain::Present(lb, ub), Some(false) => OptDomain::Absent, diff --git a/solver/src/model/extensions/mod.rs b/solver/src/model/extensions/mod.rs index 3fcdc7a8..63a0ebc4 100644 --- a/solver/src/model/extensions/mod.rs +++ b/solver/src/model/extensions/mod.rs @@ -13,6 +13,7 @@ pub mod partial_assignment; pub use assignments::*; pub use disjunction::*; pub use format::*; +use state::Term; use crate::core::state::{Domains, IntDomain}; use crate::core::*; @@ -59,7 +60,7 @@ impl AssignmentExt for SavedAssignment { } } - fn presence_literal(&self, variable: VarRef) -> Lit { + fn presence_literal(&self, variable: impl Term) -> Lit { self.presence(variable) } diff --git a/solver/src/model/model_impl.rs b/solver/src/model/model_impl.rs index 16c13800..3d4074a2 100644 --- a/solver/src/model/model_impl.rs +++ b/solver/src/model/model_impl.rs @@ -591,7 +591,7 @@ impl AssignmentExt for Model { self.state.var_domain(var) } - fn presence_literal(&self, variable: VarRef) -> Lit { + fn presence_literal(&self, variable: impl Term) -> Lit { self.state.presence(variable) } diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs index f37c82b2..91992db4 100644 --- a/solver/src/solver/solver_impl.rs +++ b/solver/src/solver/solver_impl.rs @@ -68,7 +68,14 @@ pub struct Solver { next_unposted_constraint: usize, pub brancher: Box + Send>, pub reasoners: Reasoners, + /// Current decision level at which the solver is at (corresponding to the number of saved states in the trail) + /// Note that a `DecLvl` may be either the root (`DecLvl::ROOT`), start with an assumption or start with a decision. + /// All assumption must be immediately after the root, before any decision. decision_level: DecLvl, + /// Last level that can be treated as assumption (including ROOT). + /// Invariant: `last_assumption_level <= decision_level` + /// Invariant: there may be no decisions any level below `last_assumption_level` + last_assumption_level: DecLvl, pub stats: Stats, /// A data structure with the various communication channels /// needed to receive/send updates and commands. @@ -82,6 +89,7 @@ impl Solver { brancher: default_brancher(), reasoners: Reasoners::new(), decision_level: DecLvl::ROOT, + last_assumption_level: DecLvl::ROOT, stats: Default::default(), sync: Synchro::new(), } @@ -510,7 +518,7 @@ impl Solver { /// Searches for the first satisfying assignment, returning none if the search /// space was exhausted without encountering a solution. pub fn solve(&mut self) -> Result>, Exit> { - match self._solve(DecLvl::ROOT)? { + match self.search()? { SolveResult::AtSolution => Ok(Some(Arc::new(self.model.state.clone()))), SolveResult::ExternalSolution(s) => Ok(Some(s)), SolveResult::Unsat(_) => Ok(None), @@ -519,7 +527,12 @@ impl Solver { /// Enumerates all possible values for the given variables. /// Returns a list of assignments, where each assigment is a vector of values for the variables given as input + /// + /// IMPORTANT: this method will post non-removable clauses to block solutions. So even resetting will not bring + /// the solver back to its previous state. The solver should be cloned before calling enumerate if it is + /// needed for something else. pub fn enumerate(&mut self, variables: &[VarRef]) -> Result>, Exit> { + assert_eq!(self.decision_level, DecLvl::ROOT); debug_assert!( { variables @@ -533,7 +546,7 @@ impl Solver { let mut valid_assignments = Vec::with_capacity(64); loop { - match self._solve(DecLvl::ROOT)? { + match self.search()? { SolveResult::Unsat(_) => return Ok(valid_assignments), SolveResult::AtSolution => { // found a solution. record the corresponding assignment and add a clause forbidding it in future solutions @@ -547,7 +560,7 @@ impl Solver { } valid_assignments.push(assignment); - if let Some(dl) = self.backtrack_level_for_clause(&clause, DecLvl::ROOT) { + if let Some(dl) = self.backtrack_level_for_clause(&clause) { self.restore(dl); self.reasoners.sat.add_clause(clause); } else { @@ -566,39 +579,23 @@ impl Solver { // make sure brancher has knowledge of all variables. self.brancher.import_vars(&self.model); - // TODO? let start_time = Instant::now(); - // TODO? let start_cycles = StartCycleCount::now(); + assert_eq!(self.decision_level, DecLvl::ROOT); - match self.propagate_and_backtrack_to_consistent(self.current_decision_level()) { + match self.propagate_and_backtrack_to_consistent() { Ok(()) => (), Err(conflict) => { + // conflict at root, return empty unsat core debug_assert!(conflict.is_empty()); return Ok(Err(Explanation::new())); } }; for lit in assumption_lits { - match self.assume(lit) { - Ok(_) => { - if let Err(conflict) = self.propagate_and_backtrack_to_consistent(self.current_decision_level()) { - let unsat_core = self - .model - .state - .extract_unsat_core_after_conflict(conflict, &mut self.reasoners); - return Ok(Err(unsat_core)); - } - } - Err(failed) => { - let unsat_core = self - .model - .state - .extract_unsat_core_after_invalid_update(failed, &mut self.reasoners); - return Ok(Err(unsat_core)); - } + if let Err(unsat_core) = self.assume_and_propagate(lit) { + return Ok(Err(unsat_core)); } } - let last_assumption_dec_lvl = self.current_decision_level(); - match self._solve(last_assumption_dec_lvl)? { + match self.search()? { SolveResult::AtSolution => Ok(Ok(Arc::new(self.model.state.clone()))), SolveResult::ExternalSolution(s) => Ok(Ok(s)), SolveResult::Unsat(conflict) => { @@ -614,7 +611,7 @@ impl Solver { /// Implementation of the public facing `solve()` method that provides more control. /// In particular, the output distinguishes between whether the solution was found by this /// solver or another one (i.e. was read from the input channel). - fn _solve(&mut self, last_assumption_dec_lvl: DecLvl) -> Result { + fn search(&mut self) -> Result { // make sure brancher has knowledge of all variables. self.brancher.import_vars(&self.model); @@ -639,7 +636,7 @@ impl Solver { } } - if let Err(conflict) = self.propagate_and_backtrack_to_consistent(last_assumption_dec_lvl) { + if let Err(conflict) = self.propagate_and_backtrack_to_consistent() { // UNSAT self.stats.solve_time += start_time.elapsed(); self.stats.solve_cycles += start_cycles.elapsed(); @@ -651,7 +648,7 @@ impl Solver { self.decide(lit); } Some(Decision::Restart) => { - self.restore(last_assumption_dec_lvl); + self.reset_search(); self.stats.add_restart(); } None => { @@ -699,14 +696,16 @@ impl Solver { minimize: bool, mut on_new_solution: impl FnMut(IntCst, &SavedAssignment), ) -> Result)>, Exit> { + assert_eq!(self.decision_level, DecLvl::ROOT); + assert_eq!(self.last_assumption_level, DecLvl::ROOT); // best solution found so far let mut best = None; - let mut must_improve_lits = Vec::new(); loop { - let sol = match self.solve_with_assumptions(must_improve_lits.clone())? { - Ok(sol) => { + let sol = match self.search()? { + SolveResult::AtSolution => { // solver stopped at a solution, this is necessarily an improvement on the best solution found so far // notify other solvers that we have found a new solution + let sol = Arc::new(self.model.state.clone()); self.sync.notify_solution_found(sol.clone()); let objective_value = sol.var_domain(objective).lb; on_new_solution(objective_value, &sol); @@ -714,13 +713,10 @@ impl Solver { println!("********* New sol: {objective_value} *********"); self.print_stats(); } - self.restore(DecLvl::new(must_improve_lits.len().try_into().unwrap())); sol } - Err(_) => { - // exhausted search space, return the best result found so far - return Ok(best); - } + SolveResult::ExternalSolution(sol) => sol, // a solution was handed to us by another solver + SolveResult::Unsat(_conflict) => return Ok(best), // exhausted search space under the current wuality assumptions }; // determine whether the solution found is an improvement on the previous one (might not be the case if sent by another solver) @@ -747,10 +743,15 @@ impl Solver { best = Some((objective_value, sol)); // force future solutions to improve on this one - if minimize { - must_improve_lits.push(objective.lt_lit(objective_value)); + let improvement_literal = if minimize { + objective.lt_lit(objective_value) } else { - must_improve_lits.push(objective.gt_lit(objective_value)); + objective.gt_lit(objective_value) + }; + self.reset_search(); + match self.assume_and_propagate(improvement_literal) { + Ok(_) => {} + Err(_unsat_core) => return Ok(best), // no way to improve this bound } } } @@ -769,28 +770,70 @@ impl Solver { self.stats.add_decision(decision) } - pub fn assume(&mut self, assumption: Lit) -> Result { - assert!( + /// Posts an assumption on a new decision level and returns an `UnsatCore` if the assumption + /// is trivially inconsistent with the previous ones (without running any propagation). + /// + /// If the assumption is accepted, returns an `Ok(x)` result where `x` is true iff the assumption was not already entailed + /// (i.e. something changed in the domains). + pub fn assume(&mut self, assumption: Lit) -> Result { + assert_eq!(self.last_assumption_level, self.decision_level); + debug_assert!( self.model.state.decisions().is_empty(), "Not allowed to make assumptions after solver already started making decisions (i.e. started solving) !", ); self.save_state(); - self.model.state.assume(assumption) + self.last_assumption_level = self.decision_level; + match self.model.state.assume(assumption) { + Ok(status) => Ok(status), + Err(invalid_update) => { + // invalid update, transform it int an unsat core + Err(self + .model + .state + .extract_unsat_core_after_invalid_update(invalid_update, &mut self.reasoners)) + } + } } - /// Determines the appropriate backtrack level for this clause and returns the literal that - /// is asserted at this level. + /// Posts an assumptions on a new decision level, run all propagators and returns an `UnsatCore` + /// if the assumptions turns out to be incompatibly with previous ones. /// - /// The common understanding is that it should be the earliest level at which the clause is unit. - /// However, the explanation of eager propagation of optional might generate explanations where some - /// literals are not violated, those are ignored in determining the asserting level. + /// If the assumption is accepted returns an `Ok(x)` result where is true if the assumption was not already entailed + /// (i.e. something changed in the domains). + pub fn assume_and_propagate(&mut self, assumption: Lit) -> Result { + if self.assume(assumption)? { + // the assumption changed something in the domain + match self.propagate_and_backtrack_to_consistent() { + Ok(_) => Ok(true), + Err(conflict) => Err(self + .model + .state + .extract_unsat_core_after_conflict(conflict, &mut self.reasoners)), + } + } else { + // no changes made by the asssumption + Ok(false) + } + } + + /// Determines the appropriate backtrack level for this clause, i.e., the earliest level at which + /// the clause is unit. /// /// If there is more that one violated literal at the latest level, then no literal is asserted /// and the bactrack level is set to the ante-last level (might occur with clause sharing). - fn backtrack_level_for_clause(&self, clause: &[Lit], last_assumption_dec_lvl: DecLvl) -> Option { + /// + /// If the last level at which the clause is not violated is an assumption level, then the method returns + /// None, meaning that the problem cannot be made SAT without relaxing the assumptions. + fn backtrack_level_for_clause(&self, clause: &[Lit]) -> Option { debug_assert_eq!(self.model.state.value_of_clause(clause.iter().copied()), Some(false)); - - // level of the two latest set element of the clause + let last_assumption_dec_lvl = self.last_assumption_level; + + // level of the two latest set element of the clause. + // Those are set to the last assumption level beyond which we cannot backtrack + // Note that this may artificially "delay" the propagation of a unit clause to a level + // beyond the one it became unit. As a result when relaxing assumptions, we may undo the consequences of the propagation + // even though the clause remains unit. Since this will only occur for learnt clauses it is not a problem + // for correctness but may result in redundant work. let mut max = last_assumption_dec_lvl; let mut max_next = last_assumption_dec_lvl; @@ -808,10 +851,14 @@ impl Solver { } debug_assert!(max >= last_assumption_dec_lvl); if max == last_assumption_dec_lvl { + // clause is still violated on the last assumption level None } else if max == max_next { Some(max - 1) } else { + // indicate that we may backtrack to the first level where the clause is unit + // (but not earlier that the last assumption level) + debug_assert!(max_next >= last_assumption_dec_lvl); Some(max_next) } } @@ -821,7 +868,7 @@ impl Solver { /// As a side effect, the activity of the variables in the clause will be increased. /// Returns `false` if the clause is conflicting at the root and thus constitutes a contradiction. #[must_use] - fn add_conflicting_clause_and_backtrack(&mut self, expl: &Conflict, last_assumption_dec_lvl: DecLvl) -> bool { + fn add_conflicting_clause_and_backtrack(&mut self, expl: &Conflict) -> bool { // // print the clause before analysis // println!("conflict ({}) :", expl.literals().len()); // for &l in expl.literals() { @@ -845,7 +892,7 @@ impl Solver { // // println!("]"); // } // println!(); - if let Some(dl) = self.backtrack_level_for_clause(expl.literals(), last_assumption_dec_lvl) { + if let Some(dl) = self.backtrack_level_for_clause(expl.literals()) { // inform the brancher that we are in a conflict state self.brancher.conflict(expl, &self.model, &mut self.reasoners, dl); // backtrack @@ -879,7 +926,7 @@ impl Solver { /// - propagating in the current state /// - return if no conflict was detected /// - otherwise: learn a conflicting clause, backtrack up the decision tree and repeat the process. - pub fn propagate_and_backtrack_to_consistent(&mut self, last_assumption_dec_lvl: DecLvl) -> Result<(), Conflict> { + pub fn propagate_and_backtrack_to_consistent(&mut self) -> Result<(), Conflict> { loop { match self.propagate() { Ok(()) => return Ok(()), @@ -891,7 +938,7 @@ impl Solver { conflict.literals().iter().map(|l| self.model.fmt(*l)).format(" | ") ); self.sync.notify_learnt(&conflict.clause); - if self.add_conflicting_clause_and_backtrack(&conflict, last_assumption_dec_lvl) { + if self.add_conflicting_clause_and_backtrack(&conflict) { // we backtracked, loop again to propagate } else { // could not backtrack to a non-conflicting state, UNSAT @@ -996,6 +1043,12 @@ impl Solver { th.print_stats(); } } + + /// Undo any decision that was made. + /// This results in backtracking to the last assumption level (or to the ROOT if no assumption was made). + pub fn reset_search(&mut self) { + self.restore(self.last_assumption_level); + } } impl Backtrack for Solver { @@ -1033,6 +1086,9 @@ impl Backtrack for Solver { fn restore(&mut self, saved_id: DecLvl) { self.decision_level = saved_id; + if self.last_assumption_level > saved_id { + self.last_assumption_level = saved_id; + } self.model.restore(saved_id); self.brancher.restore(saved_id); for w in self.reasoners.writers() { @@ -1051,6 +1107,7 @@ impl Clone for Solver { brancher: self.brancher.clone_to_box(), reasoners: self.reasoners.clone(), decision_level: self.decision_level, + last_assumption_level: self.last_assumption_level, stats: self.stats.clone(), sync: self.sync.clone(), } From 2d18a814756f0e2c28ce82c0d82cde704fcff2b8 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Tue, 7 Jan 2025 17:00:39 +0100 Subject: [PATCH 11/16] fix(solver): enforce all constraints to be manually posted before search/decide/assume --- solver/src/solver/solver_impl.rs | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs index 91992db4..495190f6 100644 --- a/solver/src/solver/solver_impl.rs +++ b/solver/src/solver/solver_impl.rs @@ -498,9 +498,14 @@ impl Solver { (disjuncts.into(), Lit::TRUE) } + /// Returns true if all constraints are posted. + fn all_constraints_posted(&self) -> bool { + self.next_unposted_constraint == self.model.shape.constraints.len() + } + /// Post all constraints of the model that have not been previously posted. fn post_constraints(&mut self) -> Result<(), InvalidUpdate> { - if self.next_unposted_constraint == self.model.shape.constraints.len() { + if self.all_constraints_posted() { return Ok(()); // fast path that avoids updating metrics } let start_time = Instant::now(); @@ -518,6 +523,10 @@ impl Solver { /// Searches for the first satisfying assignment, returning none if the search /// space was exhausted without encountering a solution. pub fn solve(&mut self) -> Result>, Exit> { + if self.post_constraints().is_err() { + return Ok(None); + } + match self.search()? { SolveResult::AtSolution => Ok(Some(Arc::new(self.model.state.clone()))), SolveResult::ExternalSolution(s) => Ok(Some(s)), @@ -545,6 +554,10 @@ impl Solver { ); let mut valid_assignments = Vec::with_capacity(64); + if self.post_constraints().is_err() { + // Trivially UNSAT, return the empty vec of valid assignments + return Ok(valid_assignments); + } loop { match self.search()? { SolveResult::Unsat(_) => return Ok(valid_assignments), @@ -612,6 +625,7 @@ impl Solver { /// In particular, the output distinguishes between whether the solution was found by this /// solver or another one (i.e. was read from the input channel). fn search(&mut self) -> Result { + assert!(self.all_constraints_posted()); // make sure brancher has knowledge of all variables. self.brancher.import_vars(&self.model); @@ -700,6 +714,12 @@ impl Solver { assert_eq!(self.last_assumption_level, DecLvl::ROOT); // best solution found so far let mut best = None; + + if self.post_constraints().is_err() { + // trivially UNSAT + return Ok(None); + } + loop { let sol = match self.search()? { SolveResult::AtSolution => { @@ -758,6 +778,7 @@ impl Solver { } pub fn decide(&mut self, decision: Lit) { + assert!(self.all_constraints_posted()); self.save_state(); log_dec!( "decision: {:?} -- {} dom:{:?}", @@ -776,6 +797,7 @@ impl Solver { /// If the assumption is accepted, returns an `Ok(x)` result where `x` is true iff the assumption was not already entailed /// (i.e. something changed in the domains). pub fn assume(&mut self, assumption: Lit) -> Result { + assert!(self.all_constraints_posted()); assert_eq!(self.last_assumption_level, self.decision_level); debug_assert!( self.model.state.decisions().is_empty(), From 9891dddba6a9627b91748ec7a7b02796fe201c4d Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Wed, 8 Jan 2025 14:11:53 +0100 Subject: [PATCH 12/16] feat(solver): Make sure search always let the solver in a fully propagated state. --- solver/src/solver/solver_impl.rs | 78 +++++++++++++++++++++----------- 1 file changed, 52 insertions(+), 26 deletions(-) diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs index 495190f6..a6d1971f 100644 --- a/solver/src/solver/solver_impl.rs +++ b/solver/src/solver/solver_impl.rs @@ -40,8 +40,8 @@ macro_rules! log_dec { } } -/// Result of the `_solve` method. -enum SolveResult { +/// Result of the `search` method. +enum SearchResult { /// A solution was found through search and the solver's assignment is on this solution AtSolution, /// The solver was made aware of a solution from its input channel. @@ -528,9 +528,9 @@ impl Solver { } match self.search()? { - SolveResult::AtSolution => Ok(Some(Arc::new(self.model.state.clone()))), - SolveResult::ExternalSolution(s) => Ok(Some(s)), - SolveResult::Unsat(_) => Ok(None), + SearchResult::AtSolution => Ok(Some(Arc::new(self.model.state.clone()))), + SearchResult::ExternalSolution(s) => Ok(Some(s)), + SearchResult::Unsat(_) => Ok(None), } } @@ -560,8 +560,8 @@ impl Solver { } loop { match self.search()? { - SolveResult::Unsat(_) => return Ok(valid_assignments), - SolveResult::AtSolution => { + SearchResult::Unsat(_) => return Ok(valid_assignments), + SearchResult::AtSolution => { // found a solution. record the corresponding assignment and add a clause forbidding it in future solutions let mut assignment = Vec::with_capacity(variables.len()); let mut clause = Vec::with_capacity(variables.len() * 2); @@ -580,7 +580,7 @@ impl Solver { return Ok(valid_assignments); } } - SolveResult::ExternalSolution(_) => panic!(), + SearchResult::ExternalSolution(_) => panic!(), } } } @@ -609,9 +609,9 @@ impl Solver { } } match self.search()? { - SolveResult::AtSolution => Ok(Ok(Arc::new(self.model.state.clone()))), - SolveResult::ExternalSolution(s) => Ok(Ok(s)), - SolveResult::Unsat(conflict) => { + SearchResult::AtSolution => Ok(Ok(Arc::new(self.model.state.clone()))), + SearchResult::ExternalSolution(s) => Ok(Ok(s)), + SearchResult::Unsat(conflict) => { let unsat_core = self .model .state @@ -621,10 +621,26 @@ impl Solver { } } - /// Implementation of the public facing `solve()` method that provides more control. - /// In particular, the output distinguishes between whether the solution was found by this - /// solver or another one (i.e. was read from the input channel). - fn search(&mut self) -> Result { + /// Searches for a satisfying solution that fulfills the posted assumptions. + /// The search might start from any node (with or without decisions already taken) and is allowed to undo + /// any previous decision. However it will maintain all posted assumptions and may only backtrack to the level of the last one + /// (or ROOT in the absence of assumptions). + /// + /// Search will stop when either: + /// - the solver is at a solution `Ok(AtSolution)`. + /// In this case the solution can be extracted from the current domains. + /// - the solver proved unsatisfiability under the current assumption `Ok(Unsat)`. + /// In this case, a conflict will be provided from which an UNSAT core can be built. + /// + /// The method may return as well when: + /// - the solver receives an `Interrupt` message. Result: `Err(Interrupted)` + /// - the solver receives an external solution. Result: `Ok(ExternalSolution)`. + /// In this case the solver will return the external solution, which is intended to be handled by the caller + /// (typically to set up new upper bonds before calling search again). + /// + /// Invariant: when exiting, the `search` method will always let the solver in a state where all reasoners are fully propagated. + /// The only exceptions is redundant clauses received from an external process that may still be pending (but those can be handled in any ddecision level). + fn search(&mut self) -> Result { assert!(self.all_constraints_posted()); // make sure brancher has knowledge of all variables. self.brancher.import_vars(&self.model); @@ -632,6 +648,17 @@ impl Solver { let start_time = Instant::now(); let start_cycles = StartCycleCount::now(); loop { + // first propagate everything to make sure we are in a clean, consistent state + // note that this method call will have the search backtrack when encountering an inconsistent state + if let Err(conflict) = self.propagate_and_backtrack_to_consistent() { + // UNSAT + self.stats.solve_time += start_time.elapsed(); + self.stats.solve_cycles += start_cycles.elapsed(); + return Ok(SearchResult::Unsat(conflict)); + } + + // in a consistent state, check for any incoming messages that may cause us to exit the search + let mut requires_new_propagation = false; while let Ok(signal) = self.sync.signals.try_recv() { match signal { InputSignal::Interrupt => { @@ -641,20 +668,19 @@ impl Solver { } InputSignal::LearnedClause(cl) => { self.reasoners.sat.add_forgettable_clause(cl.as_ref()); + requires_new_propagation = true; } InputSignal::SolutionFound(assignment) => { self.stats.solve_time += start_time.elapsed(); self.stats.solve_cycles += start_cycles.elapsed(); - return Ok(SolveResult::ExternalSolution(assignment)); + return Ok(SearchResult::ExternalSolution(assignment)); } } } - - if let Err(conflict) = self.propagate_and_backtrack_to_consistent() { - // UNSAT - self.stats.solve_time += start_time.elapsed(); - self.stats.solve_cycles += start_cycles.elapsed(); - return Ok(SolveResult::Unsat(conflict)); + if requires_new_propagation { + // at least one new redundant clause added, go back directly to propagation + // to handle it before taking a decision + continue; } match self.brancher.next_decision(&self.stats, &self.model) { Some(Decision::SetLiteral(lit)) => { @@ -674,7 +700,7 @@ impl Solver { self.model.shape.validate(&self.model.state).unwrap(); true }); - return Ok(SolveResult::AtSolution); + return Ok(SearchResult::AtSolution); } } } @@ -722,7 +748,7 @@ impl Solver { loop { let sol = match self.search()? { - SolveResult::AtSolution => { + SearchResult::AtSolution => { // solver stopped at a solution, this is necessarily an improvement on the best solution found so far // notify other solvers that we have found a new solution let sol = Arc::new(self.model.state.clone()); @@ -735,8 +761,8 @@ impl Solver { } sol } - SolveResult::ExternalSolution(sol) => sol, // a solution was handed to us by another solver - SolveResult::Unsat(_conflict) => return Ok(best), // exhausted search space under the current wuality assumptions + SearchResult::ExternalSolution(sol) => sol, // a solution was handed to us by another solver + SearchResult::Unsat(_conflict) => return Ok(best), // exhausted search space under the current wuality assumptions }; // determine whether the solution found is an improvement on the previous one (might not be the case if sent by another solver) From ccdd4181bfca41beeaf3f33cb13be9a19f65853d Mon Sep 17 00:00:00 2001 From: Nika Beriachvili Date: Wed, 8 Jan 2025 16:26:33 +0100 Subject: [PATCH 13/16] fix(unsat cores): fix wrong literal (implied *by* an assumption) being returned in an unsat core and add test could only happen for literals on non-boolean variables, which is why previous tests did not detect this bug --- solver/src/core/state/domains.rs | 73 ++++++++++++++++++++++++++++++-- 1 file changed, 70 insertions(+), 3 deletions(-) diff --git a/solver/src/core/state/domains.rs b/solver/src/core/state/domains.rs index 37da5567..36ed3b6e 100644 --- a/solver/src/core/state/domains.rs +++ b/solver/src/core/state/domains.rs @@ -545,8 +545,9 @@ impl Domains { loop { for l in explanation.lits.drain(..) { if let Some(loc) = self.implying_event(l) { - if self.trail().get_event(loc).cause == Origin::ASSUMPTION { - result.lits.push(l); + let ev = self.trail().get_event(loc); + if ev.cause == Origin::ASSUMPTION { + result.lits.push(ev.new_literal()); } else { debug_assert!(self.entails(l)); self.queue.push(loc, l); @@ -1021,7 +1022,7 @@ mod tests { } #[test] - fn test_unsat_core_extraction() { + fn test_unsat_core_extraction_bool() { let mut model = Domains::new(); let a = Lit::geq(model.new_var(0, 1), 1); let b = Lit::geq(model.new_var(0, 1), 1); @@ -1191,4 +1192,70 @@ mod tests { expected.insert(h); assert_eq!(unsat_core_set, expected); } + + #[test] + fn test_unsat_core_extraction_int() { + let mut model = Domains::new(); + let x = model.new_var(0, 10); + let y = model.new_var(0, 10); + + // assumptions: [x <= 3], [y <= 4] + // constraint: [x <= 5] => [y >= 6] + + let writer = ReasonerId::Sat; + + let cause_xleq5 = Cause::inference(writer, 0u32); + + #[allow(unused_must_use)] + let propagate = |model: &mut Domains| -> Result { + if model.entails(x.leq(5)) { + model.set(y.geq(6), cause_xleq5)?; + } + Ok(true) + }; + + struct Expl { + x: VarRef, + y: VarRef, + } + impl Explainer for Expl { + fn explain( + &mut self, + cause: InferenceCause, + literal: Lit, + _model: &DomainsSnapshot, + explanation: &mut Explanation, + ) { + assert_eq!(cause.writer, ReasonerId::Sat); + match cause.payload { + 0 => { + assert_eq!(literal, !(self.y.leq(4))); // i.e. y.geq(5) + explanation.push(self.x.leq(5)); + } + _ => panic!("unexpected payload"), + } + } + } + + let mut network = Expl { x, y }; + + propagate(&mut model).unwrap(); + + model.save_state(); + assert!(model.assume(x.leq(3)).unwrap()); + assert_eq!(model.bounds(x.variable()), (0, 3)); + propagate(&mut model).unwrap(); + assert_eq!(model.bounds(y.variable()), (6, 10)); + + model.save_state(); + let err = model.assume(y.leq(4)).unwrap_err(); + + let unsat_core = model.extract_unsat_core_after_invalid_update(err, &mut network).lits; + let unsat_core_set: HashSet = unsat_core.iter().copied().collect(); + + let mut expected = HashSet::new(); + expected.insert(x.leq(3)); // Previously, an unfixed bug would result in [x <= 5] instead of the "actual" assumption [x <= 3] + expected.insert(y.leq(4)); + assert_eq!(unsat_core_set, expected); + } } From 5bd1707d2facadec8c713966d41d4a50ad7e1d89 Mon Sep 17 00:00:00 2001 From: Nika Beriachvili Date: Wed, 8 Jan 2025 16:29:27 +0100 Subject: [PATCH 14/16] chore: fix formatting --- solver/src/core/state/domains.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/solver/src/core/state/domains.rs b/solver/src/core/state/domains.rs index 36ed3b6e..e543f811 100644 --- a/solver/src/core/state/domains.rs +++ b/solver/src/core/state/domains.rs @@ -1252,7 +1252,7 @@ mod tests { let unsat_core = model.extract_unsat_core_after_invalid_update(err, &mut network).lits; let unsat_core_set: HashSet = unsat_core.iter().copied().collect(); - + let mut expected = HashSet::new(); expected.insert(x.leq(3)); // Previously, an unfixed bug would result in [x <= 5] instead of the "actual" assumption [x <= 3] expected.insert(y.leq(4)); From d232bb34448922dbdd3aca9bfef26c8ddc29f0c4 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Wed, 8 Jan 2025 16:48:10 +0100 Subject: [PATCH 15/16] chore(solver): Make explanation API more robust to violated assumptions --- solver/src/core/state/domains.rs | 124 +++++++++++++++++---------- solver/src/core/state/explanation.rs | 13 ++- solver/src/reasoners/eq/dense.rs | 8 +- solver/src/solver/solver_impl.rs | 9 +- 4 files changed, 101 insertions(+), 53 deletions(-) diff --git a/solver/src/core/state/domains.rs b/solver/src/core/state/domains.rs index e543f811..0ba28001 100644 --- a/solver/src/core/state/domains.rs +++ b/solver/src/core/state/domains.rs @@ -1,3 +1,5 @@ +use itertools::Itertools; + use crate::backtrack::{Backtrack, DecLvl, DecisionLevelClass, EventIndex, ObsTrail}; use crate::collections::ref_store::RefMap; use crate::core::literals::{Disjunction, DisjunctionBuilder, ImplicationGraph, LitSet}; @@ -6,6 +8,7 @@ use crate::core::state::event::Event; use crate::core::state::int_domains::IntDomains; use crate::core::state::{Cause, DomainsSnapshot, Explainer, Explanation, ExplanationQueue, InvalidUpdate, OptDomain}; use crate::core::*; +use crate::solver::UnsatCore; use std::fmt::{Debug, Formatter}; #[cfg(debug_assertions)] @@ -409,14 +412,21 @@ impl Domains { /// where: /// /// - the literals `l_i` are entailed at the previous decision level of the current state, - /// - the literal `l_dec` is the decision that was taken at the current decision level. + /// - the literal `l_dec` is a literal that was decided or inferred at the current decision level. /// /// The update of `l` must not directly originate from a decision as it is necessarily the case that /// `!l` holds in the current state. It is thus considered a logic error to impose an obviously wrong decision. /// /// It can, however, directly originate from an assumption (in which case we are necessarily UNSAT, by the way). - pub fn clause_for_invalid_update(&mut self, failed: InvalidUpdate, explainer: &mut impl Explainer) -> Conflict { + pub fn clause_for_invalid_inferrence(&mut self, failed: InvalidUpdate, explainer: &mut impl Explainer) -> Conflict { let InvalidUpdate(literal, cause) = failed; + debug_assert!( + !matches!( + cause, + Origin::Direct(DirectOrigin::Decision | DirectOrigin::Assumption | DirectOrigin::Encoding) + ), + "The cause is not an inferrence" + ); debug_assert!(!self.entails(literal)); // an update is invalid iff its negation holds AND the affected variable is present @@ -429,13 +439,12 @@ impl Domains { explanation.push(!literal); explanation.push(self.presence(literal)); - if cause != Origin::ASSUMPTION { - // However, `literal` does not hold in the current state and we need to replace it. - // Thus we replace it with a set of literals `x_1 & ... & x_m` such that - // `x_1 & ... & x_m -> literal` - self.add_implying_literals_to_explanation(literal, cause, &mut explanation, explainer); - } - debug_assert!(explanation.lits.iter().copied().all(|l| self.entails(l))); + // However, `literal` does not hold in the current state and we need to replace it. + // Thus we replace it with a set of literals `x_1 & ... & x_m` such that + // `x_1 & ... & x_m -> literal` + self.add_implying_literals_to_explanation(literal, cause, &mut explanation, explainer); + + debug_assert!(explanation.literals().iter().all(|&l| self.entails(l))); // now all disjuncts hold in the current state // we then transform this clause to be in the first unique implication point (1UIP) form. @@ -534,11 +543,12 @@ impl Domains { fn extract_assumptions_implying( &mut self, - explanation: &mut Explanation, + mut explanation: Explanation, explainer: &mut impl Explainer, ) -> Explanation { - debug_assert!(explanation.lits.iter().all(|&l| self.entails(l))); - let mut result = Explanation::new(); + debug_assert!(explanation.literals().iter().all(|&l| self.entails(l))); + // accumulate assumption literals in a set of literals to eliminate redudant elements + let mut result = LitSet::new(); self.queue.clear(); @@ -546,11 +556,21 @@ impl Domains { for l in explanation.lits.drain(..) { if let Some(loc) = self.implying_event(l) { let ev = self.trail().get_event(loc); - if ev.cause == Origin::ASSUMPTION { - result.lits.push(ev.new_literal()); - } else { - debug_assert!(self.entails(l)); - self.queue.push(loc, l); + // event is not entailed at root, we need to consider it + match ev.cause { + Origin::Direct(DirectOrigin::Assumption) => { + result.insert(ev.new_literal()); + } + Origin::Direct(DirectOrigin::Decision) => { + panic!("Unexpected decision in trail, when trying to extract an unsat core"); + } + Origin::Direct(DirectOrigin::Encoding) => { + debug_assert_eq!(self.entailing_level(l), DecLvl::ROOT); + } + _ => { + debug_assert!(self.entails(l)); + self.queue.push(loc, l); + } } } } @@ -561,32 +581,43 @@ impl Domains { } let (lit, _) = self.queue.pop().unwrap(); - if let Some(implying_lits) = self.implying_literals(lit, explainer) { - explanation.lits.extend(implying_lits); - } + let implying_lits = self.implying_literals(lit, explainer).expect("Encountered "); + explanation.extend(implying_lits); } - result + UnsatCore::from(Vec::from(result)) } - pub fn extract_unsat_core_after_invalid_update( + /// Extract an UNSAT core after a failure to impose or propagate an assumption. + pub fn extract_unsat_core_after_invalid_assumption( &mut self, failed: InvalidUpdate, explainer: &mut impl Explainer, - ) -> Explanation { + ) -> UnsatCore { let InvalidUpdate(literal, cause) = failed; - debug_assert!(!self.entails(literal)); - let mut explanation = Explanation::new(); - explanation.lits = self - .clause_for_invalid_update(failed, explainer) - .clause - .literals() - .iter() - .map(|&l| !l) - .collect(); - - let mut unsat_core = self.extract_assumptions_implying(&mut explanation, explainer); + debug_assert!( + !matches!(cause, Origin::Direct(DirectOrigin::Decision | DirectOrigin::Encoding)), + "The cause is neither an inferrence nor an assumption" + ); + + let mut base_unsat_core = None; + + // The base of the conflict is `literal & !literal & prez(literal)` + // however literal could not be imposed in the model, so we treat it differently. + let mut base_conflict = Explanation::from(vec![!literal, self.presence(literal)]); + if cause == Origin::ASSUMPTION { - unsat_core.lits.push(literal); + // The literal cannot be explained (not an inferrence). + // Set it aside, we will add it to the UNSAT core at the end + base_unsat_core = Some(literal); + } else { + // the literal is inferred, add its implicants to the conflict set + self.add_implying_literals_to_explanation(literal, cause, &mut base_conflict, explainer); + } + + let mut unsat_core = self.extract_assumptions_implying(base_conflict, explainer); + if let Some(base_literal) = base_unsat_core { + // add the initial assumption to the unsat core + unsat_core.push(base_literal); } unsat_core } @@ -595,10 +626,9 @@ impl Domains { &mut self, conflict: Conflict, explainer: &mut impl Explainer, - ) -> Explanation { - let mut explanation = Explanation::new(); - explanation.lits = conflict.clause.literals().iter().map(|&l| !l).collect(); - self.extract_assumptions_implying(&mut explanation, explainer) + ) -> UnsatCore { + let explanation = Explanation::from(conflict.clause.literals().iter().map(|&l| !l).collect_vec()); + self.extract_assumptions_implying(explanation, explainer) } /// Returns all decisions that were taken since the root decision level. @@ -985,7 +1015,7 @@ mod tests { _ => panic!(), }; - let clause = model.clause_for_invalid_update(err, &mut network); + let clause = model.clause_for_invalid_inferrence(err, &mut network); let clause: HashSet<_> = clause.literals().iter().copied().collect(); // we have three rules @@ -1150,7 +1180,7 @@ mod tests { _ => panic!(), }; - let conflict = model.clause_for_invalid_update(err, &mut network); + let conflict = model.clause_for_invalid_inferrence(err, &mut network); let unsat_core = model.extract_unsat_core_after_conflict(conflict, &mut network).lits; let unsat_core_set: HashSet = unsat_core.iter().copied().collect(); @@ -1169,7 +1199,9 @@ mod tests { _ => panic!(), }; - let unsat_core = model.extract_unsat_core_after_invalid_update(err, &mut network).lits; + let unsat_core = model + .extract_unsat_core_after_invalid_assumption(err, &mut network) + .lits; let unsat_core_set: HashSet = unsat_core.iter().copied().collect(); let mut expected = HashSet::new(); @@ -1183,7 +1215,9 @@ mod tests { model.save_state(); let err = model.assume(h).unwrap_err(); - let unsat_core = model.extract_unsat_core_after_invalid_update(err, &mut network).lits; + let unsat_core = model + .extract_unsat_core_after_invalid_assumption(err, &mut network) + .lits; let unsat_core_set: HashSet = unsat_core.iter().copied().collect(); let mut expected = HashSet::new(); @@ -1250,7 +1284,9 @@ mod tests { model.save_state(); let err = model.assume(y.leq(4)).unwrap_err(); - let unsat_core = model.extract_unsat_core_after_invalid_update(err, &mut network).lits; + let unsat_core = model + .extract_unsat_core_after_invalid_assumption(err, &mut network) + .lits; let unsat_core_set: HashSet = unsat_core.iter().copied().collect(); let mut expected = HashSet::new(); diff --git a/solver/src/core/state/explanation.rs b/solver/src/core/state/explanation.rs index 9f005caf..eaea1cab 100644 --- a/solver/src/core/state/explanation.rs +++ b/solver/src/core/state/explanation.rs @@ -6,7 +6,7 @@ use std::collections::BinaryHeap; /// Builder for a conjunction of literals that make the explained literal true #[derive(Clone, Debug)] pub struct Explanation { - pub lits: Vec, + pub(crate) lits: Vec, } impl Explanation { pub fn new() -> Self { @@ -23,6 +23,11 @@ impl Explanation { pub fn push(&mut self, lit: Lit) { self.lits.push(lit) } + + pub fn extend(&mut self, additional_lits: impl IntoIterator) { + self.lits.extend(additional_lits); + } + pub fn pop(&mut self) -> Option { self.lits.pop() } @@ -41,6 +46,12 @@ impl Default for Explanation { } } +impl From> for Explanation { + fn from(lits: Vec) -> Self { + Explanation { lits } + } +} + pub trait Explainer { fn explain(&mut self, cause: InferenceCause, literal: Lit, model: &DomainsSnapshot, explanation: &mut Explanation); } diff --git a/solver/src/reasoners/eq/dense.rs b/solver/src/reasoners/eq/dense.rs index 2849707c..e3e25b0f 100644 --- a/solver/src/reasoners/eq/dense.rs +++ b/solver/src/reasoners/eq/dense.rs @@ -635,10 +635,10 @@ impl DenseEqTheory { /// DomNeq: (x != v) & (x <= v) => (x <= v - 1) /// (x != v) & (x >= v) => (x >= v + 1) /// (x != v) & (-x <= -v) => (-x <= -v-1) (rewrite of previous for uniformity with signed vars - /// - /// DomUpper: (x <= v) => (x != v+1) + /// + /// DomUpper: (x <= v) => (x != v+1) /// DomLower: (x >= v) => (x != v-1) - /// DomSingleton: (x >= v) & (x <= v) => (x = v) + /// DomSingleton: (x >= v) & (x <= v) => (x = v) pub fn propagate_domain_event( &mut self, v: SignedVar, @@ -1142,7 +1142,7 @@ mod tests { }; let explainer = &mut SingleTheoryExplainer(&mut theory); let clause = match contradiction { - Contradiction::InvalidUpdate(up) => domains.clause_for_invalid_update(up, explainer), + Contradiction::InvalidUpdate(up) => domains.clause_for_invalid_inferrence(up, explainer), Contradiction::Explanation(expl) => domains.refine_explanation(expl, explainer), }; println!("ab: {ab:?}, bc: {bc:?}, ac: {ac:?}"); diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs index a6d1971f..d30264f9 100644 --- a/solver/src/solver/solver_impl.rs +++ b/solver/src/solver/solver_impl.rs @@ -838,7 +838,7 @@ impl Solver { Err(self .model .state - .extract_unsat_core_after_invalid_update(invalid_update, &mut self.reasoners)) + .extract_unsat_core_after_invalid_assumption(invalid_update, &mut self.reasoners)) } } } @@ -1056,9 +1056,10 @@ impl Solver { self.brancher.pre_conflict_analysis(&self.model); // contradiction, learn clause and exit let clause = match contradiction { - Contradiction::InvalidUpdate(fail) => { - self.model.state.clause_for_invalid_update(fail, &mut self.reasoners) - } + Contradiction::InvalidUpdate(fail) => self + .model + .state + .clause_for_invalid_inferrence(fail, &mut self.reasoners), Contradiction::Explanation(expl) => { self.model.state.refine_explanation(expl, &mut self.reasoners) } From c0efeaacd03cbbc03e4082b07bea7dc03fddd955 Mon Sep 17 00:00:00 2001 From: Nika Beriachvili Date: Wed, 8 Jan 2025 18:32:28 +0100 Subject: [PATCH 16/16] fix(unsat cores): change test to not extract an unsat core from a conflict resulting from propagating a decision --- solver/src/core/state/domains.rs | 39 ++------------------------------ 1 file changed, 2 insertions(+), 37 deletions(-) diff --git a/solver/src/core/state/domains.rs b/solver/src/core/state/domains.rs index 0ba28001..48ddfa78 100644 --- a/solver/src/core/state/domains.rs +++ b/solver/src/core/state/domains.rs @@ -1063,8 +1063,8 @@ mod tests { let g = Lit::geq(model.new_var(0, 1), 1); let h = Lit::geq(model.new_var(0, 1), 1); - // assumptions: a, b, d - // expected core: a, b + // assumptions: a, b, d, g + // expected core: a, b, g // constraint 0: "a => c" // constraint 1: "b & c => f" @@ -1172,25 +1172,6 @@ mod tests { propagate(&mut model).unwrap(); assert_eq!(model.bounds(e.variable()), (1, 1)); - model.save_state(); - model.decide(g).unwrap(); - assert_eq!(model.bounds(g.variable()), (1, 1)); - let err = match propagate(&mut model) { - Err(err) => err, - _ => panic!(), - }; - - let conflict = model.clause_for_invalid_inferrence(err, &mut network); - let unsat_core = model.extract_unsat_core_after_conflict(conflict, &mut network).lits; - let unsat_core_set: HashSet = unsat_core.iter().copied().collect(); - - let mut expected = HashSet::new(); - expected.insert(a); - expected.insert(b); - assert_eq!(unsat_core_set, expected); - - model.restore_last(); - model.save_state(); model.assume(g).unwrap(); assert_eq!(model.bounds(g.variable()), (1, 1)); @@ -1209,22 +1190,6 @@ mod tests { expected.insert(b); expected.insert(g); assert_eq!(unsat_core_set, expected); - - model.restore_last(); - - model.save_state(); - let err = model.assume(h).unwrap_err(); - - let unsat_core = model - .extract_unsat_core_after_invalid_assumption(err, &mut network) - .lits; - let unsat_core_set: HashSet = unsat_core.iter().copied().collect(); - - let mut expected = HashSet::new(); - expected.insert(a); - expected.insert(b); - expected.insert(h); - assert_eq!(unsat_core_set, expected); } #[test]