feat: Post equality as single predicate instead of splitting in two (#305)

Currently, whenever we post a predicate `[x == v]`, we decompose it into
`[x >= v] /\ [x <= v]`. However, this can make certain structures
unnecessarily complicated.

This PR aims to address this by posting `[x == v]` directly instead of
decomposing.

## TODO
- [x] Check for any other locations where we make this assumption
(@maartenflippo and @EmirDe, your input would be much appreciated here!)
- [x] Check the performance

## Experiments

### Overall
`main`:
```
{'ERROR': 19,
 'OPTIMAL': 120,
 'SATISFIABLE': 228,
 'UNKNOWN': 114,
 'UNSATISFIABLE': 6}
 ```
 
 `feat/post-equality-as-single-predicate`:
 ```
 {'ERROR': 19,
 'OPTIMAL': 122,
 'SATISFIABLE': 228,
 'UNKNOWN': 112,
 'UNSATISFIABLE': 6}
 ```
 
 ### MiniZinc Scoring
 ```
 {
    'main': 180.59,
    'feat/post-equality-as-single-predicate': 177.41
}
 ```
 
 ### Primal Integral
 ```
 {
    'main': 25.06,
    'feat/post-equality-as-single-predicate': 23.63,
}
 ```

Author: ImkoMarijnissen

pumpkin-crates/core/src/basic_types/predicate_id_generators/predicate_id_generator.rs

@@ -2,7 +2,6 @@ use crate::containers::HashMap;
 use crate::containers::KeyedVec;
 use crate::containers::StorageKey;
 use crate::engine::predicates::predicate::Predicate;
-use crate::pumpkin_assert_moderate;
 
 #[derive(Debug, Default, Clone)]
 pub(crate) struct PredicateIdGenerator {
@@ -11,10 +10,6 @@ pub(crate) struct PredicateIdGenerator {
 }
 
 impl PredicateIdGenerator {
-    pub(crate) fn has_id_for_predicate(&self, predicate: Predicate) -> bool {
-        self.predicate_to_id.contains_key(&predicate)
-    }
-
     /// Returns an id for the predicate. If the predicate already has an id, its id is returned.
     /// Otherwise, a new id is create and returned.
     pub(crate) fn get_id(&mut self, predicate: Predicate) -> PredicateId {
@@ -36,12 +31,6 @@ impl PredicateIdGenerator {
         self.predicate_to_id.clear();
     }
 
-    pub(crate) fn replace_predicate(&mut self, predicate: Predicate, replacement: Predicate) {
-        pumpkin_assert_moderate!(self.has_id_for_predicate(predicate));
-        let predicate_id = self.get_id(predicate);
-        self.id_to_predicate[predicate_id] = replacement
-    }
-
     pub(crate) fn num_predicate_ids(&self) -> usize {
         self.id_to_predicate.len()
     }

pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs

@@ -472,6 +472,16 @@ impl ConflictAnalysisContext<'_> {
                     reason_buffer.extend(std::iter::once(predicate_lb));
                     reason_buffer.extend(std::iter::once(predicate_ub));
                 }
+                (
+                    PredicateType::Equal,
+                    PredicateType::LowerBound | PredicateType::UpperBound | PredicateType::NotEqual,
+                ) => {
+                    // The trail predicate is equality, but the input predicate is either a
+                    // lower-bound, upper-bound, or not equals.
+                    //
+                    // TODO: could consider lifting here
+                    reason_buffer.extend(std::iter::once(trail_entry.predicate))
+                }
                 _ => unreachable!(
                     "Unreachable combination of {} and {}",
                     trail_entry.predicate, predicate

pumpkin-crates/core/src/engine/conflict_analysis/resolvers/resolution_resolver.rs

@@ -130,125 +130,7 @@ impl ConflictResolver for ResolutionResolver {
             // 1) Pop the predicate last assigned on the trail from the nogood.
             let next_predicate = self.pop_predicate_from_conflict_nogood();
 
-            // 2) Add the reason of the next_predicate to the nogood.
-
-            // 2.a) Here we treat the special case: if the next predicate is a decision, this means
-            // that we are done with analysis since the only remaining predicate in the heap is the
-            // other decision.
-            if context.assignments.is_decision_predicate(&next_predicate) {
-                // As a simple workaround, we add the currently analysed predicate to set of
-                // predicates from the lower predicate level, and stop analysis.
-                //
-                // Semantic minimisation will ensure the bound predicates get converted into an
-                // equality decision predicate.
-                while self.to_process_heap.num_nonremoved_elements() != 1 {
-                    let predicate = self.pop_predicate_from_conflict_nogood();
-                    let predicate_replacement = if context
-                        .assignments
-                        .is_decision_predicate(&predicate)
-                    {
-                        predicate
-                    } else {
-                        // Note that we decompose [x == v] into the two predicates [x >= v] and [x
-                        // <= v] and that these have distinct trail entries (where [x >= v] has a
-                        // lower trail position than [x <= v])
-                        //
-                        // However, this can lead to [x <= v] to be processed *before* [x >= v -
-                        // y], meaning that these implied predicates should be replaced with their
-                        // reason
-                        self.reason_buffer.clear();
-                        ConflictAnalysisContext::get_propagation_reason(
-                            predicate,
-                            context.assignments,
-                            CurrentNogood::new(
-                                &self.to_process_heap,
-                                &self.processed_nogood_predicates,
-                                &self.predicate_id_generator,
-                            ),
-                            context.reason_store,
-                            context.propagators,
-                            context.proof_log,
-                            context.unit_nogood_inference_codes,
-                            &mut self.reason_buffer,
-                            context.notification_engine,
-                            context.variable_names,
-                        );
-
-                        if self.reason_buffer.is_empty() {
-                            predicate
-                        } else {
-                            pumpkin_assert_simple!(predicate.is_lower_bound_predicate() || predicate.is_not_equal_predicate(), "A non-decision predicate in the nogood should be either a lower-bound or a not-equals predicate but it was {predicate} with reason {:?}", self.reason_buffer);
-                            pumpkin_assert_simple!(
-                                self.reason_buffer.len() == 1 && self.reason_buffer[0].is_lower_bound_predicate(),
-                                "The reason for the only propagated predicates left on the trail should be lower-bound predicates, but the reason for {predicate} was {:?}",
-                                self.reason_buffer,
-                            );
-
-                            self.reason_buffer[0]
-                        }
-                    };
-
-                    // We push to `predicates_lower_decision_level` since this structure will be
-                    // used for creating the final nogood
-                    self.processed_nogood_predicates.push(predicate_replacement);
-                }
-                // It could be the case that the final predicate in the nogood is implied, in
-                // this case we eagerly replace it since the conflict analysis output assumes
-                // that a single variable is propagating.
-                //
-                // For example, let's say we have made the decision [x == v] (which is
-                // decomposed into [x >= v] and [x <= v]).
-                //
-                // Now let's say we have the nogood [[x>= v - 1], [x <= v]], then we have a
-                // final element [x >= v - 1] left in the heap which is
-                // implied. This could mean that we end up with 2 predicates in
-                // the conflict nogood which goes against the 2-watcher scheme so we eagerly
-                // replace it here!
-                //
-                // If it is an initial bound then it will be removed by semantic minimisation when
-                // extracting the final nogood.
-                //
-                // TODO: This leads to a less general explanation!
-                if !context
-                    .assignments
-                    .is_decision_predicate(&self.peek_predicate_from_conflict_nogood())
-                    && !context
-                        .assignments
-                        .is_initial_bound(self.peek_predicate_from_conflict_nogood())
-                {
-                    let predicate = self.peek_predicate_from_conflict_nogood();
-
-                    self.reason_buffer.clear();
-                    ConflictAnalysisContext::get_propagation_reason(
-                        predicate,
-                        context.assignments,
-                        CurrentNogood::new(
-                            &self.to_process_heap,
-                            &self.processed_nogood_predicates,
-                            &self.predicate_id_generator,
-                        ),
-                        context.reason_store,
-                        context.propagators,
-                        context.proof_log,
-                        context.unit_nogood_inference_codes,
-                        &mut self.reason_buffer,
-                        context.notification_engine,
-                        context.variable_names,
-                    );
-                    pumpkin_assert_simple!(predicate.is_lower_bound_predicate() || predicate.is_not_equal_predicate() , "If the final predicate in the conflict nogood is not a decision predicate then it should be either a lower-bound predicate or a not-equals predicate but was {predicate}");
-                    pumpkin_assert_simple!(
-                        self.reason_buffer.len() == 1 && self.reason_buffer[0].is_lower_bound_predicate(),
-                        "The reason for the decision predicate should be a lower-bound predicate but was {}", self.reason_buffer[0]
-                    );
-                    self.replace_predicate_in_conflict_nogood(predicate, self.reason_buffer[0]);
-                }
-
-                // The final predicate in the heap will get pushed in `extract_final_nogood`
-                self.processed_nogood_predicates.push(next_predicate);
-                break;
-            }
-
-            // 2.b) Standard case, get the reason for the predicate and add it to the nogood.
+            // 2) Get the reason for the predicate and add it to the nogood.
             self.reason_buffer.clear();
             ConflictAnalysisContext::get_propagation_reason(
                 next_predicate,
@@ -428,21 +310,6 @@ impl ResolutionResolver {
         self.predicate_id_generator.get_predicate(next_predicate_id)
     }
 
-    fn peek_predicate_from_conflict_nogood(&self) -> Predicate {
-        let next_predicate_id = self.to_process_heap.peek_max().unwrap().0;
-        self.predicate_id_generator
-            .get_predicate(*next_predicate_id)
-    }
-
-    fn replace_predicate_in_conflict_nogood(
-        &mut self,
-        predicate: Predicate,
-        replacement: Predicate,
-    ) {
-        self.predicate_id_generator
-            .replace_predicate(predicate, replacement);
-    }
-
     fn extract_final_nogood(&mut self, context: &mut ConflictAnalysisContext) -> LearnedNogood {
         // The final nogood is composed of the predicates encountered from the lower decision
         // levels, plus the predicate remaining in the heap.

pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs

@@ -1094,7 +1094,7 @@ impl ConstraintSatisfactionSolver {
                 empty_domain_reason.push(predicate!(conflict_domain == entry.old_lower_bound));
             }
             PredicateType::Equal => {
-                // The last trail entry was an equality propagation; we split into two cases.
+                // 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
                     //
@@ -1103,17 +1103,19 @@ impl ConstraintSatisfactionSolver {
                     empty_domain_reason.push(predicate!(
                         conflict_domain >= entry.predicate.get_right_hand_side() + 1
                     ));
-                } else {
+                } 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
-                    pumpkin_assert_simple!(
-                        entry.predicate.get_right_hand_side() > entry.old_upper_bound
-                    );
                     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()
+                    ))
                 }
             }
         }

pumpkin-crates/core/src/engine/cp/assignments.rs

@@ -518,14 +518,41 @@ impl Assignments {
         reason: Option<AssignmentReason>,
     ) -> Result<bool, EmptyDomain> {
         let mut update_took_place = false;
-        // only tighten the lower bound if needed
-        if self.get_lower_bound(domain_id) < assigned_value {
-            update_took_place |= self.tighten_lower_bound(domain_id, assigned_value, reason)?;
+
+        let predicate = predicate!(domain_id == assigned_value);
+
+        let old_lower_bound = self.get_lower_bound(domain_id);
+        let old_upper_bound = self.get_upper_bound(domain_id);
+
+        if old_lower_bound == assigned_value && old_upper_bound == assigned_value {
+            return self.domains[domain_id].verify_consistency();
         }
 
-        // only tighten the upper bound if needed
-        if self.get_upper_bound(domain_id) > assigned_value {
-            update_took_place |= self.tighten_upper_bound(domain_id, assigned_value, reason)?;
+        // important to record trail position _before_ pushing to the trail
+        let trail_position = self.trail.len();
+
+        self.trail.push(ConstraintProgrammingTrailEntry {
+            predicate,
+            old_lower_bound,
+            old_upper_bound,
+            reason,
+        });
+
+        let decision_level = self.get_decision_level();
+        let domain = &mut self.domains[domain_id];
+
+        if old_lower_bound < assigned_value {
+            update_took_place |=
+                domain.set_lower_bound(assigned_value, decision_level, trail_position);
+            self.bounds[domain_id].0 = domain.lower_bound();
+            self.pruned_values += domain.lower_bound().abs_diff(old_lower_bound) as u64;
+        }
+
+        if old_upper_bound > assigned_value {
+            update_took_place |=
+                domain.set_upper_bound(assigned_value, decision_level, trail_position);
+            self.bounds[domain_id].1 = domain.upper_bound();
+            self.pruned_values += domain.upper_bound().abs_diff(old_upper_bound) as u64;
         }
 
         let _ = self.domains[domain_id].verify_consistency()?;
@@ -702,43 +729,50 @@ impl Assignments {
             self.trail.get_decision_level(),
         );
 
-        self.trail.synchronise(new_decision_level).enumerate().for_each(|(index, entry)| {
-            pumpkin_assert_moderate!(
-                !entry.predicate.is_equality_predicate(),
-                "For now we do not expect equality predicates on the trail, since currently equality predicates are split into lower and upper bound predicates."
-            );
-
-            // Calculate how many values are re-introduced into the domain.
-            let domain_id = entry.predicate.get_domain();
-            let lower_bound_before = self.domains[domain_id].lower_bound();
-            let upper_bound_before = self.domains[domain_id].upper_bound();
-
-            let trail_index = num_trail_entries_before_synchronisation - index - 1;
-
-            let add_on_upper_bound = entry.old_upper_bound.abs_diff(upper_bound_before) as u64;
-            let add_on_lower_bound = lower_bound_before.abs_diff(entry.old_lower_bound) as u64;
-            self.pruned_values -= add_on_upper_bound + add_on_lower_bound;
-
-            if entry.predicate.is_not_equal_predicate() && add_on_lower_bound + add_on_upper_bound == 0 {
-                self.pruned_values -= 1;
-            }
-
-            let fixed_before = self.domains[domain_id].lower_bound() == self.domains[domain_id].upper_bound();
-            self.domains[domain_id].undo_trail_entry(&entry);
-
-            let new_lower_bound = self.domains[domain_id].lower_bound();
-            let new_upper_bound = self.domains[domain_id].upper_bound();
-            self.bounds[domain_id] = (new_lower_bound, new_upper_bound);
-
-            notification_engine.undo_trail_entry(fixed_before, lower_bound_before, upper_bound_before, new_lower_bound, new_upper_bound, trail_index, entry.predicate);
-
-            if new_lower_bound != new_upper_bound {
-
-            // Variable used to be fixed but is not after backtracking
-            unfixed_variables.push((domain_id, lower_bound_before));
-            }
+        self.trail
+            .synchronise(new_decision_level)
+            .enumerate()
+            .for_each(|(index, entry)| {
+                // Calculate how many values are re-introduced into the domain.
+                let domain_id = entry.predicate.get_domain();
+                let lower_bound_before = self.domains[domain_id].lower_bound();
+                let upper_bound_before = self.domains[domain_id].upper_bound();
+
+                let trail_index = num_trail_entries_before_synchronisation - index - 1;
+
+                let add_on_upper_bound = entry.old_upper_bound.abs_diff(upper_bound_before) as u64;
+                let add_on_lower_bound = entry.old_lower_bound.abs_diff(lower_bound_before) as u64;
+                self.pruned_values -= add_on_upper_bound + add_on_lower_bound;
+
+                if entry.predicate.is_not_equal_predicate()
+                    && add_on_lower_bound + add_on_upper_bound == 0
+                {
+                    self.pruned_values -= 1;
+                }
 
-        });
+                let fixed_before =
+                    self.domains[domain_id].lower_bound() == self.domains[domain_id].upper_bound();
+                self.domains[domain_id].undo_trail_entry(&entry);
+
+                let new_lower_bound = self.domains[domain_id].lower_bound();
+                let new_upper_bound = self.domains[domain_id].upper_bound();
+                self.bounds[domain_id] = (new_lower_bound, new_upper_bound);
+
+                notification_engine.undo_trail_entry(
+                    fixed_before,
+                    lower_bound_before,
+                    upper_bound_before,
+                    new_lower_bound,
+                    new_upper_bound,
+                    trail_index,
+                    entry.predicate,
+                );
+
+                if new_lower_bound != new_upper_bound {
+                    // Variable used to be fixed but is not after backtracking
+                    unfixed_variables.push((domain_id, lower_bound_before));
+                }
+            });
 
         // Drain does not remove the events from the internal data structure. Elements are removed
         // lazily, as the iterator gets executed. For this reason we go through the entire iterator.
@@ -1187,17 +1221,24 @@ impl IntegerDomain {
                 }
             }
             PredicateType::Equal => {
-                // I think we never push equality predicates to the trail
-                // in the current version. Equality gets substituted
-                // by a lower and upper bound predicate.
-                unreachable!()
+                let lower_bound_update = self.lower_bound_updates.last().unwrap();
+                let upper_bound_update = self.upper_bound_updates.last().unwrap();
+
+                if lower_bound_update.trail_position > upper_bound_update.trail_position {
+                    let _ = self.lower_bound_updates.pop();
+                } else if upper_bound_update.trail_position > lower_bound_update.trail_position {
+                    let _ = self.upper_bound_updates.pop();
+                } else {
+                    let _ = self.lower_bound_updates.pop();
+                    let _ = self.upper_bound_updates.pop();
+                }
             }
         };
 
         // these asserts will be removed, for now it is a sanity check
         // later we may remove the old bound from the trail entry since it is not needed
-        pumpkin_assert_simple!(self.lower_bound() == entry.old_lower_bound);
-        pumpkin_assert_simple!(self.upper_bound() == entry.old_upper_bound);
+        pumpkin_assert_eq_simple!(self.lower_bound(), entry.old_lower_bound);
+        pumpkin_assert_eq_simple!(self.upper_bound(), entry.old_upper_bound);
 
         pumpkin_assert_moderate!(self.debug_bounds_check());
     }