From 7b2537880bb21cba6bc80a12b7a7e3a009552be1 Mon Sep 17 00:00:00 2001
From: Imko Marijnissen <imko.marijnissen@gmail.com>
Date: Tue, 10 Mar 2026 08:19:21 +0100
Subject: [PATCH 01/10] feat: initial setup for circuit

---
 minizinc/lib/fzn_circuit.mzn                  |  3 +
 .../constraints/src/constraints/circuit.rs    | 51 +++++++++++
 .../constraints/src/constraints/mod.rs        |  2 +
 .../src/propagators/circuit/checker.rs        | 23 +++++
 .../src/propagators/circuit/mod.rs            |  5 +
 .../src/propagators/circuit/propagator.rs     | 91 +++++++++++++++++++
 .../propagators/src/propagators/mod.rs        |  1 +
 .../flatzinc/compiler/post_constraints.rs     | 15 +++
 8 files changed, 191 insertions(+)
 create mode 100644 minizinc/lib/fzn_circuit.mzn
 create mode 100644 pumpkin-crates/constraints/src/constraints/circuit.rs
 create mode 100644 pumpkin-crates/propagators/src/propagators/circuit/checker.rs
 create mode 100644 pumpkin-crates/propagators/src/propagators/circuit/mod.rs
 create mode 100644 pumpkin-crates/propagators/src/propagators/circuit/propagator.rs

diff --git a/minizinc/lib/fzn_circuit.mzn b/minizinc/lib/fzn_circuit.mzn
new file mode 100644
index 000000000..c32e74bed
--- /dev/null
+++ b/minizinc/lib/fzn_circuit.mzn
@@ -0,0 +1,3 @@
+predicate fzn_circuit(array[int] of var int: x) = pumpkin_circuit(x);
+
+predicate pumpkin_circuit(array[int] of var int: x);
diff --git a/pumpkin-crates/constraints/src/constraints/circuit.rs b/pumpkin-crates/constraints/src/constraints/circuit.rs
new file mode 100644
index 000000000..3b13d022b
--- /dev/null
+++ b/pumpkin-crates/constraints/src/constraints/circuit.rs
@@ -0,0 +1,51 @@
+use pumpkin_core::constraints::Constraint;
+use pumpkin_core::proof::ConstraintTag;
+use pumpkin_core::variables::IntegerVariable;
+use pumpkin_propagators::circuit::CircuitConstructor;
+
+use crate::all_different;
+
+pub fn circuit<Var: IntegerVariable + 'static>(
+    variables: impl Into<Box<[Var]>>,
+    constraint_tag: ConstraintTag,
+) -> impl Constraint {
+    Circuit {
+        successors: variables.into(),
+        constraint_tag,
+    }
+}
+
+struct Circuit<Var> {
+    successors: Box<[Var]>,
+    constraint_tag: ConstraintTag,
+}
+
+impl<Var: IntegerVariable + 'static> Constraint for Circuit<Var> {
+    fn post(
+        self,
+        solver: &mut pumpkin_core::Solver,
+    ) -> Result<(), pumpkin_core::ConstraintOperationError> {
+        all_different(self.successors.clone(), self.constraint_tag).post(solver)?;
+
+        CircuitConstructor {
+            successors: self.successors,
+            constraint_tag: self.constraint_tag,
+        }
+        .post(solver)
+    }
+
+    fn implied_by(
+        self,
+        solver: &mut pumpkin_core::Solver,
+        reification_literal: pumpkin_core::variables::Literal,
+    ) -> Result<(), pumpkin_core::ConstraintOperationError> {
+        all_different(self.successors.clone(), self.constraint_tag)
+            .implied_by(solver, reification_literal)?;
+
+        CircuitConstructor {
+            successors: self.successors,
+            constraint_tag: self.constraint_tag,
+        }
+        .implied_by(solver, reification_literal)
+    }
+}
diff --git a/pumpkin-crates/constraints/src/constraints/mod.rs b/pumpkin-crates/constraints/src/constraints/mod.rs
index 675f9ca6d..6a8754c58 100644
--- a/pumpkin-crates/constraints/src/constraints/mod.rs
+++ b/pumpkin-crates/constraints/src/constraints/mod.rs
@@ -30,6 +30,7 @@
 mod all_different;
 mod arithmetic;
 mod boolean;
+mod circuit;
 mod clause;
 mod cumulative;
 mod disjunctive_strict;
@@ -39,6 +40,7 @@ mod table;
 pub use all_different::*;
 pub use arithmetic::*;
 pub use boolean::*;
+pub use circuit::*;
 pub use clause::*;
 pub use cumulative::*;
 pub use disjunctive_strict::*;
