From c697ab07f7deee82f7442929d2cd10af90c6c4bc Mon Sep 17 00:00:00 2001
From: Jacob Finkelman <jfinkelm@amazon.com>
Date: Wed, 20 Dec 2023 17:07:43 +0000
Subject: [PATCH 1/2] Invalidate less contradicted_incompatibilities

---
 src/internal/core.rs             | 21 ++++++++++++++-------
 src/internal/partial_solution.rs |  4 ++++
 2 files changed, 18 insertions(+), 7 deletions(-)

diff --git a/src/internal/core.rs b/src/internal/core.rs
index c53f6a35..af5e0203 100644
--- a/src/internal/core.rs
+++ b/src/internal/core.rs
@@ -29,7 +29,7 @@ pub struct State<P: Package, VS: VersionSet, Priority: Ord + Clone> {
 
     /// Store the ids of incompatibilities that are already contradicted
     /// and will stay that way until the next conflict and backtrack is operated.
-    contradicted_incompatibilities: rustc_hash::FxHashSet<IncompId<P, VS>>,
+    contradicted_incompatibilities: Map<IncompId<P, VS>, DecisionLevel>,
 
     /// All incompatibilities expressing dependencies,
     /// with common dependents merged.
@@ -62,7 +62,7 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> State<P, VS, Priority> {
             root_package,
             root_version,
             incompatibilities,
-            contradicted_incompatibilities: rustc_hash::FxHashSet::default(),
+            contradicted_incompatibilities: Map::default(),
             partial_solution: PartialSolution::empty(),
             incompatibility_store,
             unit_propagation_buffer: SmallVec::Empty,
@@ -111,7 +111,10 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> State<P, VS, Priority> {
             let mut conflict_id = None;
             // We only care about incompatibilities if it contains the current package.
             for &incompat_id in self.incompatibilities[&current_package].iter().rev() {
-                if self.contradicted_incompatibilities.contains(&incompat_id) {
+                if self
+                    .contradicted_incompatibilities
+                    .contains_key(&incompat_id)
+                {
                     continue;
                 }
                 let current_incompat = &self.incompatibility_store[incompat_id];
@@ -135,10 +138,12 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> State<P, VS, Priority> {
                             &self.incompatibility_store,
                         );
                         // With the partial solution updated, the incompatibility is now contradicted.
-                        self.contradicted_incompatibilities.insert(incompat_id);
+                        self.contradicted_incompatibilities
+                            .insert(incompat_id, self.partial_solution.current_decision_level());
                     }
                     Relation::Contradicted(_) => {
-                        self.contradicted_incompatibilities.insert(incompat_id);
+                        self.contradicted_incompatibilities
+                            .insert(incompat_id, self.partial_solution.current_decision_level());
                     }
                     _ => {}
                 }
@@ -155,7 +160,8 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> State<P, VS, Priority> {
                 );
                 // After conflict resolution and the partial solution update,
                 // the root cause incompatibility is now contradicted.
-                self.contradicted_incompatibilities.insert(root_cause);
+                self.contradicted_incompatibilities
+                    .insert(root_cause, self.partial_solution.current_decision_level());
             }
         }
         // If there are no more changed packages, unit propagation is done.
@@ -220,7 +226,8 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> State<P, VS, Priority> {
     ) {
         self.partial_solution
             .backtrack(decision_level, &self.incompatibility_store);
-        self.contradicted_incompatibilities.clear();
+        self.contradicted_incompatibilities
+            .retain(|_, dl| *dl <= decision_level);
         if incompat_changed {
             self.merge_incompatibility(incompat);
         }
diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs
index 057dea13..a40f4c97 100644
--- a/src/internal/partial_solution.rs
+++ b/src/internal/partial_solution.rs
@@ -493,6 +493,10 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
             .unwrap();
         decision_level.max(DecisionLevel(1))
     }
+
+    pub fn current_decision_level(&self) -> DecisionLevel {
+        self.current_decision_level
+    }
 }
 
 impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {

From 7c98334a92499ad89cdc3ad40405b3ec23235533 Mon Sep 17 00:00:00 2001
From: Jacob Finkelman <jfinkelm@amazon.com>
Date: Wed, 20 Dec 2023 17:12:14 +0000
Subject: [PATCH 2/2] update comments

---
 src/internal/core.rs | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/internal/core.rs b/src/internal/core.rs
index af5e0203..58831469 100644
--- a/src/internal/core.rs
+++ b/src/internal/core.rs
@@ -27,8 +27,9 @@ pub struct State<P: Package, VS: VersionSet, Priority: Ord + Clone> {
 
     incompatibilities: Map<P, Vec<IncompId<P, VS>>>,
 
-    /// Store the ids of incompatibilities that are already contradicted
-    /// and will stay that way until the next conflict and backtrack is operated.
+    /// Store the ids of incompatibilities that are already contradicted.
+    /// For each one keep track of the decision level when it was found to be contradicted.
+    /// These will stay contradicted until we have backtracked beyond its associated decision level.
     contradicted_incompatibilities: Map<IncompId<P, VS>, DecisionLevel>,
 
     /// All incompatibilities expressing dependencies,
@@ -226,6 +227,7 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> State<P, VS, Priority> {
     ) {
         self.partial_solution
             .backtrack(decision_level, &self.incompatibility_store);
+        // Remove contradicted incompatibilities that depend on decisions we just backtracked away.
         self.contradicted_incompatibilities
             .retain(|_, dl| *dl <= decision_level);
         if incompat_changed {