feat: Implement Circuit Propagator

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);

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)
+    }
+}

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::*;

pumpkin-crates/propagators/Cargo.toml

@@ -17,6 +17,7 @@ enumset = "1.1.13"
 bitfield-struct = "0.13.0"
 convert_case = "0.11.0"
 clap = { version = "4.5.40", optional = true, features=["derive"]}
+fixedbitset = "0.5.7"
 
 [features]
 clap = ["dep:clap", "pumpkin-core/clap"]

pumpkin-crates/propagators/src/propagators/circuit/checker.rs

@@ -0,0 +1,59 @@
+use fixedbitset::FixedBitSet;
+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]>,
+}
+
+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 {
+        // 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;
+            };
+
+            // 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) {
+                    // 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;
+                };
+
+                // Then we move to the next value in the chain.
+                next_idx = domain_value_to_index(next_node);
+            }
+        }
+
+        false
+    }
+}

pumpkin-crates/propagators/src/propagators/circuit/mod.rs

@@ -0,0 +1,5 @@
+mod checker;
+mod propagator;
+
+pub use checker::*;
+pub use propagator::*;