diff --git a/pumpkin-crates/propagators/src/propagators/circuit/checker.rs b/pumpkin-crates/propagators/src/propagators/circuit/checker.rs
new file mode 100644
index 000000000..450e79234
--- /dev/null
+++ b/pumpkin-crates/propagators/src/propagators/circuit/checker.rs
@@ -0,0 +1,23 @@
+use pumpkin_checking::AtomicConstraint;
+use pumpkin_checking::CheckerVariable;
+use pumpkin_checking::InferenceChecker;
+
+#[derive(Debug, Clone)]
+pub struct CircuitChecker<Var> {
+    pub successors: Box<[Var]>,
+}
+
+impl<Var, Atomic> InferenceChecker<Atomic> for CircuitChecker<Var>
+where
+    Var: CheckerVariable<Atomic>,
+    Atomic: AtomicConstraint,
+{
+    fn check(
+        &self,
+        state: pumpkin_checking::VariableState<Atomic>,
+        premises: &[Atomic],
+        consequent: Option<&Atomic>,
+    ) -> bool {
+        todo!()
+    }
+}
diff --git a/pumpkin-crates/propagators/src/propagators/circuit/mod.rs b/pumpkin-crates/propagators/src/propagators/circuit/mod.rs
new file mode 100644
index 000000000..0552fb72a
--- /dev/null
+++ b/pumpkin-crates/propagators/src/propagators/circuit/mod.rs
@@ -0,0 +1,5 @@
+mod checker;
+mod propagator;
+
+pub use checker::*;
+pub use propagator::*;
diff --git a/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs b/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
new file mode 100644
index 000000000..5ca2ba9a4
--- /dev/null
+++ b/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
@@ -0,0 +1,91 @@
+use pumpkin_core::declare_inference_label;
+use pumpkin_core::proof::ConstraintTag;
+use pumpkin_core::proof::InferenceCode;
+use pumpkin_core::propagation::DomainEvents;
+use pumpkin_core::propagation::Domains;
+use pumpkin_core::propagation::InferenceCheckers;
+use pumpkin_core::propagation::LocalId;
+use pumpkin_core::propagation::Priority;
+use pumpkin_core::propagation::PropagationContext;
+use pumpkin_core::propagation::Propagator;
+use pumpkin_core::propagation::PropagatorConstructor;
+use pumpkin_core::results::PropagationStatusCP;
+use pumpkin_core::variables::IntegerVariable;
+
+use crate::circuit::CircuitChecker;
+
+#[derive(Debug)]
+pub struct CircuitConstructor<Var> {
+    pub successors: Box<[Var]>,
+    pub constraint_tag: ConstraintTag,
+}
+
+impl<Var: IntegerVariable + 'static> PropagatorConstructor for CircuitConstructor<Var> {
+    type PropagatorImpl = CircuitPropagator<Var>;
+
+    fn create(
+        self,
+        mut context: pumpkin_core::propagation::PropagatorConstructorContext,
+    ) -> Self::PropagatorImpl {
+        self.successors
+            .iter()
+            .enumerate()
+            .for_each(|(index, successor)| {
+                context.register(
+                    successor.clone(),
+                    DomainEvents::ASSIGN,
+                    LocalId::from(index as u32),
+                )
+            });
+
+        CircuitPropagator {
+            successors: self.successors,
+            inference_code: InferenceCode::new(self.constraint_tag, CircuitPrevent),
+        }
+    }
+
+    fn add_inference_checkers(&self, mut checkers: InferenceCheckers<'_>) {
+        checkers.add_inference_checker(
+            InferenceCode::new(self.constraint_tag, CircuitPrevent),
+            Box::new(CircuitChecker {
+                successors: self.successors.clone(),
+            }),
+        );
+    }
+}
+
+declare_inference_label!(CircuitPrevent);
+
+#[derive(Debug, Clone)]
+pub struct CircuitPropagator<Var> {
+    successors: Box<[Var]>,
+    inference_code: InferenceCode,
+}
+
+impl<Var: IntegerVariable + 'static> Propagator for CircuitPropagator<Var> {
+    fn name(&self) -> &str {
+        "Circuit"
+    }
+
+    fn priority(&self) -> Priority {
+        // TODO
+        Priority::Medium
+    }
+
+    fn propagate_from_scratch(&self, mut context: PropagationContext) -> PropagationStatusCP {
+        // Note that circuit is currently 1-indexed!
+        self.check(context.domains())?;
+
+        self.prevent(&mut context)
+    }
+}
+
+impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
+    fn check(&self, context: Domains) -> PropagationStatusCP {
+        todo!()
+    }
+
+    fn prevent(&self, context: &mut PropagationContext) -> PropagationStatusCP {
+        todo!()
+    }
+}
diff --git a/pumpkin-crates/propagators/src/propagators/mod.rs b/pumpkin-crates/propagators/src/propagators/mod.rs
index f29a87a30..b5c721375 100644
--- a/pumpkin-crates/propagators/src/propagators/mod.rs
+++ b/pumpkin-crates/propagators/src/propagators/mod.rs
@@ -5,6 +5,7 @@
 use pumpkin_core::propagation;
 
 pub mod arithmetic;
+pub mod circuit;
 pub mod cumulative;
 pub mod disjunctive;
 pub mod element;
diff --git a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/post_constraints.rs b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/post_constraints.rs
index e72963c14..8c9d2d074 100644
--- a/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/post_constraints.rs
+++ b/pumpkin-solver/src/bin/pumpkin-solver/flatzinc/compiler/post_constraints.rs
@@ -345,6 +345,7 @@ pub(crate) fn run(
             "pumpkin_cumulative_var" => todo!(
                 "The `cumulative` constraint with variable duration/resource consumption/bound is not implemented yet!"
             ),
+            "pumpkin_circuit" => compile_circuit(context, exprs, options, constraint_tag)?,
             unknown => todo!("unsupported constraint {unknown}"),
         };
 
@@ -419,6 +420,20 @@ fn compile_cumulative(
     Ok(post_result.is_ok())
 }
 
+fn compile_circuit(
+    context: &mut CompilationContext<'_>,
+    exprs: &[flatzinc::Expr],
+    _options: &FlatZincOptions,
+    constraint_tag: ConstraintTag,
+) -> Result<bool, FlatZincError> {
+    check_parameters!(exprs, 1, "pumpkin_circuit");
+
+    let successors = context.resolve_integer_variable_array(&exprs[0])?.to_vec();
+
+    let post_result = pumpkin_constraints::circuit(successors, constraint_tag).post(context.solver);
+    Ok(post_result.is_ok())
+}
+
 fn compile_array_int_maximum(
     context: &mut CompilationContext<'_>,
     exprs: &[flatzinc::Expr],

From 46bf1dc4240acdc333df1a3e4e4748fbc233895c Mon Sep 17 00:00:00 2001
From: Imko Marijnissen <imko.marijnissen@gmail.com>
Date: Tue, 10 Mar 2026 09:10:58 +0100
Subject: [PATCH 02/10] feat: add circuit check

---
 Cargo.lock                                    |   7 +
 pumpkin-crates/propagators/Cargo.toml         |   1 +
 .../src/propagators/circuit/propagator.rs     | 168 +++++++++++++++++-
 3 files changed, 168 insertions(+), 8 deletions(-)

diff --git a/Cargo.lock b/Cargo.lock
index 6798d34cb..483741e11 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -459,6 +459,12 @@ version = "0.1.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "5baebc0774151f905a1a2cc41989300b1e6fbb29aff0ceffa1064fdd3088d582"
 
+[[package]]
+name = "fixedbitset"
+version = "0.5.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1d674e81391d1e1ab681a28d99df07927c6d4aa5b027d7da16ba32d1d21ecd99"
+
 [[package]]
 name = "flate2"
 version = "1.1.9"
@@ -1025,6 +1031,7 @@ dependencies = [
  "clap",
  "convert_case",
  "enumset",
+ "fixedbitset",
  "pumpkin-checking",
  "pumpkin-core",
 ]
diff --git a/pumpkin-crates/propagators/Cargo.toml b/pumpkin-crates/propagators/Cargo.toml
index 02e9a4e60..7d6f69fc8 100644
--- a/pumpkin-crates/propagators/Cargo.toml
+++ b/pumpkin-crates/propagators/Cargo.toml
@@ -17,6 +17,7 @@ enumset = "1.1.2"
 bitfield-struct = "0.9.2"
 convert_case = "0.8.0"
 clap = { version = "4.5.40", optional = true, features=["derive"]}
+fixedbitset = "0.5.7"
 
 [features]
 clap = ["dep:clap", "pumpkin-core/clap"]
diff --git a/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs b/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
index 5ca2ba9a4..9f9cad243 100644
--- a/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
+++ b/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
@@ -1,15 +1,25 @@
+use fixedbitset::FixedBitSet;
+use pumpkin_core::asserts::pumpkin_assert_moderate;
 use pumpkin_core::declare_inference_label;
+use pumpkin_core::predicate;
+use pumpkin_core::predicates::PropositionalConjunction;
 use pumpkin_core::proof::ConstraintTag;
 use pumpkin_core::proof::InferenceCode;
 use pumpkin_core::propagation::DomainEvents;
 use pumpkin_core::propagation::Domains;
+use pumpkin_core::propagation::EnqueueDecision;
 use pumpkin_core::propagation::InferenceCheckers;
 use pumpkin_core::propagation::LocalId;
+use pumpkin_core::propagation::NotificationContext;
+use pumpkin_core::propagation::OpaqueDomainEvent;
 use pumpkin_core::propagation::Priority;
 use pumpkin_core::propagation::PropagationContext;
 use pumpkin_core::propagation::Propagator;
 use pumpkin_core::propagation::PropagatorConstructor;
+use pumpkin_core::propagation::ReadDomains;
 use pumpkin_core::results::PropagationStatusCP;
+use pumpkin_core::state::Conflict;
+use pumpkin_core::state::PropagatorConflict;
 use pumpkin_core::variables::IntegerVariable;
 
 use crate::circuit::CircuitChecker;
@@ -38,9 +48,17 @@ impl<Var: IntegerVariable + 'static> PropagatorConstructor for CircuitConstructo
                 )
             });
 
