diff --git a/pumpkin-crates/core/src/basic_types/mod.rs b/pumpkin-crates/core/src/basic_types/mod.rs index eb2114b3e..c670a7ac7 100644 --- a/pumpkin-crates/core/src/basic_types/mod.rs +++ b/pumpkin-crates/core/src/basic_types/mod.rs @@ -23,5 +23,5 @@ pub use random::*; pub use solution::ProblemSolution; pub use solution::Solution; pub use solution::SolutionReference; -pub(crate) use stored_conflict_info::StoredConflictInfo; +pub(crate) use stored_conflict_info::*; pub(crate) use trail::Trail; diff --git a/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs b/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs index e9176255a..1537ad7fc 100644 --- a/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs +++ b/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs @@ -1,10 +1,13 @@ -use super::PropositionalConjunction; use super::propagation_status_cp::PropagatorConflict; use crate::ConstraintOperationError; #[cfg(doc)] use crate::engine::ConstraintSatisfactionSolver; #[cfg(doc)] use crate::engine::propagation::Propagator; +use crate::engine::reason::ReasonRef; +use crate::predicates::Predicate; +use crate::proof::InferenceCode; +use crate::variables::DomainId; /// A conflict info which can be stored in the solver. /// Two (related) conflicts can happen: @@ -13,8 +16,28 @@ use crate::engine::propagation::Propagator; #[derive(Debug, PartialEq, Eq, Clone)] pub(crate) enum StoredConflictInfo { Propagator(PropagatorConflict), - EmptyDomain { - conflict_nogood: PropositionalConjunction, - }, + EmptyDomain(EmptyDomainConflict), + /// The conflict is due to inconsistent assumptions. + /// + /// The provided predicate and its negation are both assumptions. + InconsistentAssumptions(Predicate), RootLevelConflict(ConstraintOperationError), } + +/// A conflict because a domain became empty. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub(crate) struct EmptyDomainConflict { + /// The predicate that caused a domain to become empty. + pub(crate) trigger_predicate: Predicate, + /// The reason for [`EmptyDomainConflict::trigger_predicate`] to be true. + pub(crate) trigger_reason: ReasonRef, + /// The [`InferenceCode`] that accompanies [`EmptyDomainConflict::trigger_reason`]. + pub(crate) trigger_inference_code: InferenceCode, +} + +impl EmptyDomainConflict { + /// The domain that became empty. + pub(crate) fn domain(&self) -> DomainId { + self.trigger_predicate.get_domain() + } +} diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs b/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs index 4a8e0ff19..ef4af5328 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs @@ -2,6 +2,7 @@ use std::fmt::Debug; use super::minimisers::SemanticMinimiser; use crate::Random; +use crate::basic_types::EmptyDomainConflict; use crate::basic_types::StoredConflictInfo; use crate::branching::Brancher; use crate::containers::HashMap; @@ -23,11 +24,13 @@ use crate::engine::reason::ReasonRef; use crate::engine::reason::ReasonStore; use crate::engine::solver_statistics::SolverStatistics; use crate::predicate; +use crate::predicates::PropositionalConjunction; use crate::proof::InferenceCode; use crate::proof::ProofLog; use crate::proof::RootExplanationContext; use crate::proof::explain_root_assignment; use crate::propagators::nogoods::NogoodPropagator; +use crate::pumpkin_assert_eq_simple; use crate::pumpkin_assert_simple; /// Used during conflict analysis to provide the necessary information. @@ -120,19 +123,22 @@ impl ConflictAnalysisContext<'_> { conflict.conjunction } - StoredConflictInfo::EmptyDomain { conflict_nogood } => conflict_nogood, + StoredConflictInfo::EmptyDomain(conflict) => self.compute_conflict_nogood(conflict), StoredConflictInfo::RootLevelConflict(_) => { unreachable!("Should never attempt to learn a nogood from a root level conflict") } + StoredConflictInfo::InconsistentAssumptions(predicate) => { + vec![predicate, !predicate].into() + } }; for &predicate in conflict_nogood.iter() { - if self + let predicate_dl = self .assignments .get_decision_level_for_predicate(&predicate) - .unwrap() - == 0 - { + .expect("all predicates in the conflict nogood should be assigned to true"); + + if predicate_dl == 0 { explain_root_assignment( &mut RootExplanationContext { propagators: self.propagators, @@ -495,4 +501,93 @@ impl ConflictAnalysisContext<'_> { }; } } + + fn compute_conflict_nogood( + &mut self, + conflict: EmptyDomainConflict, + ) -> PropositionalConjunction { + let conflict_domain = conflict.domain(); + + // Look up the reason for the bound that changed. + // The reason for changing the bound cannot be a decision, so we can safely unwrap. + let mut empty_domain_reason: Vec = vec![]; + let _ = self.reason_store.get_or_compute( + conflict.trigger_reason, + ExplanationContext::without_working_nogood( + self.assignments, + self.assignments.num_trail_entries() - 1, + self.notification_engine, + ), + self.propagators, + &mut empty_domain_reason, + ); + + // We also need to log this last propagation to the proof log as an inference. + let _ = self.proof_log.log_inference( + conflict.trigger_inference_code, + empty_domain_reason.iter().copied(), + Some(conflict.trigger_predicate), + self.variable_names, + ); + + let old_lower_bound = self.assignments.get_lower_bound(conflict_domain); + let old_upper_bound = self.assignments.get_upper_bound(conflict_domain); + + match conflict.trigger_predicate.get_predicate_type() { + PredicateType::LowerBound => { + // The last trail entry was a lower-bound propagation meaning that the empty domain + // was caused by the upper-bound + // + // We lift so that it is the most general upper-bound possible while still causing + // the empty domain + empty_domain_reason.push(predicate!( + conflict_domain <= conflict.trigger_predicate.get_right_hand_side() - 1 + )); + } + PredicateType::UpperBound => { + // The last trail entry was an upper-bound propagation meaning that the empty domain + // was caused by the lower-bound + // + // We lift so that it is the most general lower-bound possible while still causing + // the empty domain + empty_domain_reason.push(predicate!( + conflict_domain >= conflict.trigger_predicate.get_right_hand_side() + 1 + )); + } + PredicateType::NotEqual => { + // The last trail entry was a not equals propagation meaning that the empty domain + // was due to the domain being assigned to the removed value + pumpkin_assert_eq_simple!(old_upper_bound, old_lower_bound); + + empty_domain_reason.push(predicate!(conflict_domain == old_lower_bound)); + } + PredicateType::Equal => { + // The last trail entry was an equality propagation; we split into three cases. + if conflict.trigger_predicate.get_right_hand_side() < old_lower_bound { + // 1) The assigned value was lower than the lower-bound + // + // We lift so that it is the most general lower-bound possible while still + // causing the empty domain + empty_domain_reason.push(predicate!( + conflict_domain >= conflict.trigger_predicate.get_right_hand_side() + 1 + )); + } else if conflict.trigger_predicate.get_right_hand_side() > old_upper_bound { + // 2) The assigned value was larger than the upper-bound + // + // We lift so that it is the most general upper-bound possible while still + // causing the empty domain + empty_domain_reason.push(predicate!( + conflict_domain <= conflict.trigger_predicate.get_right_hand_side() - 1 + )); + } else { + // 3) The assigned value was equal to a hole in the domain + empty_domain_reason.push(predicate!( + conflict_domain != conflict.trigger_predicate.get_right_hand_side() + )) + } + } + } + + empty_domain_reason.into() + } } diff --git a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs index 9ee67c8ff..93ad459b9 100644 --- a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs +++ b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs @@ -27,9 +27,9 @@ use super::variables::Literal; use crate::Solver; use crate::basic_types::CSPSolverExecutionFlag; use crate::basic_types::ConstraintOperationError; +use crate::basic_types::EmptyDomainConflict; use crate::basic_types::Inconsistency; use crate::basic_types::PredicateId; -use crate::basic_types::PropositionalConjunction; use crate::basic_types::Random; use crate::basic_types::SolutionReference; use crate::basic_types::StoredConflictInfo; @@ -52,8 +52,6 @@ use crate::engine::propagation::constructor::PropagatorConstructorContext; use crate::engine::propagation::store::PropagatorHandle; use crate::engine::reason::ReasonStore; use crate::engine::variables::DomainId; -use crate::predicate; -use crate::predicates::PredicateType; use crate::proof::ConstraintTag; use crate::proof::FinalizingContext; use crate::proof::InferenceCode; @@ -234,25 +232,41 @@ impl ConstraintSatisfactionSolver { } fn complete_proof(&mut self) { - let conflict = match self.state.get_conflict_info() { - StoredConflictInfo::Propagator(conflict) => { - let _ = self.internal_parameters.proof_log.log_inference( - conflict.inference_code, - conflict.conjunction.iter().copied(), - None, - &self.variable_names, - ); + struct DummyBrancher; - conflict.conjunction.clone() + impl Brancher for DummyBrancher { + fn next_decision(&mut self, _: &mut SelectionContext) -> Option { + unreachable!() } - StoredConflictInfo::EmptyDomain { conflict_nogood } => conflict_nogood.clone(), - StoredConflictInfo::RootLevelConflict(_) => { - unreachable!("There should always be a specified conflicting constraint.") + + fn subscribe_to_events(&self) -> Vec { + unreachable!() } + } + + let mut conflict_analysis_context = ConflictAnalysisContext { + assignments: &mut self.assignments, + counters: &mut self.solver_statistics, + solver_state: &mut self.state, + reason_store: &mut self.reason_store, + brancher: &mut DummyBrancher, + semantic_minimiser: &mut self.semantic_minimiser, + propagators: &mut self.propagators, + notification_engine: &mut self.notification_engine, + propagator_queue: &mut self.propagator_queue, + should_minimise: self.internal_parameters.learning_clause_minimisation, + proof_log: &mut self.internal_parameters.proof_log, + unit_nogood_inference_codes: &mut self.unit_nogood_inference_codes, + trailed_values: &mut self.trailed_values, + variable_names: &self.variable_names, + rng: &mut self.internal_parameters.random_generator, + restart_strategy: &mut self.restart_strategy, }; + let conflict = conflict_analysis_context.get_conflict_nogood(); + let context = FinalizingContext { - conflict, + conflict: conflict.into(), propagators: &mut self.propagators, proof_log: &mut self.internal_parameters.proof_log, unit_nogood_inference_codes: &self.unit_nogood_inference_codes, @@ -925,105 +939,6 @@ impl ConstraintSatisfactionSolver { notification_engine.synchronise(backtrack_level, assignments, trailed_values); } - pub(crate) fn compute_reason_for_empty_domain(&mut self) -> PropositionalConjunction { - // The empty domain happened after posting the last predicate on the trail. - // The reason for this empty domain is computed as the reason for the bounds before the last - // trail predicate was posted, plus the reason for the last trail predicate. - - // The last predicate on the trail reveals the domain id that has resulted - // in an empty domain. - let entry = self.assignments.get_last_entry_on_trail(); - let (entry_reason, entry_inference_code) = entry - .reason - .expect("Cannot cause an empty domain using a decision."); - let conflict_domain = entry.predicate.get_domain(); - assert!( - entry.old_lower_bound != self.assignments.get_lower_bound(conflict_domain) - || entry.old_upper_bound != self.assignments.get_upper_bound(conflict_domain), - "One of the two bounds had to change." - ); - - // Look up the reason for the bound that changed. - // The reason for changing the bound cannot be a decision, so we can safely unwrap. - let mut empty_domain_reason: Vec = vec![]; - let _ = self.reason_store.get_or_compute( - entry_reason, - ExplanationContext::without_working_nogood( - &self.assignments, - self.assignments.num_trail_entries() - 1, - &mut self.notification_engine, - ), - &mut self.propagators, - &mut empty_domain_reason, - ); - - // We also need to log this last propagation to the proof log as an inference. - let _ = self.internal_parameters.proof_log.log_inference( - entry_inference_code, - empty_domain_reason.iter().copied(), - Some(entry.predicate), - &self.variable_names, - ); - - // Now we get the explanation for the bound which was conflicting with the last trail entry - match entry.predicate.get_predicate_type() { - PredicateType::LowerBound => { - // The last trail entry was a lower-bound propagation meaning that the empty domain - // was caused by the upper-bound - // - // We lift so that it is the most general upper-bound possible while still causing - // the empty domain - empty_domain_reason.push(predicate!( - conflict_domain <= entry.predicate.get_right_hand_side() - 1 - )); - } - PredicateType::UpperBound => { - // The last trail entry was an upper-bound propagation meaning that the empty domain - // was caused by the lower-bound - // - // We lift so that it is the most general lower-bound possible while still causing - // the empty domain - empty_domain_reason.push(predicate!( - conflict_domain >= entry.predicate.get_right_hand_side() + 1 - )); - } - PredicateType::NotEqual => { - // The last trail entry was a not equals propagation meaning that the empty domain - // was due to the domain being assigned to the removed value - pumpkin_assert_eq_simple!(entry.old_upper_bound, entry.old_lower_bound); - - empty_domain_reason.push(predicate!(conflict_domain == entry.old_lower_bound)); - } - PredicateType::Equal => { - // The last trail entry was an equality propagation; we split into three cases. - if entry.predicate.get_right_hand_side() < entry.old_lower_bound { - // 1) The assigned value was lower than the lower-bound - // - // We lift so that it is the most general lower-bound possible while still - // causing the empty domain - empty_domain_reason.push(predicate!( - conflict_domain >= entry.predicate.get_right_hand_side() + 1 - )); - } else if entry.predicate.get_right_hand_side() > entry.old_upper_bound { - // 2) The assigned value was larger than the upper-bound - // - // We lift so that it is the most general upper-bound possible while still - // causing the empty domain - empty_domain_reason.push(predicate!( - conflict_domain <= entry.predicate.get_right_hand_side() - 1 - )); - } else { - // 3) The assigned value was equal to a hole in the domain - empty_domain_reason.push(predicate!( - conflict_domain != entry.predicate.get_right_hand_side() - )) - } - } - } - - empty_domain_reason.into() - } - /// Main propagation loop. pub(crate) fn propagate(&mut self) { // Record the number of predicates on the trail for statistics purposes. @@ -1355,17 +1270,18 @@ impl ConstraintSatisfactionSolver { return; } - let empty_domain_reason = self.compute_reason_for_empty_domain(); - // TODO: As a temporary solution, we remove the last trail element. // This way we guarantee that the assignment is consistent, which is needed // for the conflict analysis data structures. The proper alternative would // be to forbid the assignments from getting into an inconsistent state. - self.assignments.remove_last_trail_element(); + let (trigger_predicate, trigger_reason, trigger_inference_code) = + self.assignments.remove_last_trail_element(); - let stored_conflict_info = StoredConflictInfo::EmptyDomain { - conflict_nogood: empty_domain_reason, - }; + let stored_conflict_info = StoredConflictInfo::EmptyDomain(EmptyDomainConflict { + trigger_predicate, + trigger_reason, + trigger_inference_code, + }); self.state.declare_conflict(stored_conflict_info); } @@ -1525,9 +1441,7 @@ impl CSPSolverState { CSPSolverStateInternal::Conflict { conflict_info } => conflict_info.clone(), CSPSolverStateInternal::InfeasibleUnderAssumptions { violated_assumption, - } => StoredConflictInfo::EmptyDomain { - conflict_nogood: vec![*violated_assumption, !(*violated_assumption)].into(), - }, + } => StoredConflictInfo::InconsistentAssumptions(*violated_assumption), _ => { panic!("Cannot extract conflict clause if solver is not in a conflict."); } diff --git a/pumpkin-crates/core/src/engine/cp/assignments.rs b/pumpkin-crates/core/src/engine/cp/assignments.rs index a8cf8975c..1aae1fde9 100644 --- a/pumpkin-crates/core/src/engine/cp/assignments.rs +++ b/pumpkin-crates/core/src/engine/cp/assignments.rs @@ -112,10 +112,6 @@ impl Assignments { self.trail[index] } - pub(crate) fn get_last_entry_on_trail(&self) -> ConstraintProgrammingTrailEntry { - *self.trail.last().unwrap() - } - // registers the domain of a new integer variable // note that this is an internal method that does _not_ allocate additional information // necessary for the solver apart from the domain when creating a new integer variable, use @@ -782,11 +778,15 @@ impl Assignments { } /// todo: This is a temporary hack, not to be used in general. - pub(crate) fn remove_last_trail_element(&mut self) { + pub(crate) fn remove_last_trail_element(&mut self) -> (Predicate, ReasonRef, InferenceCode) { let entry = self.trail.pop().unwrap(); let domain_id = entry.predicate.get_domain(); self.domains[domain_id].undo_trail_entry(&entry); self.update_bounds_snapshot(domain_id); + + let (reason, inference_code) = entry.reason.unwrap(); + + (entry.predicate, reason, inference_code) } /// Get the number of values pruned from all the domains.