+        let mut recently_fixed = FixedBitSet::with_capacity(self.successors.len());
+        for (index, var) in self.successors.iter().enumerate() {
+            if context.is_fixed(var) {
+                recently_fixed.insert(index);
+            }
+        }
+
         CircuitPropagator {
             successors: self.successors,
             inference_code: InferenceCode::new(self.constraint_tag, CircuitPrevent),
+            recently_fixed,
         }
     }
 
@@ -60,6 +78,8 @@ declare_inference_label!(CircuitPrevent);
 pub struct CircuitPropagator<Var> {
     successors: Box<[Var]>,
     inference_code: InferenceCode,
+
+    recently_fixed: FixedBitSet,
 }
 
 impl<Var: IntegerVariable + 'static> Propagator for CircuitPropagator<Var> {
@@ -72,20 +92,152 @@ impl<Var: IntegerVariable + 'static> Propagator for CircuitPropagator<Var> {
         Priority::Medium
     }
 
-    fn propagate_from_scratch(&self, mut context: PropagationContext) -> PropagationStatusCP {
-        // Note that circuit is currently 1-indexed!
-        self.check(context.domains())?;
+    fn notify(
+        &mut self,
+        _context: NotificationContext,
+        local_id: LocalId,
+        _event: OpaqueDomainEvent,
+    ) -> EnqueueDecision {
+        self.recently_fixed.insert(local_id.unpack() as usize);
+        EnqueueDecision::Enqueue
+    }
+
+    fn propagate(&mut self, mut context: PropagationContext) -> PropagationStatusCP {
+        self.check(context.domains())
+    }
 
-        self.prevent(&mut context)
+    fn propagate_from_scratch(&self, context: PropagationContext) -> PropagationStatusCP {
+        todo!()
     }
 }
 
 impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
-    fn check(&self, context: Domains) -> PropagationStatusCP {
-        todo!()
+    fn check(&mut self, context: Domains) -> PropagationStatusCP {
+        let mut explored = FixedBitSet::with_capacity(self.successors.len());
+        let mut cycle = Vec::default();
+
+        // We look at the variables which were recently fixed and use them as potential starts of
+        // cycles
+        while let Some(start) = self.recently_fixed.ones().next() {
+            self.recently_fixed.remove(start);
+
+            // We have already seen this variable when attempting to explore a previous chain, but
+            // it did not lead to a conflict; we do not need to consider this variable as the start
+            // of a cycle again
+            if explored.contains(start) {
+                continue;
+            }
+
+            // We consider a new cycle
+            cycle.clear();
+            let mut current = start;
+
+            // We will traverse the fixed path until we find a cycle
+            loop {
+                let var = &self.successors[current];
+
+                // If we have seen this node before, then we can simply return here
+                if explored.contains(current) {
+                    // Of course, if it is a cycle containing all nodes, then we do not need to
+                    // report an error
+                    if cycle.len() == self.successors.len() {
+                        return Ok(());
+                    }
+
+                    // But if it is a cycle which contains all, then we should
+                    return Err(Conflict::Propagator(PropagatorConflict {
+                        conjunction: self.create_conflict_explanation(context, &cycle),
+                        inference_code: self.inference_code.clone(),
+                    }));
+                }
+
+                // If the current variable is fixed, then we continue looking for a cycle by going
+                // to the next node; if not, then we can break from this loop, since it is not a
+                // cycle
+                if context.is_fixed(var) {
+                    // First, we mark the current node as explored and as part of the potential
+                    // cycle
+                    explored.insert(current);
+                    cycle.push(start);
+
+                    // Then we move on to the next node
+                    current = (context.lower_bound(var) - 1) as usize;
+                } else {
+                    break;
+                }
+            }
+        }
+
+        Ok(())
     }
 
-    fn prevent(&self, context: &mut PropagationContext) -> PropagationStatusCP {
-        todo!()
+    fn create_conflict_explanation(
+        &self,
+        context: Domains,
+        cycle: &[usize],
+    ) -> PropositionalConjunction {
+        cycle
+            .iter()
+            .map(|&index| {
+                let var = &self.successors[index];
+
+                pumpkin_assert_moderate!(context.is_fixed(var));
+
+                predicate!(var == context.lower_bound(var))
+            })
+            .collect()
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use pumpkin_core::state::State;
+
+    use crate::circuit::CircuitConstructor;
+
+    #[test]
+    fn circuit_hamiltonian_path_conflict_detection() {
+        let mut state = State::default();
+
+        let x = state.new_interval_variable(2, 2, None);
+        let y = state.new_interval_variable(3, 3, None);
+        let z = state.new_interval_variable(1, 1, None);
+
+        let constraint_tag = state.new_constraint_tag();
+
+        let _ = state.add_propagator(CircuitConstructor {
+            successors: vec![x, y, z].into(),
+            constraint_tag,
+        });
+
+        let result = state.propagate_to_fixed_point();
+
+        assert!(
+            result.is_ok(),
+            "If there is a cycle concerning all variables, then no conflict should be reported"
+        )
+    }
+
+    #[test]
+    fn circuit_conflict_detection_simple() {
+        let mut state = State::default();
+
+        let x = state.new_interval_variable(2, 2, None);
+        let y = state.new_interval_variable(1, 1, None);
+        let z = state.new_interval_variable(1, 3, None);
+
+        let constraint_tag = state.new_constraint_tag();
+
+        let _ = state.add_propagator(CircuitConstructor {
+            successors: vec![x, y, z].into(),
+            constraint_tag,
+        });
+
+        let result = state.propagate_to_fixed_point();
+
+        assert!(
+            result.is_err(),
+            "If there is a cycle concerning all variables, then no conflict should be reported"
+        )
     }
 }

From 6ac3fbb2ab810deb40e50bcc4846a0136fe63601 Mon Sep 17 00:00:00 2001
From: Imko Marijnissen <imko.marijnissen@gmail.com>
Date: Tue, 10 Mar 2026 09:22:21 +0100
Subject: [PATCH 03/10] feat: more prevent setup

---
 .../src/propagators/circuit/propagator.rs     | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

diff --git a/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs b/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
index 9f9cad243..0dd8250ec 100644
--- a/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
+++ b/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
@@ -103,7 +103,8 @@ impl<Var: IntegerVariable + 'static> Propagator for CircuitPropagator<Var> {
     }
 
     fn propagate(&mut self, mut context: PropagationContext) -> PropagationStatusCP {
-        self.check(context.domains())
+        self.check(context.domains())?;
+        self.prevent(context)
     }
 
     fn propagate_from_scratch(&self, context: PropagationContext) -> PropagationStatusCP {
@@ -111,6 +112,18 @@ impl<Var: IntegerVariable + 'static> Propagator for CircuitPropagator<Var> {
     }
 }
 
+impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
+    fn prevent(&mut self, mut context: PropagationContext) -> PropagationStatusCP {}
+
+    fn create_prevent_explanation(
+        &self,
+        context: Domains,
+        path: &[usize],
+    ) -> PropositionalConjunction {
+        todo!()
+    }
+}
+
 impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
     fn check(&mut self, context: Domains) -> PropagationStatusCP {
         let mut explored = FixedBitSet::with_capacity(self.successors.len());
@@ -146,7 +159,7 @@ impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
 
                     // But if it is a cycle which contains all, then we should
                     return Err(Conflict::Propagator(PropagatorConflict {
-                        conjunction: self.create_conflict_explanation(context, &cycle),
+                        conjunction: self.create_check_explanation(context, &cycle),
                         inference_code: self.inference_code.clone(),
                     }));
                 }
@@ -171,7 +184,7 @@ impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
         Ok(())
     }
 
-    fn create_conflict_explanation(
+    fn create_check_explanation(
         &self,
         context: Domains,
         cycle: &[usize],

From 560f82e6456246722153ff1878f15207305dfa93 Mon Sep 17 00:00:00 2001
From: Imko Marijnissen <imko.marijnissen@gmail.com>
Date: Tue, 10 Mar 2026 10:03:53 +0100
Subject: [PATCH 04/10] fix: check issues

---
 .../src/propagators/circuit/propagator.rs     | 61 +++++++++++++++----
 1 file changed, 48 insertions(+), 13 deletions(-)

diff --git a/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs b/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
index 0dd8250ec..b396dd4e3 100644
--- a/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
+++ b/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
@@ -45,7 +45,12 @@ impl<Var: IntegerVariable + 'static> PropagatorConstructor for CircuitConstructo
                     successor.clone(),
                     DomainEvents::ASSIGN,
                     LocalId::from(index as u32),
-                )
+                );
+                context.register_backtrack(
+                    successor.clone(),
+                    DomainEvents::ASSIGN,
+                    LocalId::from(index as u32),
+                );
             });
 
         let mut recently_fixed = FixedBitSet::with_capacity(self.successors.len());
@@ -102,9 +107,18 @@ impl<Var: IntegerVariable + 'static> Propagator for CircuitPropagator<Var> {
         EnqueueDecision::Enqueue
     }
 
+    fn notify_backtrack(
+        &mut self,
+        _context: Domains,
+        local_id: LocalId,
+        _event: OpaqueDomainEvent,
+    ) {
+        self.recently_fixed.remove(local_id.unpack() as usize);
+    }
+
     fn propagate(&mut self, mut context: PropagationContext) -> PropagationStatusCP {
-        self.check(context.domains())?;
-        self.prevent(context)
+        self.check(context.domains())
+        // self.prevent(context)
     }
 
     fn propagate_from_scratch(&self, context: PropagationContext) -> PropagationStatusCP {
@@ -113,7 +127,9 @@ impl<Var: IntegerVariable + 'static> Propagator for CircuitPropagator<Var> {
 }
 
 impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
-    fn prevent(&mut self, mut context: PropagationContext) -> PropagationStatusCP {}
+    fn prevent(&mut self, mut context: PropagationContext) -> PropagationStatusCP {
+        todo!()
+    }
 
     fn create_prevent_explanation(
         &self,
@@ -126,22 +142,31 @@ impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
 
 impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
     fn check(&mut self, context: Domains) -> PropagationStatusCP {
-        let mut explored = FixedBitSet::with_capacity(self.successors.len());
+        // We keep track of:
+        // 1. `cycle` - The elements which are in the (potential) current cycle; these are used in
+        //    the explanation
+        // 2. `explored` - The elements which have been visited; once we encounter any of these
+        //    nodes, we can stop since we have already explored them
+        // 3. `explored_current_iteration` - The elements which have been visited as part of the
+        //    (potential) current cycle; used to detect when a cycle has occurred. Note that using
+        //    `explored` for this purpose would be incorrect and would lead to conflicts being
+        //    detected which are not actual cycles.
         let mut cycle = Vec::default();
+        let mut explored = FixedBitSet::with_capacity(self.successors.len());
+        let mut explored_current_iteration = FixedBitSet::with_capacity(self.successors.len());
 
         // We look at the variables which were recently fixed and use them as potential starts of
         // cycles
         while let Some(start) = self.recently_fixed.ones().next() {
             self.recently_fixed.remove(start);
 
-            // We have already seen this variable when attempting to explore a previous chain, but
-            // it did not lead to a conflict; we do not need to consider this variable as the start
-            // of a cycle again
+            // If we have already explored this node before, then we can continue
             if explored.contains(start) {
                 continue;
             }
 
             // We consider a new cycle
+            explored_current_iteration.clear();
             cycle.clear();
             let mut current = start;
 
@@ -149,8 +174,9 @@ impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
             loop {
                 let var = &self.successors[current];
 
-                // If we have seen this node before, then we can simply return here
-                if explored.contains(current) {
+                // If we have seen this node befor in the current iteration, then we can simply
+                // return here
+                if explored_current_iteration.contains(current) {
                     // Of course, if it is a cycle containing all nodes, then we do not need to
                     // report an error
                     if cycle.len() == self.successors.len() {
@@ -168,13 +194,22 @@ impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
                 // to the next node; if not, then we can break from this loop, since it is not a
                 // cycle
                 if context.is_fixed(var) {
-                    // First, we mark the current node as explored and as part of the potential
+                    let next = (context.lower_bound(var) - 1) as usize;
+
+                    // If we have already encountered this node, then we know that a cycle cannot
+                    // be found from this node.
+                    if explored.contains(current) {
+                        break;
+                    }
+
+                    // Next, we mark the current node as explored and as part of the potential
                     // cycle
                     explored.insert(current);
-                    cycle.push(start);
+                    explored_current_iteration.insert(current);
+                    cycle.push(current);
 
                     // Then we move on to the next node
-                    current = (context.lower_bound(var) - 1) as usize;
+                    current = next;
                 } else {
                     break;
                 }

From 3e7785efda4ee804942efc688772f0fe2dc1212a Mon Sep 17 00:00:00 2001
From: Imko Marijnissen <imko.marijnissen@gmail.com>
Date: Wed, 11 Mar 2026 11:17:52 +0100
Subject: [PATCH 05/10] feat: add prevent algorithm

---
 .../src/propagators/circuit/propagator.rs     | 46 +++++++++++++++++--
 1 file changed, 42 insertions(+), 4 deletions(-)

diff --git a/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs b/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
index b396dd4e3..3dfefc843 100644
--- a/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
+++ b/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
@@ -117,8 +117,8 @@ impl<Var: IntegerVariable + 'static> Propagator for CircuitPropagator<Var> {
     }
 
     fn propagate(&mut self, mut context: PropagationContext) -> PropagationStatusCP {
-        self.check(context.domains())
-        // self.prevent(context)
+        self.check(context.domains())?;
+        self.prevent(context)
     }
 
     fn propagate_from_scratch(&self, context: PropagationContext) -> PropagationStatusCP {
@@ -128,7 +128,37 @@ impl<Var: IntegerVariable + 'static> Propagator for CircuitPropagator<Var> {
 
 impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
     fn prevent(&mut self, mut context: PropagationContext) -> PropagationStatusCP {
-        todo!()
+        let mut has_incoming_edge = FixedBitSet::with_capacity(self.successors.len());
+        for successor in self.successors.iter() {
+            if context.is_fixed(successor) {
+                let next = (context.lower_bound(successor) - 1) as usize;
+                has_incoming_edge.insert(next);
+            }
+        }
+
+        // Unmarked and fixed means that it is a beginning of a chain
+        for unmarked in has_incoming_edge
+            .zeroes()
+            .filter(|&index| context.is_fixed(&self.successors[index]))
+            .collect::<Vec<_>>()
+        {
+            let mut path = vec![unmarked];
+
+            let mut next = (context.lower_bound(&self.successors[unmarked]) - 1) as usize;
+            while context.is_fixed(&self.successors[next]) {
+                path.push(next);
+                next = (context.lower_bound(&self.successors[next]) - 1) as usize;
+            }
+
+            let reason = self.create_prevent_explanation(context.domains(), &path);
+            context.post(
+                predicate!(self.successors[next] != (unmarked + 1) as i32),
+                reason,
+                &self.inference_code,
+            )?;
+        }
+
+        Ok(())
     }
 
     fn create_prevent_explanation(
@@ -136,7 +166,15 @@ impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
         context: Domains,
         path: &[usize],
     ) -> PropositionalConjunction {
-        todo!()
+        path.iter()
+            .map(|&index| {
+                let var = &self.successors[index];
+
+                pumpkin_assert_moderate!(context.is_fixed(var));
+
+                predicate!(var == context.lower_bound(var))
+            })
+            .collect()
     }
 }
 

From 0ef035643dcb98a7aae792be3b61c7c8eac81baf Mon Sep 17 00:00:00 2001
From: Imko Marijnissen <imko.marijnissen@gmail.com>
Date: Wed, 11 Mar 2026 12:02:44 +0100
Subject: [PATCH 06/10] feat: add simple checker + add self-loop detection

---
 .../src/propagators/circuit/checker.rs        | 30 +++++++++++++++++--
 .../src/propagators/circuit/propagator.rs     |  9 ++++++
 2 files changed, 36 insertions(+), 3 deletions(-)

diff --git a/pumpkin-crates/propagators/src/propagators/circuit/checker.rs b/pumpkin-crates/propagators/src/propagators/circuit/checker.rs
index 450e79234..0326376a8 100644
--- a/pumpkin-crates/propagators/src/propagators/circuit/checker.rs
+++ b/pumpkin-crates/propagators/src/propagators/circuit/checker.rs
@@ -1,3 +1,4 @@
+use fixedbitset::FixedBitSet;
 use pumpkin_checking::AtomicConstraint;
 use pumpkin_checking::CheckerVariable;
 use pumpkin_checking::InferenceChecker;
@@ -15,9 +16,32 @@ where
     fn check(
         &self,
         state: pumpkin_checking::VariableState<Atomic>,
-        premises: &[Atomic],
-        consequent: Option<&Atomic>,
+        _premises: &[Atomic],
+        _consequent: Option<&Atomic>,
     ) -> bool {
-        todo!()
+        let mut explored = FixedBitSet::with_capacity(self.successors.len()).clone();
+        let start = self
+            .successors
+            .iter()
+            .position(|var| var.induced_fixed_value(&state).is_some());
+
+        if start.is_none() {
+            return false;
+        }
+
+        let start = start.unwrap();
+
+        explored.insert(start);
+        let mut next = (self.successors[start].induced_fixed_value(&state).unwrap() - 1) as usize;
+
+        while let Some(next_fixed) = self.successors[next].induced_fixed_value(&state) {
+            if explored.contains(next) {
+                return true;
+            }
+            explored.insert(next);
+            next = (next_fixed - 1) as usize;
+        }
+
+        return false;
     }
 }
diff --git a/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs b/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
index 3dfefc843..f8ea0bf45 100644
--- a/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
+++ b/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
@@ -1,5 +1,6 @@
 use fixedbitset::FixedBitSet;
 use pumpkin_core::asserts::pumpkin_assert_moderate;
+use pumpkin_core::conjunction;
 use pumpkin_core::declare_inference_label;
 use pumpkin_core::predicate;
 use pumpkin_core::predicates::PropositionalConjunction;
@@ -117,6 +118,14 @@ impl<Var: IntegerVariable + 'static> Propagator for CircuitPropagator<Var> {
     }
 
     fn propagate(&mut self, mut context: PropagationContext) -> PropagationStatusCP {
+        for (i, successor) in self.successors.iter().enumerate() {
+            context.post(
+                predicate!(successor != (i + 1) as i32),
+                conjunction!(),
+                &self.inference_code,
+            )?;
+        }
+
         self.check(context.domains())?;
         self.prevent(context)
     }

From 4c2373871ef7b785cc5da3ea63e75de10796c64f Mon Sep 17 00:00:00 2001
From: Imko Marijnissen <imko.marijnissen@gmail.com>
Date: Wed, 11 Mar 2026 13:41:57 +0100
Subject: [PATCH 07/10] feat: only perform self-loop removal in first iteration

---
 .../src/propagators/circuit/propagator.rs     | 19 +++++++++++++------
 1 file changed, 13 insertions(+), 6 deletions(-)

diff --git a/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs b/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
index f8ea0bf45..df904a25c 100644
--- a/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
+++ b/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
@@ -62,6 +62,7 @@ impl<Var: IntegerVariable + 'static> PropagatorConstructor for CircuitConstructo
         }
 
         CircuitPropagator {
+            first_iteration: true,
             successors: self.successors,
             inference_code: InferenceCode::new(self.constraint_tag, CircuitPrevent),
             recently_fixed,
@@ -82,6 +83,8 @@ declare_inference_label!(CircuitPrevent);
 
 #[derive(Debug, Clone)]
 pub struct CircuitPropagator<Var> {
+    first_iteration: bool,
+
     successors: Box<[Var]>,
     inference_code: InferenceCode,
 
@@ -118,12 +121,16 @@ impl<Var: IntegerVariable + 'static> Propagator for CircuitPropagator<Var> {
     }
 
     fn propagate(&mut self, mut context: PropagationContext) -> PropagationStatusCP {
-        for (i, successor) in self.successors.iter().enumerate() {
-            context.post(
-                predicate!(successor != (i + 1) as i32),
-                conjunction!(),
-                &self.inference_code,
-            )?;
+        // If it is the first iteration, then we remove self-loops
+        if self.first_iteration {
+            self.first_iteration = false;
+            for (i, successor) in self.successors.iter().enumerate() {
+                context.post(
+                    predicate!(successor != (i + 1) as i32),
+                    conjunction!(),
+                    &self.inference_code,
+                )?;
+            }
         }
 
         self.check(context.domains())?;

From c16419a0ed369ebf9633a7baceaa3cf2f4c13184 Mon Sep 17 00:00:00 2001
From: Imko Marijnissen <imko.marijnissen@gmail.com>
Date: Thu, 12 Mar 2026 08:04:36 +0100
Subject: [PATCH 08/10] refactor: cleaning up the propagator + fixing the
 checker based on Maarten's contributions

---
 .../core/src/propagation/domains.rs           |   9 ++
 .../hypercube_linear/propagator.rs            |   2 +-
 .../src/propagators/circuit/checker.rs        |  38 +++---
 .../src/propagators/circuit/propagator.rs     | 112 +++++++++++-------
 4 files changed, 102 insertions(+), 59 deletions(-)

diff --git a/pumpkin-crates/core/src/propagation/domains.rs b/pumpkin-crates/core/src/propagation/domains.rs
index 9d01e218d..5b1bb5e58 100644
--- a/pumpkin-crates/core/src/propagation/domains.rs
+++ b/pumpkin-crates/core/src/propagation/domains.rs
@@ -76,6 +76,10 @@ pub trait ReadDomains {
     /// fixed).
     fn is_fixed<Var: IntegerVariable>(&self, var: &Var) -> bool;
 
+    /// Returns the fixed value if the domain of the given variable is singleton (i.e., the variable
+    /// is fixed).
+    fn fixed_value<Var: IntegerVariable>(&self, var: &Var) -> Option<i32>;
+
     /// Returns the lowest value in the domain of `var`.
     fn lower_bound<Var: IntegerVariable>(&self, var: &Var) -> i32;
 
@@ -181,6 +185,11 @@ impl<T: HasAssignments> ReadDomains for T {
         self.lower_bound(var) == self.upper_bound(var)
     }
 
+    fn fixed_value<Var: IntegerVariable>(&self, var: &Var) -> Option<i32> {
+        let lower_bound = self.lower_bound(var);
+        (lower_bound == self.upper_bound(var)).then_some(lower_bound)
+    }
+
     fn lower_bound<Var: IntegerVariable>(&self, var: &Var) -> i32 {
         var.lower_bound(self.assignments())
     }
diff --git a/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs b/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs
index 8cab794e6..0e8da9ddd 100644
--- a/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs
+++ b/pumpkin-crates/core/src/propagators/hypercube_linear/propagator.rs
@@ -60,7 +60,7 @@ impl PropagatorConstructor for HypercubeLinearConstructor {
         } else {
             let last_idx = hypercube_predicates.len() - 1;
             [
-                context.register_predicate(hypercube_predicates[0.min(last_idx)]),
+                context.register_predicate(hypercube_predicates[0]),
                 context.register_predicate(hypercube_predicates[1.min(last_idx)]),
             ]
         };
diff --git a/pumpkin-crates/propagators/src/propagators/circuit/checker.rs b/pumpkin-crates/propagators/src/propagators/circuit/checker.rs
index 0326376a8..ddc37580d 100644
--- a/pumpkin-crates/propagators/src/propagators/circuit/checker.rs
+++ b/pumpkin-crates/propagators/src/propagators/circuit/checker.rs
@@ -19,29 +19,31 @@ where
         _premises: &[Atomic],
         _consequent: Option<&Atomic>,
     ) -> bool {
-        let mut explored = FixedBitSet::with_capacity(self.successors.len()).clone();
-        let start = self
-            .successors
-            .iter()
-            .position(|var| var.induced_fixed_value(&state).is_some());
-
-        if start.is_none() {
-            return false;
-        }
+        for successor in self.successors.iter() {
+            let Some(next_node) = successor.induced_fixed_value(&state) else {
+                continue;
+            };
+
+            // circuit is 1-indexed
+            let mut next_idx = usize::try_from(next_node).unwrap() - 1;
+
+            let mut visited = FixedBitSet::with_capacity(self.successors.len());
+
+            loop {
+                if visited.contains(next_idx) && visited.count_ones(..) < self.successors.len() {
+                    return true;
+                }
 
-        let start = start.unwrap();
+                visited.insert(next_idx);
 
-        explored.insert(start);
-        let mut next = (self.successors[start].induced_fixed_value(&state).unwrap() - 1) as usize;
+                let Some(next_node) = self.successors[next_idx].induced_fixed_value(&state) else {
+                    break;
+                };
 
-        while let Some(next_fixed) = self.successors[next].induced_fixed_value(&state) {
-            if explored.contains(next) {
-                return true;
+                next_idx = usize::try_from(next_node).unwrap() - 1;
             }
-            explored.insert(next);
-            next = (next_fixed - 1) as usize;
         }
 
-        return false;
+        false
     }
 }
diff --git a/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs b/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
index df904a25c..7d660d843 100644
--- a/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
+++ b/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
@@ -1,5 +1,4 @@
 use fixedbitset::FixedBitSet;
-use pumpkin_core::asserts::pumpkin_assert_moderate;
 use pumpkin_core::conjunction;
 use pumpkin_core::declare_inference_label;
 use pumpkin_core::predicate;
@@ -124,54 +123,73 @@ impl<Var: IntegerVariable + 'static> Propagator for CircuitPropagator<Var> {
         // If it is the first iteration, then we remove self-loops
         if self.first_iteration {
             self.first_iteration = false;
-            for (i, successor) in self.successors.iter().enumerate() {
-                context.post(
-                    predicate!(successor != (i + 1) as i32),
-                    conjunction!(),
-                    &self.inference_code,
-                )?;
-            }
+            self.remove_self_loops(&mut context)?;
         }
 
         self.check(context.domains())?;
         self.prevent(context)
     }
 
-    fn propagate_from_scratch(&self, context: PropagationContext) -> PropagationStatusCP {
+    fn propagate_from_scratch(&self, _context: PropagationContext) -> PropagationStatusCP {
         todo!()
     }
 }
 
+impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
+    fn remove_self_loops(&self, context: &mut PropagationContext) -> PropagationStatusCP {
+        for (i, successor) in self.successors.iter().enumerate() {
+            context.post(
+                predicate!(successor != (i + 1) as i32),
+                conjunction!(),
+                &self.inference_code,
+            )?;
+        }
+        Ok(())
+    }
+}
+
 impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
     fn prevent(&mut self, mut context: PropagationContext) -> PropagationStatusCP {
+        // First we identify the potential starts of chains; these are the variables which do not
+        // have any (fixed) incoming edge.
         let mut has_incoming_edge = FixedBitSet::with_capacity(self.successors.len());
         for successor in self.successors.iter() {
-            if context.is_fixed(successor) {
-                let next = (context.lower_bound(successor) - 1) as usize;
-                has_incoming_edge.insert(next);
+            if let Some(fixed_value) = context.fixed_value(successor) {
+                has_incoming_edge.insert(domain_value_to_index(fixed_value));
             }
         }
 
-        // Unmarked and fixed means that it is a beginning of a chain
-        for unmarked in has_incoming_edge
-            .zeroes()
-            .filter(|&index| context.is_fixed(&self.successors[index]))
-            .collect::<Vec<_>>()
-        {
-            let mut path = vec![unmarked];
-
-            let mut next = (context.lower_bound(&self.successors[unmarked]) - 1) as usize;
-            while context.is_fixed(&self.successors[next]) {
-                path.push(next);
-                next = (context.lower_bound(&self.successors[next]) - 1) as usize;
+        // Now we go over all variables that are potential starts of chains.
+        for unmarked in has_incoming_edge.zeroes() {
+            // If they are not fixed, then we can continue
+            let Some(fixed_value) = context.fixed_value(&self.successors[unmarked]) else {
+                continue;
+            };
+
+            // Now we keep track of the chain
+            let mut chain = vec![unmarked];
+
+            // Next we keep unfolding the chain until we run into a variable that is not fixed;
+            // note that it should not be possible to run into a cycle here since check has run
+            // before this.
+            let mut next = domain_value_to_index(fixed_value);
+            while let Some(fixed_value_next) = context.fixed_value(&self.successors[next]) {
+                // We add the next value to the chain
+                chain.push(next);
+                // And continue to unfold the chain from there
+                next = domain_value_to_index(fixed_value_next);
             }
 
-            let reason = self.create_prevent_explanation(context.domains(), &path);
-            context.post(
-                predicate!(self.successors[next] != (unmarked + 1) as i32),
-                reason,
-                &self.inference_code,
-            )?;
+            // We have found the chain, we remove the edge from the end of the chain to the
+            // beginning of the chain (if it exists)
+            if context.contains(&self.successors[next], index_to_domain_value(unmarked)) {
+                let reason = self.create_prevent_explanation(context.domains(), &chain);
+                context.post(
+                    predicate!(self.successors[next] != index_to_domain_value(unmarked)),
+                    reason,
+                    &self.inference_code,
+                )?;
+            }
         }
 
         Ok(())
@@ -186,9 +204,11 @@ impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
             .map(|&index| {
                 let var = &self.successors[index];
 
-                pumpkin_assert_moderate!(context.is_fixed(var));
-
-                predicate!(var == context.lower_bound(var))
+                predicate!(
+                    var == context
+                        .fixed_value(var)
+                        .expect("Expected every variable in the chain to be assigned")
+                )
             })
             .collect()
     }
@@ -247,9 +267,7 @@ impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
                 // If the current variable is fixed, then we continue looking for a cycle by going
                 // to the next node; if not, then we can break from this loop, since it is not a
                 // cycle
-                if context.is_fixed(var) {
-                    let next = (context.lower_bound(var) - 1) as usize;
-
+                if let Some(fixed_value) = context.fixed_value(var) {
                     // If we have already encountered this node, then we know that a cycle cannot
                     // be found from this node.
                     if explored.contains(current) {
@@ -263,7 +281,7 @@ impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
                     cycle.push(current);
 
                     // Then we move on to the next node
-                    current = next;
+                    current = domain_value_to_index(fixed_value);
                 } else {
                     break;
                 }
@@ -283,14 +301,28 @@ impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
             .map(|&index| {
                 let var = &self.successors[index];
 
-                pumpkin_assert_moderate!(context.is_fixed(var));
-
-                predicate!(var == context.lower_bound(var))
+                predicate!(
+                    var == context
+                        .fixed_value(var)
+                        .expect("Expected each variable in the cycle to be assigned")
+                )
             })
             .collect()
     }
 }
 
+const VALUE_OFFSET: usize = 1;
+
+#[inline]
+fn domain_value_to_index(domain_value: i32) -> usize {
+    domain_value as usize - VALUE_OFFSET
+}
+
+#[inline]
+fn index_to_domain_value(index: usize) -> i32 {
+    index as i32 + VALUE_OFFSET as i32
+}
+
 #[cfg(test)]
 mod tests {
     use pumpkin_core::state::State;

From 7ad73b87cfceb4a50fcf15d25c61a04eeb16f0c2 Mon Sep 17 00:00:00 2001
From: Imko Marijnissen <imko.marijnissen@gmail.com>
Date: Tue, 28 Jul 2026 11:41:04 +0200
Subject: [PATCH 09/10] fix: checker for circuit + update with docs

---
 .../src/propagators/circuit/checker.rs        | 20 ++++++++++++++-----
 .../src/propagators/circuit/propagator.rs     |  4 ++--
 2 files changed, 17 insertions(+), 7 deletions(-)

diff --git a/pumpkin-crates/propagators/src/propagators/circuit/checker.rs b/pumpkin-crates/propagators/src/propagators/circuit/checker.rs
index ddc37580d..e09137fca 100644
--- a/pumpkin-crates/propagators/src/propagators/circuit/checker.rs
+++ b/pumpkin-crates/propagators/src/propagators/circuit/checker.rs
@@ -3,6 +3,8 @@ use pumpkin_checking::AtomicConstraint;
 use pumpkin_checking::CheckerVariable;
 use pumpkin_checking::InferenceChecker;
 
+use crate::circuit::domain_value_to_index;
+
 #[derive(Debug, Clone)]
 pub struct CircuitChecker<Var> {
     pub successors: Box<[Var]>,
@@ -19,28 +21,36 @@ where
         _premises: &[Atomic],
         _consequent: Option<&Atomic>,
     ) -> bool {
+        // Try all the successors as possible starting points
         for successor in self.successors.iter() {
+            // Skip if successor is not yet fixed
             let Some(next_node) = successor.induced_fixed_value(&state) else {
                 continue;
             };
 
-            // circuit is 1-indexed
-            let mut next_idx = usize::try_from(next_node).unwrap() - 1;
+            // Otherwise, we find the index of the successor in the chain.
+            let mut next_idx = domain_value_to_index(next_node);
 
+            // We keep track of the visited elements.
             let mut visited = FixedBitSet::with_capacity(self.successors.len());
 
             loop {
-                if visited.contains(next_idx) && visited.count_ones(..) < self.successors.len() {
-                    return true;
+                if visited.contains(next_idx) {
+                    // If we have already seen the node, then we check whether it is a subtour or a
+                    // full circuit
+                    return visited.count_ones(..) < self.successors.len();
                 }
 
+                // Otherwise, we mark the successor as visited.
                 visited.insert(next_idx);
 
                 let Some(next_node) = self.successors[next_idx].induced_fixed_value(&state) else {
+                    // If there is no fixed successor, then we move to the next element.
                     break;
                 };
 
-                next_idx = usize::try_from(next_node).unwrap() - 1;
+                // Then we move to the next value in the chain.
+                next_idx = domain_value_to_index(next_node);
             }
         }
 
diff --git a/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs b/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
index 8b9c1eaf2..95f2c1eca 100644
--- a/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
+++ b/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
@@ -311,12 +311,12 @@ impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
 const VALUE_OFFSET: usize = 1;
 
 #[inline]
-fn domain_value_to_index(domain_value: i32) -> usize {
+pub(crate) fn domain_value_to_index(domain_value: i32) -> usize {
     domain_value as usize - VALUE_OFFSET
 }
 
 #[inline]
-fn index_to_domain_value(index: usize) -> i32 {
+pub(crate) fn index_to_domain_value(index: usize) -> i32 {
     index as i32 + VALUE_OFFSET as i32
 }
 

From 5481dcad3d312f99cb7186796108f34f3abd4542 Mon Sep 17 00:00:00 2001
From: Imko Marijnissen <imko.marijnissen@gmail.com>
Date: Tue, 28 Jul 2026 11:44:12 +0200
Subject: [PATCH 10/10] chore: small updates to propagator

---
 .../src/propagators/circuit/propagator.rs            | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs b/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
index 95f2c1eca..329e6d1a9 100644
--- a/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
+++ b/pumpkin-crates/propagators/src/propagators/circuit/propagator.rs
@@ -38,7 +38,9 @@ impl<Var: IntegerVariable + 'static> PropagatorConstructor for CircuitConstructo
         self,
         mut context: pumpkin_core::propagation::PropagatorConstructorContext,
     ) -> (EventsToRegister, Self::PropagatorImpl) {
+        let mut recently_fixed = FixedBitSet::with_capacity(self.successors.len());
         let mut registration = EventsToRegister::builder();
+
         for (index, successor) in self.successors.iter().enumerate() {
             registration =
                 registration.add(successor, DomainEvents::ASSIGN, LocalId::from(index as u32));
@@ -47,11 +49,8 @@ impl<Var: IntegerVariable + 'static> PropagatorConstructor for CircuitConstructo
                 DomainEvents::ASSIGN,
                 LocalId::from(index as u32),
             );
-        }
 
-        let mut recently_fixed = FixedBitSet::with_capacity(self.successors.len());
-        for (index, var) in self.successors.iter().enumerate() {
-            if context.is_fixed(var) {
+            if context.is_fixed(successor) {
                 recently_fixed.insert(index);
             }
         }
@@ -136,6 +135,11 @@ impl<Var: IntegerVariable + 'static> Propagator for CircuitPropagator<Var> {
 
 impl<Var: IntegerVariable + 'static> CircuitPropagator<Var> {
     fn remove_self_loops(&self, context: &mut PropagationContext) -> PropagationStatusCP {
+        if self.successors.len() == 1 {
+            // There is only a single possible cycle; generally this case would not occur.
+            return Ok(());
+        }
+
         for (i, successor) in self.successors.iter().enumerate() {
             context.post(
                 predicate!(successor != (i + 1) as i32),