From a4c554ae0879aaa17c427792ed04f2ea58e6efdd Mon Sep 17 00:00:00 2001 From: Charles Prud'homme Date: Tue, 29 Sep 2026 09:02:56 +0200 Subject: [PATCH 1/5] Add BC/AC consistency propagators for GlobalCardinality PropGccBC (bounds-consistency, Quimper et al. CP-2003) and PropGccAC (arc-consistency, Regin AAAI-96) are posted alongside the existing PropFastGCC, opt-in via GlobalCardinality(..., "BC"/"AC") or model.globalCardinality(..., "BC"/"AC"). Both share a dense flow network over the full [min, max] value range so that unrestricted ("escape") values are handled soundly. Includes a fix for AlgoGccAC's augmenting-path search: after a warm start where every variable is already matched, the search had no genuinely free variable to end an augmenting path on, so a later propagate() that raised several values' lower bounds at once could wrongly report a value's minimum as unreachable even though a trivial reassignment existed (found via fuzzing against a DEFAULT+search ground truth, after testDeficitAppearingAfterWarmStart caught it on real peaceable_queens instances under optimization). The search now also accepts a variable sitting on a value with slack as a valid endpoint, mirroring the existing donation-through-source mechanism. --- .../constraints/IIntConstraintFactory.java | 41 +- .../globalcardinality/GlobalCardinality.java | 46 +- .../nary/globalcardinality/PropGccAC.java | 112 ++++ .../nary/globalcardinality/PropGccBC.java | 119 ++++ .../globalcardinality/algo/AlgoGccAC.java | 357 ++++++++++++ .../globalcardinality/algo/AlgoGccBC.java | 529 ++++++++++++++++++ .../nary/GlobalCardinalityACTest.java | 318 +++++++++++ .../nary/GlobalCardinalityBCTest.java | 270 +++++++++ 8 files changed, 1786 insertions(+), 6 deletions(-) create mode 100644 solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/PropGccAC.java create mode 100644 solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/PropGccBC.java create mode 100644 solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/AlgoGccAC.java create mode 100644 solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/AlgoGccBC.java create mode 100644 solver/src/test/java/org/chocosolver/solver/constraints/nary/GlobalCardinalityACTest.java create mode 100644 solver/src/test/java/org/chocosolver/solver/constraints/nary/GlobalCardinalityBCTest.java diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/IIntConstraintFactory.java b/solver/src/main/java/org/chocosolver/solver/constraints/IIntConstraintFactory.java index 0320f061f5..cf8f47cbae 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/IIntConstraintFactory.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/IIntConstraintFactory.java @@ -1779,7 +1779,8 @@ default Constraint element(IntVar value, IntVar[] table, IntVar index, int offse * Creates a global cardinality constraint (GCC): * Each value values[i] should be taken by exactly occurrences[i] variables of vars. *
- * This constraint does not ensure any well-defined level of consistency, yet. + * Uses the {@code "DEFAULT"} consistency level (see + * {@link #globalCardinality(IntVar[], int[], IntVar[], boolean, String)}). * * @param vars collection of variables * @param values collection of constrained values @@ -1787,6 +1788,40 @@ default Constraint element(IntVar value, IntVar[] table, IntVar index, int offse * @param closed restricts domains of vars to values if set to true */ default Constraint globalCardinality(IntVar[] vars, int[] values, IntVar[] occurrences, boolean closed) { + return globalCardinality(vars, values, occurrences, closed, "DEFAULT"); + } + + /** + * Creates a global cardinality constraint (GCC): + * Each value values[i] should be taken by exactly occurrences[i] variables of vars. + * + * @param vars collection of variables + * @param values collection of constrained values + * @param occurrences collection of cardinality variables + * @param closed restricts domains of vars to values if set to true + * @param consistency consistency level, among {"DEFAULT", "BC", "AC"} + *

+ * DEFAULT: + *
+ * Fast filtering, without any well-defined level of consistency. + *

+ * BC: + *
+ * Bound-consistency, based on: + * C.-G. Quimper, P. van Beek, A. Lopez-Ortiz, A. Golynski, and S.B. Sadjad. + * "An efficient bounds consistency algorithm for the global cardinality + * constraint." CP-2003. + * Posted in addition to the {@code "DEFAULT"} filtering. + *

+ * AC: + *
+ * Arc-consistency, based on: + * J.-C. Regin. "Generalized Arc Consistency for Global Cardinality + * Constraint." AAAI-96. + * Posted in addition to the {@code "DEFAULT"} filtering. + */ + default Constraint globalCardinality(IntVar[] vars, int[] values, IntVar[] occurrences, + boolean closed, String consistency) { if (ref().getSolver().isLCG()) { if (ref().getSettings().warnUser()) { ref().getSolver().log().white().println("Warning: globalCardinality constraint is decomposed (due to LCG)."); @@ -1827,10 +1862,10 @@ default Constraint globalCardinality(IntVar[] vars, int[] values, IntVar[] occur v2[i] = toAdd.get(i - values.length); cards[i] = vars[0].getModel().intVar(0); } - return new GlobalCardinality(vars, v2, cards); + return new GlobalCardinality(vars, v2, cards, consistency); } } - return new GlobalCardinality(vars, values, occurrences); + return new GlobalCardinality(vars, values, occurrences, consistency); } /** diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/GlobalCardinality.java b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/GlobalCardinality.java index c030ee9002..d2984af277 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/GlobalCardinality.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/GlobalCardinality.java @@ -25,11 +25,40 @@ */ public class GlobalCardinality extends Constraint { + /** + * Consistency level enforced by the propagator(s) posted for a {@link GlobalCardinality} + * constraint. + */ + public enum Consistency { + /** + * Fast filtering (see {@link PropFastGCC}), without any well-defined consistency level + * guarantee. + */ + DEFAULT, + /** + * Bound-consistency (see {@link PropGccBC}), following: + * C.-G. Quimper, P. van Beek, A. Lopez-Ortiz, A. Golynski, and S.B. Sadjad. + * "An efficient bounds consistency algorithm for the global cardinality constraint." + * CP-2003. + */ + BC, + /** + * Arc-consistency (see {@link PropGccAC}), following: + * J.-C. Regin. "Generalized Arc Consistency for Global Cardinality Constraint." AAAI-96. + */ + AC + } + public GlobalCardinality(IntVar[] vars, int[] values, IntVar[] cards) { - super(ConstraintsName.GCC, createProp(vars, values, cards)); + this(vars, values, cards, Consistency.DEFAULT.name()); } - private static Propagator createProp(IntVar[] vars, int[] values, IntVar[] cards) { + public GlobalCardinality(IntVar[] vars, int[] values, IntVar[] cards, String consistency) { + super(ConstraintsName.GCC, createProp(vars, values, cards, Consistency.valueOf(consistency))); + } + + private static Propagator[] createProp(IntVar[] vars, int[] values, IntVar[] cards, + Consistency consistency) { assert values.length == cards.length; TIntIntHashMap map = new TIntIntHashMap(); int idx = 0; @@ -41,7 +70,18 @@ private static Propagator createProp(IntVar[] vars, int[] values, IntVar throw new UnsupportedOperationException("ERROR: multiple occurrences of value: " + v); } } - return new PropFastGCC(vars, values, map, cards); + PropFastGCC fast = new PropFastGCC(vars, values, map, cards); + switch (consistency) { + case BC: + //noinspection unchecked + return new Propagator[]{fast, new PropGccBC(vars, values, cards)}; + case AC: + //noinspection unchecked + return new Propagator[]{fast, new PropGccAC(vars, values, cards)}; + default: + //noinspection unchecked + return new Propagator[]{fast}; + } } public static Constraint reformulate(IntVar[] vars, IntVar[] card, Model model) { diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/PropGccAC.java b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/PropGccAC.java new file mode 100644 index 0000000000..9b5e57701b --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/PropGccAC.java @@ -0,0 +1,112 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.constraints.nary.globalcardinality; + +import org.chocosolver.solver.constraints.Propagator; +import org.chocosolver.solver.constraints.PropagatorPriority; +import org.chocosolver.solver.constraints.nary.globalcardinality.algo.AlgoGccAC; +import org.chocosolver.solver.exception.ContradictionException; +import org.chocosolver.solver.variables.IntVar; +import org.chocosolver.util.ESat; +import org.chocosolver.util.tools.ArrayUtils; + +import java.util.Arrays; + +/** + * Arc-consistency propagator for the Global Cardinality Constraint (GCC), based on: + * J.-C. Regin. "Generalized Arc Consistency for Global Cardinality Constraint." AAAI-96. + *

+ * Meant to be posted alongside {@link PropFastGCC}, which is left in charge of tightening the + * bounds of the cardinality variables and of the soundness/completeness of the constraint; this + * propagator only brings arc-consistency on the decision variables. + * + * @author Charles Prud'homme + */ +public class PropGccAC extends Propagator { + + //*********************************************************************************** + // VARIABLES + //*********************************************************************************** + + private final int n; + private final int n2; + private final int[] values; + private final AlgoGccAC filter; + + //*********************************************************************************** + // CONSTRUCTORS + //*********************************************************************************** + + /** + * @param decvars array of decision variables + * @param restrictedValues array of restricted values + * @param valueCardinalities array of cardinality variables, one per restricted value + */ + public PropGccAC(IntVar[] decvars, int[] restrictedValues, IntVar[] valueCardinalities) { + super(ArrayUtils.append(decvars, valueCardinalities), PropagatorPriority.QUADRATIC, false); + this.values = restrictedValues; + this.n = decvars.length; + this.n2 = values.length; + this.filter = new AlgoGccAC(this); + filter.reset(decvars); + } + + //*********************************************************************************** + // PROPAGATION + //*********************************************************************************** + + @Override + public void propagate(int evtmask) throws ContradictionException { + int gMin = Integer.MAX_VALUE; + int gMax = Integer.MIN_VALUE; + for (int i = 0; i < n; i++) { + gMin = Math.min(gMin, vars[i].getLB()); + gMax = Math.max(gMax, vars[i].getUB()); + } + for (int v : values) { + gMin = Math.min(gMin, v); + gMax = Math.max(gMax, v); + } + int range = gMax - gMin + 1; + int[] minOcc = new int[range]; + int[] maxOcc = new int[range]; + // values out of the restricted list are unconstrained: [0, n] + Arrays.fill(maxOcc, n); + for (int i = 0; i < n2; i++) { + IntVar card = vars[n + i]; + int idx = values[i] - gMin; + minOcc[idx] = card.getLB(); + maxOcc[idx] = card.getUB(); + } + filter.filter(minOcc, maxOcc, gMin); + } + + //*********************************************************************************** + // INFO + //*********************************************************************************** + + @Override + public ESat isEntailed() { + return ESat.TRUE; // redundant propagator, PropFastGCC already checks correctness + } + + @Override + public String toString() { + StringBuilder st = new StringBuilder(); + st.append("PropGccAC_("); + int i = 0; + for (; i < Math.min(4, vars.length); i++) { + st.append(vars[i].getName()).append(", "); + } + if (i < vars.length - 2) { + st.append("...,"); + } + st.append(vars[vars.length - 1].getName()).append(")"); + return st.toString(); + } + +} diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/PropGccBC.java b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/PropGccBC.java new file mode 100644 index 0000000000..74a101a863 --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/PropGccBC.java @@ -0,0 +1,119 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.constraints.nary.globalcardinality; + +import org.chocosolver.solver.constraints.Propagator; +import org.chocosolver.solver.constraints.PropagatorPriority; +import org.chocosolver.solver.constraints.nary.globalcardinality.algo.AlgoGccBC; +import org.chocosolver.solver.exception.ContradictionException; +import org.chocosolver.solver.variables.IntVar; +import org.chocosolver.solver.variables.events.IntEventType; +import org.chocosolver.util.ESat; +import org.chocosolver.util.tools.ArrayUtils; + +import java.util.Arrays; + +/** + * Bound-consistency propagator for the Global Cardinality Constraint (GCC), based on: + * C.-G. Quimper, P. van Beek, A. Lopez-Ortiz, A. Golynski, and S.B. Sadjad. + * "An efficient bounds consistency algorithm for the global cardinality constraint." CP-2003. + *

+ * Meant to be posted alongside {@link PropFastGCC}, which is left in charge of tightening + * the bounds of the cardinality variables and of the soundness/completeness of the constraint; + * this propagator only brings bound-consistency on the decision variables. + * + * @author Charles Prud'homme + */ +public class PropGccBC extends Propagator { + + //*********************************************************************************** + // VARIABLES + //*********************************************************************************** + + private final int n; + private final int n2; + private final int[] values; + private final AlgoGccBC filter; + + //*********************************************************************************** + // CONSTRUCTORS + //*********************************************************************************** + + /** + * @param decvars array of decision variables + * @param restrictedValues array of restricted values + * @param valueCardinalities array of cardinality variables, one per restricted value + */ + public PropGccBC(IntVar[] decvars, int[] restrictedValues, IntVar[] valueCardinalities) { + super(ArrayUtils.append(decvars, valueCardinalities), PropagatorPriority.LINEAR, false); + this.values = restrictedValues; + this.n = decvars.length; + this.n2 = values.length; + this.filter = new AlgoGccBC(this); + filter.reset(decvars); + } + + //*********************************************************************************** + // PROPAGATION + //*********************************************************************************** + + @Override + public void propagate(int evtmask) throws ContradictionException { + int gMin = Integer.MAX_VALUE; + int gMax = Integer.MIN_VALUE; + for (int i = 0; i < n; i++) { + gMin = Math.min(gMin, vars[i].getLB()); + gMax = Math.max(gMax, vars[i].getUB()); + } + for (int v : values) { + gMin = Math.min(gMin, v); + gMax = Math.max(gMax, v); + } + int range = gMax - gMin + 1; + int[] minOcc = new int[range]; + int[] maxOcc = new int[range]; + // values out of the restricted list are unconstrained: [0, n] + Arrays.fill(maxOcc, n); + for (int i = 0; i < n2; i++) { + IntVar card = vars[n + i]; + int idx = values[i] - gMin; + minOcc[idx] = card.getLB(); + maxOcc[idx] = card.getUB(); + } + filter.filter(minOcc, maxOcc, gMin); + } + + //*********************************************************************************** + // INFO + //*********************************************************************************** + + @Override + public int getPropagationConditions(int vIdx) { + return IntEventType.boundAndInst(); + } + + @Override + public ESat isEntailed() { + return ESat.TRUE; // redundant propagator, PropFastGCC already checks correctness + } + + @Override + public String toString() { + StringBuilder st = new StringBuilder(); + st.append("PropGccBC_("); + int i = 0; + for (; i < Math.min(4, vars.length); i++) { + st.append(vars[i].getName()).append(", "); + } + if (i < vars.length - 2) { + st.append("...,"); + } + st.append(vars[vars.length - 1].getName()).append(")"); + return st.toString(); + } + +} diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/AlgoGccAC.java b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/AlgoGccAC.java new file mode 100644 index 0000000000..0bf6583a8c --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/AlgoGccAC.java @@ -0,0 +1,357 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.constraints.nary.globalcardinality.algo; + +import org.chocosolver.solver.constraints.Propagator; +import org.chocosolver.solver.exception.ContradictionException; +import org.chocosolver.solver.variables.IntVar; +import org.chocosolver.util.graphOperations.connectivity.StrongConnectivityFinder; +import org.chocosolver.util.objects.graphs.DirectedGraph; +import org.chocosolver.util.objects.setDataStructures.ISet; +import org.chocosolver.util.objects.setDataStructures.ISetIterator; +import org.chocosolver.util.objects.setDataStructures.SetFactory; +import org.chocosolver.util.objects.setDataStructures.SetType; + +import java.util.Arrays; + +/** + * Arc-consistency algorithm for the global cardinality constraint (GCC), based on: + * J.-C. Regin. "Generalized Arc Consistency for Global Cardinality Constraint." AAAI-96. + *

+ * Finds a feasible and maximal flow over the dense range {@code [firstValue, firstValue + + * minOcc.length - 1]} (every value in the range gets its own node, {@code [0, n]}-bounded when it + * is not one of the restricted values), then removes every (variable, value) edge that crosses + * two different strongly connected components of the residual graph. + *

+ * The range must be dense (one node per value, not just the restricted ones) for the same reason + * {@link org.chocosolver.solver.constraints.nary.globalcardinality.algo.AlgoGccBC} needs a dense + * {@code minOcc}/{@code maxOcc}: a variable may have unrestricted values in its domain, and + * whether it may safely use one of them is not always a local decision — it can depend on the + * rest of the network. + * + * @author Charles Prud'homme + */ +public class AlgoGccAC { + + private static final int UNMATCHED = -1; + private static final int FROM_SOURCE = -2; + + private final Propagator aCause; + + private IntVar[] vars; + private int n; + private int range; + private int firstValue; + + // node numbering in the residual/SCC digraph: 0..n-1 vars, n..n+range-1 values (dense, + // one per value of the range), n+range the pseudo source node shared by every capacity edge. + private DirectedGraph digraph; + private StrongConnectivityFinder sccFinder; + private int[] nodeSCC; + + private int[] minOcc; + private int[] maxOcc; + private int[] matching; // var -> value index (0..range-1), transiently UNMATCHED mid-search + private int[] flow; // value index -> number of matched vars + + private ISet[] domVars; // value index -> vars whose domain currently contains it + + // BFS working memory for the augmenting-path search + private int[] fifo; + private boolean[] varVisited; + private boolean[] valueVisited; + private boolean srcVisited; + private int[] predOfVar; // var index -> value index that reached it + private int[] predOfValue; // value index -> var index that reached it, or FROM_SOURCE + private int predOfSrc; // value index that reached the source pseudo node + private boolean compatibleFlow; + + public AlgoGccAC(Propagator cause) { + this.aCause = cause; + } + + public void reset(IntVar[] variables) { + this.vars = variables; + this.n = vars.length; + this.matching = new int[n]; + Arrays.fill(matching, UNMATCHED); + this.varVisited = new boolean[n]; + this.predOfVar = new int[n]; + } + + //*********************************************************************************** + // PROPAGATION + //*********************************************************************************** + + /** + * Enforces arc-consistency on {@code vars} given dense minimum/maximum occurrence bounds over + * the contiguous range {@code [firstValue, firstValue + minOcc.length - 1]}. + * + * @param minOcc minimum number of occurrences, per value, dense on the range + * @param maxOcc maximum number of occurrences, per value, dense on the range + * @param firstValue first value of the range covered by {@code minOcc}/{@code maxOcc} + * @return {@code true} iff at least one domain update has been done + */ + public boolean filter(int[] minOcc, int[] maxOcc, int firstValue) throws ContradictionException { + this.minOcc = minOcc; + this.maxOcc = maxOcc; + this.firstValue = firstValue; + int newRange = minOcc.length; + if (domVars == null || range != newRange) { + range = newRange; + flow = new int[range]; + domVars = new ISet[range]; + for (int j = 0; j < range; j++) { + domVars[j] = SetFactory.makeBitSet(0); + } + fifo = new int[n + range + 1]; + valueVisited = new boolean[range]; + predOfValue = new int[range]; + digraph = new DirectedGraph(n + range + 1, SetType.BITSET, false); + sccFinder = new StrongConnectivityFinder(digraph); + } + prepare(); + computeFeasibleMaximalFlow(); + buildResidualDigraph(); + sccFinder.findAllSCC(); + nodeSCC = sccFinder.getNodesSCC(); + return pruneDomains(); + } + + /** + * Repairs {@code matching}/{@code flow} against the current domains and capacities, and + * rebuilds the {@code domVars} adjacency used by the augmenting-path search. + */ + private void prepare() { + for (int j = 0; j < range; j++) { + domVars[j].clear(); + } + for (int i = 0; i < n; i++) { + IntVar v = vars[i]; + int ub = v.getUB(); + for (int k = v.getLB(); k <= ub; k = v.nextValue(k)) { + domVars[k - firstValue].add(i); + } + int j = matching[i]; + if (j != UNMATCHED && !v.contains(firstValue + j)) { + matching[i] = UNMATCHED; + } + } + Arrays.fill(flow, 0); + for (int i = 0; i < n; i++) { + if (matching[i] != UNMATCHED) { + flow[matching[i]]++; + } + } + // a cardinality upper bound may have shrunk below the (previously valid) flow: drop + // enough arbitrary matches to fit back under the new capacity. + for (int j = 0; j < range; j++) { + while (flow[j] > maxOcc[j]) { + for (int i = 0; i < n; i++) { + if (matching[i] == j) { + matching[i] = UNMATCHED; + flow[j]--; + break; + } + } + } + } + // a cardinality lower bound may have grown since the warm-started matching was built: any + // deficit left over here is handled directly by the augmenting-path search below, which + // knows how to pull a variable away from a value that has slack (see findAugmentingPath). + } + + //*********************************************************************************** + // FEASIBLE + MAXIMAL FLOW (Ford-Fulkerson with lower bounds on value nodes) + //*********************************************************************************** + + private void computeFeasibleMaximalFlow() throws ContradictionException { + while (true) { + int freeVar = findAugmentingPath(); + if (freeVar == UNMATCHED) { + if (!compatibleFlow) { + aCause.fails(); // some value cannot reach its minimum: infeasible + } + // the range is dense (covers every variable's whole domain), so every variable + // must end up matched to some value; one left over means a real Hall violation. + for (int i = 0; i < n; i++) { + if (matching[i] == UNMATCHED) { + aCause.fails(); + } + } + return; // compatibleFlow phase found nothing more: maximal flow reached + } + augment(freeVar); + } + } + + /** + * Breadth-first search for an augmenting path. First tries to reach a variable that can fix + * a value under its minimum ({@code compatibleFlow = false}); once no value is under its + * minimum any more, tries to grow the flow further, up to the maxima + * ({@code compatibleFlow = true}). + * + * @return the index of a variable that can be newly matched, or {@link #UNMATCHED} if none + * is reachable + */ + private int findAugmentingPath() { + Arrays.fill(varVisited, false); + Arrays.fill(valueVisited, false); + srcVisited = false; + int head = 0; + int tail = 0; + + boolean anyDeficit = false; + for (int j = 0; j < range; j++) { + if (flow[j] < minOcc[j]) { + fifo[tail++] = n + j; + valueVisited[j] = true; + anyDeficit = true; + } + } + compatibleFlow = !anyDeficit; + if (compatibleFlow) { + for (int j = 0; j < range; j++) { + if (flow[j] < maxOcc[j]) { + fifo[tail++] = n + j; + valueVisited[j] = true; + } + } + } + + int src = n + range; + while (head < tail) { + int x = fifo[head++]; + if (x < n) { // var node, always already matched when reached this way + int j = matching[x]; + // warm start: every variable may already be matched, leaving no genuinely free + // one for the search to end on. Pulling x away from a value that has slack is + // always safe -- j keeps at least its minimum -- so it is just as good an + // endpoint: augment() will walk the same predecessor chain back to the deficient + // value either way (see BEST_PRACTICES.md). + if (!compatibleFlow && flow[j] > minOcc[j]) { + flow[j]--; + return x; + } + if (!valueVisited[j]) { + valueVisited[j] = true; + predOfValue[j] = x; + fifo[tail++] = n + j; + } + } else if (x < src) { // value node + int j = x - n; + ISetIterator it = domVars[j].iterator(); + while (it.hasNext()) { + int i = it.nextInt(); + if (matching[i] != j && !varVisited[i]) { + varVisited[i] = true; + predOfVar[i] = j; + if (matching[i] == UNMATCHED) { + return i; + } + fifo[tail++] = i; + } + } + if (!compatibleFlow && flow[j] > minOcc[j] && !srcVisited) { + srcVisited = true; + predOfSrc = j; + fifo[tail++] = src; + } + } else if (!compatibleFlow) { // source pseudo node + for (int j = 0; j < range; j++) { + if (flow[j] < maxOcc[j] && !valueVisited[j]) { + valueVisited[j] = true; + predOfValue[j] = FROM_SOURCE; + fifo[tail++] = n + j; + } + } + } + } + return UNMATCHED; + } + + /** + * Flips the matching along the augmenting path ending at {@code freeVar}, growing the flow + * of the value at the root of the path by one unit. + */ + private void augment(int freeVar) { + int varNode = freeVar; + int valIdx = predOfVar[varNode]; + if (compatibleFlow) { + while (flow[valIdx] == maxOcc[valIdx]) { + matching[varNode] = valIdx; + varNode = predOfValue[valIdx]; + valIdx = predOfVar[varNode]; + } + } else { + while (flow[valIdx] >= minOcc[valIdx]) { + matching[varNode] = valIdx; + int pred = predOfValue[valIdx]; + if (pred == FROM_SOURCE) { + flow[valIdx]++; + int donor = predOfSrc; + flow[donor]--; + varNode = predOfValue[donor]; + } else { + varNode = pred; + } + valIdx = predOfVar[varNode]; + } + } + matching[varNode] = valIdx; + flow[valIdx]++; + } + + //*********************************************************************************** + // PRUNING (strongly connected components of the residual graph) + //*********************************************************************************** + + private void buildResidualDigraph() { + int nbNodes = n + range + 1; + for (int idx = 0; idx < nbNodes; idx++) { + digraph.getSuccessorsOf(idx).clear(); + digraph.getPredecessorsOf(idx).clear(); + } + for (int i = 0; i < n; i++) { + IntVar v = vars[i]; + int ub = v.getUB(); + for (int k = v.getLB(); k <= ub; k = v.nextValue(k)) { + int j = k - firstValue; + if (matching[i] == j) { + digraph.addEdge(n + j, i); + } else { + digraph.addEdge(i, n + j); + } + } + } + int src = n + range; + for (int j = 0; j < range; j++) { + if (flow[j] < maxOcc[j]) { + digraph.addEdge(n + j, src); + } + if (flow[j] > minOcc[j]) { + digraph.addEdge(src, n + j); + } + } + } + + private boolean pruneDomains() throws ContradictionException { + boolean filter = false; + for (int i = 0; i < n; i++) { + IntVar v = vars[i]; + int ub = v.getUB(); + for (int k = v.getLB(); k <= ub; k = v.nextValue(k)) { + int j = k - firstValue; + // the matched pair is part of the feasible flow: never touch it here. + if (matching[i] != j && nodeSCC[i] != nodeSCC[n + j]) { + filter |= v.removeValue(k, aCause); + } + } + } + return filter; + } +} diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/AlgoGccBC.java b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/AlgoGccBC.java new file mode 100644 index 0000000000..e3cf0407dc --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/AlgoGccBC.java @@ -0,0 +1,529 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.constraints.nary.globalcardinality.algo; + +import org.chocosolver.solver.constraints.Propagator; +import org.chocosolver.solver.exception.ContradictionException; +import org.chocosolver.solver.variables.IntVar; +import org.chocosolver.util.sort.ArraySort; +import org.chocosolver.util.sort.IntComparator; +import org.chocosolver.util.tools.MathUtils; + +/** + * Bound-consistency algorithm for the global cardinality constraint (GCC). + *

+ * Based on: C.-G. Quimper, P. van Beek, A. Lopez-Ortiz, A. Golynski, and S.B. Sadjad. + * "An efficient bounds consistency algorithm for the global cardinality constraint." CP-2003. + * + * @author Charles Prud'homme + */ +public class AlgoGccBC { + + private final Propagator aCause; + private IntVar[] vars; + private int n; + + // Tree/diff/hall-interval links, shared across the four sub-filters of a single pass, + // exactly as in the reference implementation. + private int[] t; + private int[] d; + private int[] h; + private int[] bounds; + private int[] stableInterval; + private int[] potentialStableSets; + private int[] newMin; + + private int nbBounds; + + private Interval[] intervals; + private int[] minsorted; + private int[] maxsorted; + + private IntComparator minComp; + private IntComparator maxComp; + private ArraySort sorter; + + public AlgoGccBC(Propagator cause) { + this.aCause = cause; + } + + public void reset(IntVar[] variables) { + this.vars = variables; + this.n = vars.length; + if (intervals == null || intervals.length < n) { + t = new int[2 * n + 2]; + d = new int[2 * n + 2]; + h = new int[2 * n + 2]; + bounds = new int[2 * n + 2]; + stableInterval = new int[2 * n + 2]; + potentialStableSets = new int[2 * n + 2]; + newMin = new int[n]; + intervals = new Interval[n]; + minsorted = new int[n]; + maxsorted = new int[n]; + for (int i = 0; i < n; i++) { + intervals[i] = new Interval(); + } + sorter = new ArraySort<>(n, false, true); + } + for (int i = 0; i < n; i++) { + minsorted[i] = i; + maxsorted[i] = i; + } + minComp = (i1, i2) -> MathUtils.safeSubstract(intervals[i1].lb, intervals[i2].lb); + maxComp = (i1, i2) -> MathUtils.safeSubstract(intervals[i1].ub, intervals[i2].ub); + } + + //****************************************************************************************************************// + //****************************************************************************************************************// + //****************************************************************************************************************// + + /** + * Enforces bound-consistency on {@code vars} given dense minimum/maximum occurrence bounds + * over the contiguous range {@code [firstValue, firstValue + minOcc.length - 1]}. + * + * @param minOcc minimum number of occurrences, per value, dense on the range + * @param maxOcc maximum number of occurrences, per value, dense on the range + * @param firstValue first value of the range covered by {@code minOcc}/{@code maxOcc} + * @return {@code true} iff at least one bound update has been done + */ + public boolean filter(int[] minOcc, int[] maxOcc, int firstValue) throws ContradictionException { + int range = minOcc.length; + PartialSum l = new PartialSum(firstValue, range, minOcc); + PartialSum u = new PartialSum(firstValue, range, maxOcc); + boolean hasFiltered = false; + boolean again; + do { + sortIt(firstValue, range); + int lowLb = vars[minsorted[0]].getLB(); + int highUb = vars[maxsorted[n - 1]].getUB(); + if (l.sum(l.minValue(), lowLb - 1) > 0 || l.sum(highUb + 1, l.maxValue()) > 0) { + aCause.fails(); + } + again = filterLowerMax(u); + again |= filterLowerMin(l); + again |= filterUpperMax(u); + again |= filterUpperMin(l); + hasFiltered |= again; + } while (again); + return hasFiltered; + } + + private void sortIt(int firstValue, int range) { + for (int i = 0; i < n; i++) { + intervals[i].lb = vars[i].getLB(); + intervals[i].ub = vars[i].getUB() + 1; + } + sorter.sort(minsorted, n, minComp); + sorter.sort(maxsorted, n, maxComp); + + int min = intervals[minsorted[0]].lb; + int max = intervals[maxsorted[0]].ub; + int last = firstValue - 2; + int nb = 0; + bounds[0] = last; + + int i = 0; + int j = 0; + while (true) { + if (i < n && min <= max) { + if (min != last) { + bounds[++nb] = last = min; + } + intervals[minsorted[i]].minrank = nb; + if (++i < n) { + min = intervals[minsorted[i]].lb; + } + } else { + if (max != last) { + bounds[++nb] = last = max; + } + intervals[maxsorted[j]].maxrank = nb; + if (++j == n) { + break; + } + max = intervals[maxsorted[j]].ub; + } + } + this.nbBounds = nb; + bounds[nb + 1] = firstValue + range + 2; + } + + private void pathset(int[] tab, int start, int end, int to) { + int next = start; + int prev = next; + while (prev != end) { + next = tab[prev]; + tab[prev] = to; + prev = next; + } + } + + private int pathmin(int[] tab, int i) { + while (tab[i] < i) { + i = tab[i]; + } + return i; + } + + private int pathmax(int[] tab, int i) { + while (tab[i] > i) { + i = tab[i]; + } + return i; + } + + /** + * Shrinks the lower bounds so that no value exceeds its maximum number of occurrences. + */ + private boolean filterLowerMax(PartialSum u) throws ContradictionException { + boolean filter = false; + for (int i = 1; i <= nbBounds + 1; i++) { + t[i] = h[i] = i - 1; + d[i] = u.sum(bounds[i - 1], bounds[i] - 1); + // A slot whose capacity is ALREADY zero here (e.g. a run of consecutive values with + // maxOcc == 0) must be redirected to its upward neighbour right now, exactly as the + // main loop does when a capacity reaches zero through a decrement. Otherwise, pathmax + // can land on it, "--d[z] == 0" is never true (d[z] goes from 0 to -1, skipping the + // transition) and t[] is left inconsistent: pathset may then loop forever, or the + // Hall-interval check that should fail is silently skipped. + if (d[i] == 0) { + t[i] = i + 1; + } + } + for (int i = 0; i < n; i++) { // visit intervals in increasing max order + int idx = maxsorted[i]; + int x = intervals[idx].minrank; + int y = intervals[idx].maxrank; + int z = pathmax(t, x + 1); + int j = t[z]; + if (--d[z] == 0) { + t[z] = z + 1; + z = pathmax(t, t[z]); + t[z] = j; + } + pathset(t, x + 1, z, z); + if (d[z] < u.sum(bounds[y], bounds[z] - 1)) { + aCause.fails(); + } + if (h[x] > x) { + int w = pathmax(h, h[x]); + int hallMax = bounds[w]; + if (vars[idx].updateLowerBound(hallMax, aCause)) { + filter = true; + intervals[idx].lb = hallMax; + } + pathset(h, x, w, w); + } + if (d[z] == u.sum(bounds[y], bounds[z] - 1)) { + pathset(h, h[y], j - 1, y); + h[y] = j - 1; + } + } + return filter; + } + + /** + * Shrinks the upper bounds so that no value exceeds its maximum number of occurrences. + */ + private boolean filterUpperMax(PartialSum u) throws ContradictionException { + boolean filter = false; + for (int i = 0; i <= nbBounds; i++) { + t[i] = h[i] = i + 1; + d[i] = u.sum(bounds[i], bounds[i + 1] - 1); + // Mirror of the zero-capacity redirection in filterLowerMax: here the climb goes + // towards lower indices (pathmin), so an already-exhausted slot points downward. + if (d[i] == 0) { + t[i] = i - 1; + } + } + for (int i = n - 1; i >= 0; i--) { // visit intervals in decreasing min order + int idx = minsorted[i]; + int x = intervals[idx].maxrank; + int y = intervals[idx].minrank; + int z = pathmin(t, x - 1); + int j = t[z]; + if (--d[z] == 0) { + t[z] = z - 1; + z = pathmin(t, t[z]); + t[z] = j; + } + pathset(t, x - 1, z, z); + if (d[z] < u.sum(bounds[z], bounds[y] - 1)) { + aCause.fails(); + } + if (h[x] < x) { + int w = pathmin(h, h[x]); + int hallMin = bounds[w]; + if (vars[idx].updateUpperBound(hallMin - 1, aCause)) { + filter = true; + intervals[idx].ub = hallMin; + } + pathset(h, x, w, w); + } + if (d[z] == u.sum(bounds[z], bounds[y] - 1)) { + pathset(h, h[y], j + 1, y); + h[y] = j + 1; + } + } + return filter; + } + + /** + * Shrinks the lower bounds so that every value reaches its minimum number of occurrences. + */ + private boolean filterLowerMin(PartialSum l) throws ContradictionException { + boolean filter = false; + int i; + int j; + int w; + int x; + int y; + int z; + int v; + + for (w = i = nbBounds + 1; i > 0; i--) { + potentialStableSets[i] = stableInterval[i] = i - 1; + d[i] = l.sum(bounds[i - 1], bounds[i] - 1); + // If the capacity between both bounds is zero, we have an unstable set between them. + if (d[i] == 0) { + h[i - 1] = w; + } else { + w = h[w] = i - 1; + } + } + + for (i = w = nbBounds + 1; i >= 0; i--) { + if (d[i] == 0) { + t[i] = w; + } else { + w = t[w] = i; + } + } + + for (i = 0; i < n; i++) { // visit intervals in increasing max order + int idx = maxsorted[i]; + x = intervals[idx].minrank; + y = intervals[idx].maxrank; + j = t[z = pathmax(t, x + 1)]; + if (z != x + 1) { + // [bounds[x], bounds[z]) is a subset of a stable set + v = potentialStableSets[w = pathmax(potentialStableSets, x + 1)]; + pathset(potentialStableSets, x + 1, w, w); // path compression + w = Math.min(y, z); + pathset(potentialStableSets, potentialStableSets[w], v, w); + potentialStableSets[w] = v; + } + + if (d[z] <= l.sum(bounds[y], bounds[z] - 1)) { + // (potentialStableSets[y], y] is a stable set + w = pathmax(stableInterval, potentialStableSets[y]); + pathset(stableInterval, potentialStableSets[y], w, w); // path compression + pathset(stableInterval, stableInterval[y], v = stableInterval[w], y); + stableInterval[y] = v; + } else { + // decrease the capacity between the two bounds + if (--d[z] == 0) { + t[z] = z + 1; + z = pathmax(t, t[z]); + t[z] = j; + } + // remind the new value the variable might get, in case it is not in a stable set + if (h[x] > x) { + w = newMin[i] = pathmax(h, x); + pathset(h, x, w, w); // path compression + } else { + newMin[i] = x; // do not shrink the variable + } + // if an unstable set is discovered + if (d[z] == l.sum(bounds[y], bounds[z] - 1)) { + if (h[y] > y) { + y = h[y]; // equivalent to pathmax since the path is fully compressed + } + pathset(h, h[y], j - 1, y); // mark the new unstable set + h[y] = j - 1; + } + } + pathset(t, x + 1, z, z); // path compression + } + + // if there is a failure set + if (h[nbBounds] != 0) { + aCause.fails(); + } + + // path compression over all elements of the stable interval structure (linear, done once) + for (i = nbBounds + 1; i > 0; i--) { + if (stableInterval[i] > i) { + stableInterval[i] = w; + } else { + w = i; + } + } + + // for all variables that are not a subset of a stable set, shrink the lower bound + for (i = n - 1; i >= 0; i--) { + int idx = maxsorted[i]; + x = intervals[idx].minrank; + y = intervals[idx].maxrank; + if ((stableInterval[x] <= x) || (y > stableInterval[x])) { + int newLb = l.skipNonNullElementsRight(bounds[newMin[i]]); + if (vars[idx].updateLowerBound(newLb, aCause)) { + filter = true; + intervals[idx].lb = newLb; + } + } + } + return filter; + } + + /** + * Shrinks the upper bounds so that every value reaches its minimum number of occurrences. + * Relies on {@code stableInterval}, as computed by the last call to {@link #filterLowerMin}. + */ + private boolean filterUpperMin(PartialSum l) throws ContradictionException { + boolean filter = false; + int w = 0; + int i; + for (i = 0; i <= nbBounds; i++) { + d[i] = l.sum(bounds[i], bounds[i + 1] - 1); + if (d[i] == 0) { + t[i] = w; + } else { + w = t[w] = i; + } + } + t[w] = i; + w = 0; + for (i = 1; i <= nbBounds; i++) { + if (d[i - 1] == 0) { + h[i] = w; + } else { + w = h[w] = i; + } + } + h[w] = i; + for (i = n - 1; i >= 0; i--) { // visit intervals in decreasing min order + int idx = minsorted[i]; + int x = intervals[idx].maxrank; + int y = intervals[idx].minrank; + + int z = pathmin(t, x - 1); + int j = t[z]; + + // if the variable is not in a discovered stable set + if (d[z] > l.sum(bounds[z], bounds[y] - 1)) { + if (--d[z] == 0) { + t[z] = z - 1; + z = pathmin(t, t[z]); + t[z] = j; + } + int newMax; + if (h[x] < x) { + w = pathmin(h, h[x]); + newMax = w; + pathset(h, x, w, w); // path compression + } else { + newMax = x; + } + newMin[i] = newMax; + if (d[z] == l.sum(bounds[z], bounds[y] - 1)) { + if (h[y] < y) { + y = h[y]; + } + pathset(h, h[y], j + 1, y); + h[y] = j + 1; + } + } + pathset(t, x - 1, z, z); + } + // for all variables that are not subsets of a stable set, shrink the upper bound + for (i = n - 1; i >= 0; i--) { + int idx = minsorted[i]; + int x = intervals[idx].minrank; + int y = intervals[idx].maxrank; + if ((stableInterval[x] <= x) || (y > stableInterval[x])) { + int newUb = l.skipNonNullElementsLeft(bounds[newMin[i]] - 1); + if (vars[idx].updateUpperBound(newUb, aCause)) { + filter = true; + intervals[idx].ub = newUb + 1; + } + } + } + return filter; + } + + private static final class Interval { + private int minrank; + private int maxrank; + private int lb; + private int ub; // exclusive, i.e. getUB() + 1 + } + + /** + * Partial-sum data structure adapted to {@code filterLower{Min,Max}}/{@code filterUpper{Min,Max}}: + * sums an array of per-value occurrence bounds over any sub-range in O(1), with two sentinel + * elements of weight 1 added on each side. + */ + private static final class PartialSum { + private final int[] sum; + private final int[] ds; + private final int firstValue; + private final int lastValue; + + private PartialSum(int firstValue, int count, int[] elt) { + this.sum = new int[count + 5]; + this.firstValue = firstValue - 3; + this.lastValue = firstValue + count + 1; + sum[0] = 0; + sum[1] = 1; + sum[2] = 2; + int i; + int j; + for (i = 2; i < count + 2; i++) { + sum[i + 1] = sum[i] + elt[i - 2]; + } + sum[i + 1] = sum[i] + 1; + sum[i + 2] = sum[i + 1] + 1; + ds = new int[count + 5]; + i = count + 3; + for (j = i + 1; i > 0; ) { + while (sum[i] == sum[i - 1]) { + ds[i--] = j; + } + j = ds[j] = i--; + } + ds[j] = 0; + } + + private int sum(int from, int to) { + if (from <= to) { + return sum[to - firstValue] - sum[from - firstValue - 1]; + } else { + return sum[to - firstValue - 1] - sum[from - firstValue]; + } + } + + private int minValue() { + return firstValue + 3; + } + + private int maxValue() { + return lastValue - 2; + } + + private int skipNonNullElementsRight(int value) { + value -= firstValue; + return (Math.max(ds[value], value)) + firstValue; + } + + private int skipNonNullElementsLeft(int value) { + value -= firstValue; + return (ds[value] > value ? ds[ds[value]] : value) + firstValue; + } + } +} diff --git a/solver/src/test/java/org/chocosolver/solver/constraints/nary/GlobalCardinalityACTest.java b/solver/src/test/java/org/chocosolver/solver/constraints/nary/GlobalCardinalityACTest.java new file mode 100644 index 0000000000..d602012d7b --- /dev/null +++ b/solver/src/test/java/org/chocosolver/solver/constraints/nary/GlobalCardinalityACTest.java @@ -0,0 +1,318 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.constraints.nary; + +import org.chocosolver.solver.Model; +import org.chocosolver.solver.Providers; +import org.chocosolver.solver.SettingsBuilder; +import org.chocosolver.solver.exception.ContradictionException; +import org.chocosolver.solver.variables.IntVar; +import org.testng.annotations.Test; + +import java.util.Arrays; +import java.util.Random; + +import static org.chocosolver.solver.Cause.Null; +import static org.chocosolver.solver.constraints.nary.globalcardinality.GlobalCardinality.reformulate; +import static org.chocosolver.solver.search.strategy.Search.inputOrderLBSearch; +import static org.chocosolver.util.tools.ArrayUtils.append; +import static org.testng.Assert.assertEquals; +import static org.testng.Assert.assertFalse; +import static org.testng.Assert.assertTrue; + +/** + * Tests for the arc-consistency ({@code "AC"}) filtering of the global cardinality constraint, + * i.e. {@link org.chocosolver.solver.constraints.nary.globalcardinality.PropGccAC}. + * + * @author Charles Prud'homme + */ +public class GlobalCardinalityACTest { + + @Test(groups = "1s", timeOut = 60000) + public void testClosed() throws ContradictionException { + Model model = new Model(); + + IntVar[] vars = model.intVarArray("vars", 6, 0, 3, true); + IntVar[] card = model.intVarArray("card", 4, 0, 6, true); + + int[] values = new int[4]; + for (int i = 0; i < values.length; i++) { + values[i] = i; + } + model.globalCardinality(vars, values, card, true, "AC").post(); + + vars[0].instantiateTo(0, Null); + vars[1].instantiateTo(1, Null); + vars[2].instantiateTo(3, Null); + vars[3].instantiateTo(2, Null); + vars[4].instantiateTo(0, Null); + vars[5].instantiateTo(0, Null); + + model.getSolver().setSearch(inputOrderLBSearch(append(vars, card))); + while (model.getSolver().solve()) { + // enumerate + } + assertTrue(model.getSolver().getSolutionCount() > 0); + } + + @Test(groups = "10s", timeOut = 60000) + public void testRandomACEnumerated() { + checkAgainstDecomposition(true, false, false); + } + + @Test(groups = "10s", timeOut = 60000) + public void testRandomACBounded() { + checkAgainstDecomposition(false, false, false); + } + + @Test(groups = "10s", timeOut = 60000) + public void testRandomACClosed() { + checkAgainstDecomposition(true, true, false); + } + + /** + * Domains that spill outside the restricted value list, not closed: a variable can "escape" + * cardinality accounting entirely by taking such a value. See BEST_PRACTICES.md for why this + * requires a dense (one node per value) flow network, not just one per restricted value. + */ + @Test(groups = "10s", timeOut = 60000) + public void testRandomACExtraValuesNotClosed() { + checkAgainstDecomposition(true, false, true); + } + + /** + * Regression test: when 5 out of 81 variables can each optionally use one restricted value + * (a "staircase" of growing domains) with no cardinality lower bound at all, AC must not + * force any of them onto a restricted value: their shared escape value (1, unrestricted) + * remains valid for each of them individually. A first (unsound) implementation of the + * escape mechanism, using a single shared "unlimited capacity" node instead of one node per + * unrestricted value, wrongly forced these variables apart. Found on a real FlatZinc instance + * ({@code peaceable_queens_n9_q5.fzn}). + */ + @Test(groups = "1s", timeOut = 60000) + public void testEscapeValueKeptWhenSafe() throws ContradictionException { + int n = 81; + int[] values = {2, 3, 4, 5, 6}; + Model model = new Model(); + IntVar[] vars = new IntVar[n]; + for (int i = 0; i < n; i++) { + vars[i] = model.intVar("v" + i, 1); // fixed to the escape value by default + } + vars[75] = model.intVar("v75", new int[]{1, 2}); + vars[76] = model.intVar("v76", new int[]{1, 2, 3}); + vars[77] = model.intVar("v77", new int[]{1, 2, 3, 4}); + vars[78] = model.intVar("v78", new int[]{1, 2, 3, 4, 5}); + vars[79] = model.intVar("v79", new int[]{1, 2, 3, 4, 5, 6}); + IntVar[] cards = model.intVarArray("card", values.length, 0, 1, true); + model.globalCardinality(vars, values, cards, false, "AC").post(); + model.getSolver().propagate(); + for (int i : new int[]{75, 76, 77, 78, 79}) { + assertTrue(vars[i].contains(1), "v" + i + " should keep its escape value 1: " + vars[i]); + } + } + + /** + * Regression test, the mirror image of {@link #testEscapeValueKeptWhenSafe}: a variable's + * escape value must be removed when using it would make the rest of the network infeasible + * (here: 3 variables share the only candidates for values 3, 4 and 6, whose minimums leave no + * room for one of the three to escape). Found on the same real FlatZinc instance. + */ + @Test(groups = "1s", timeOut = 60000) + public void testEscapeValueRemovedWhenNecessary() throws ContradictionException { + int n = 81; + int[] values = {2, 3, 4, 5, 6}; + int[][] free = { + {60, 1, 2}, {63, 1, 3}, {64, 1, 3, 4}, {67, 1, 2}, {70, 1, 3, 4, 5}, + {71, 1, 3, 4, 5, 6}, {72, 1, 3, 4, 5, 6}, {73, 1, 2}, {74, 1, 3, 4, 5, 6}, + {75, 1, 2}, {76, 1, 3, 4, 5, 6}, {77, 1, 2}, {78, 1, 3, 4, 5, 6}, + }; + Model model = new Model(); + IntVar[] vars = new IntVar[n]; + for (int i = 0; i < n; i++) { + vars[i] = model.intVar("v" + i, 1); + } + for (int[] f : free) { + int idx = f[0]; + int[] dom = Arrays.copyOfRange(f, 1, f.length); + vars[idx] = model.intVar("v" + idx, dom); + } + IntVar[] cards = model.intVarArray("card", values.length, 2, 5, true); + model.globalCardinality(vars, values, cards, false, "AC").post(); + model.getSolver().propagate(); + // var63's only restricted candidate is 3: the escape (1) must have been removed, since + // the other candidates for value3 are all needed elsewhere (see BEST_PRACTICES.md). + assertTrue(vars[63].isInstantiatedTo(3), "v63 should be forced to 3: " + vars[63]); + } + + /** + * Regression test: a warm-started matching that settles every variable on a single, + * slack-having value (as happens after a first {@code propagate()} with no lower bound + * requirement at all) must not get stuck when a later {@code propagate()} raises several + * values' lower bounds at once, on the SAME persistent {@code AlgoGccAC} instance -- even + * though trivial reassignments exist. The augmenting-path search only knows how to walk a + * chain back to a free (unmatched) variable; if warm-starting leaves none, it has no entry + * point, wrongly declaring the (perfectly feasible) deficit unreachable. This mirrors what + * happens during a real MAXIMIZE search: the objective bound pushes cardinality lower bounds + * up between search nodes. Found on {@code peaceable_queens_n9_q5.fzn}/ + * {@code peaceable_queens_n8_q3.fzn} under optimization, where AC wrongly proved a bound + * strictly lower than BC's/the true optimum. See BEST_PRACTICES.md. + */ + @Test(groups = "1s", timeOut = 60000) + public void testDeficitAppearingAfterWarmStart() throws ContradictionException { + int n = 20; + int[] values = {2, 3, 4, 5, 6}; + Model model = new Model(); + IntVar[] vars = new IntVar[n]; + for (int i = 0; i < n; i++) { + vars[i] = model.intVar("v" + i, 1, 6); // nothing forces them off value 1 (yet) + } + IntVar[] cards = model.intVarArray("card", values.length, 0, n, true); + model.globalCardinality(vars, values, cards, false, "AC").post(); + // first propagation: no deficit anywhere, the warm-started matching is free to settle + // every variable on a single value. + model.getSolver().propagate(); + + // raise every listed value's lower bound to 1 at once, as an objective bound tightening + // would: a trivial reassignment (move one variable per value away from value 1) exists + // and must be found. + for (IntVar c : cards) { + c.updateLowerBound(1, Null); + } + model.getSolver().propagate(); // must not fail + for (IntVar c : cards) { + assertTrue(c.getUB() >= 1, c.getName() + " should be able to reach its new minimum"); + } + } + + private void checkAgainstDecomposition(boolean enumerated, boolean closed, boolean extraValues) { + Random random = new Random(); + for (int seed = 0; seed < 100; seed++) { + random.setSeed(seed); + int n = 1 + random.nextInt(6); + int m = 1 + random.nextInt(4); + int[] values = new int[m]; + for (int i = 0; i < values.length; i++) { + values[i] = i; + } + int ub = extraValues ? m + 1 : m - 1; // extra, unrestricted values m..m+1 + + // model under test: GCC with AC filtering + Model model = new Model(SettingsBuilder.init().setCheckDeclaredConstraints(false)); + IntVar[] vars = model.intVarArray("vars", n, 0, ub, !enumerated); + IntVar[] cards = model.intVarArray("cards", m, 0, n, true); + model.globalCardinality(vars, values, cards, closed, "AC").post(); + model.getSolver().setSearch(inputOrderLBSearch(append(vars, cards))); + + // reference model: elementary decomposition + Model ref = new Model(SettingsBuilder.init().setCheckDeclaredConstraints(false)); + IntVar[] refVars = ref.intVarArray("vars", n, 0, ub, !enumerated); + IntVar[] refCards = ref.intVarArray("cards", m, 0, n, true); + reformulate(refVars, refCards, ref).post(); + if (closed) { + for (IntVar v : refVars) { + ref.member(v, values).post(); + } + } + ref.getSolver().setSearch(inputOrderLBSearch(append(refVars, refCards))); + + while (model.getSolver().solve()) { + // enumerate + } + while (ref.getSolver().solve()) { + // enumerate + } + assertEquals(model.getSolver().getSolutionCount(), ref.getSolver().getSolutionCount(), + "seed=" + seed + ", enumerated=" + enumerated + ", closed=" + closed + + ", extraValues=" + extraValues); + } + } + + @Test(groups = "10s", timeOut = 60000, dataProviderClass = Providers.class, dataProvider = "random") + @Providers.Arguments(values = {"1", "50"}) + public void testSameSolutionsDefaultVsBCvsAC(int seed) { + Random random = new Random(seed); + int n = 1 + random.nextInt(6); + int m = 1 + random.nextInt(4); + int[] values = new int[m]; + for (int i = 0; i < values.length; i++) { + values[i] = i; + } + + long[] counts = new long[3]; + String[] modes = {"DEFAULT", "BC", "AC"}; + for (int c = 0; c < modes.length; c++) { + Model model = new Model(SettingsBuilder.init().setCheckDeclaredConstraints(false)); + IntVar[] vars = model.intVarArray("vars", n, 0, m - 1, true); + IntVar[] cards = model.intVarArray("cards", m, 0, n, true); + model.globalCardinality(vars, values, cards, false, modes[c]).post(); + model.getSolver().setSearch(inputOrderLBSearch(append(vars, cards))); + while (model.getSolver().solve()) { + // enumerate + } + counts[c] = model.getSolver().getSolutionCount(); + } + assertEquals(counts[1], counts[0], "BC vs DEFAULT, seed=" + seed); + assertEquals(counts[2], counts[0], "AC vs DEFAULT, seed=" + seed); + } + + @Test(groups = "1s", timeOut = 60000) + public void testUnsat() { + // 5 variables, all forced to take values in {0, 1}, but the total capacity is only 3 + Model model = new Model(); + IntVar[] vars = model.intVarArray("vars", 5, 0, 1, true); + IntVar[] cards = model.intVarArray("cards", 2, 0, 1, true); // sum of upper bounds = 2 < 5 + model.globalCardinality(vars, new int[]{0, 1}, cards, true, "AC").post(); + assertFalse(model.getSolver().solve()); + } + + @Test(groups = "1s", timeOut = 60000, dataProviderClass = Providers.class, dataProvider = "random") + @Providers.Arguments(values = {"1", "50"}) + public void testFixpoint(int seed) throws ContradictionException { + Random random = new Random(seed); + int n = 2 + random.nextInt(8); + int m = 1 + random.nextInt(5); + int[] values = new int[m]; + for (int i = 0; i < values.length; i++) { + values[i] = i; + } + Model model = new Model(); + IntVar[] vars = model.intVarArray("vars", n, 0, m - 1, true); + IntVar[] cards = model.intVarArray("cards", m, 0, n, true); + model.globalCardinality(vars, values, cards, false, "AC").post(); + + // apply a few random domain reductions, then check that a second propagation + // does not change anything anymore (fixpoint reached), as required by + // BEST_PRACTICES.md 3.4. + for (int i = 0; i < n; i++) { + if (random.nextInt(3) == 0) { + int v = values[random.nextInt(m)]; + if (vars[i].contains(v) && vars[i].getDomainSize() > 1) { + vars[i].removeValue(v, Null); + } + } + } + try { + model.getSolver().propagate(); + } catch (ContradictionException e) { + return; // a failure is a valid outcome + } + int[] before = snapshot(vars, cards); + model.getSolver().propagate(); + int[] after = snapshot(vars, cards); + assertEquals(after, before, "seed=" + seed); + } + + private static int[] snapshot(IntVar[] vars, IntVar[] cards) { + IntVar[] all = append(vars, cards); + int[] res = new int[2 * all.length]; + for (int i = 0; i < all.length; i++) { + res[2 * i] = all[i].getLB(); + res[2 * i + 1] = all[i].getUB(); + } + return res; + } +} diff --git a/solver/src/test/java/org/chocosolver/solver/constraints/nary/GlobalCardinalityBCTest.java b/solver/src/test/java/org/chocosolver/solver/constraints/nary/GlobalCardinalityBCTest.java new file mode 100644 index 0000000000..dc754241a9 --- /dev/null +++ b/solver/src/test/java/org/chocosolver/solver/constraints/nary/GlobalCardinalityBCTest.java @@ -0,0 +1,270 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.constraints.nary; + +import org.chocosolver.solver.Model; +import org.chocosolver.solver.Providers; +import org.chocosolver.solver.SettingsBuilder; +import org.chocosolver.solver.exception.ContradictionException; +import org.chocosolver.solver.variables.IntVar; +import org.testng.annotations.Test; + +import java.util.Random; + +import static org.chocosolver.solver.Cause.Null; +import static org.chocosolver.solver.constraints.nary.globalcardinality.GlobalCardinality.reformulate; +import static org.chocosolver.solver.search.strategy.Search.inputOrderLBSearch; +import static org.chocosolver.util.tools.ArrayUtils.append; +import static org.testng.Assert.assertEquals; +import static org.testng.Assert.assertFalse; +import static org.testng.Assert.assertTrue; + +/** + * Tests for the bound-consistency ({@code "BC"}) filtering of the global cardinality constraint, + * i.e. {@link org.chocosolver.solver.constraints.nary.globalcardinality.PropGccBC}. + * + * @author Charles Prud'homme + */ +public class GlobalCardinalityBCTest { + + @Test(groups = "1s", timeOut = 60000) + public void testClosed() throws ContradictionException { + Model model = new Model(); + + IntVar[] vars = model.intVarArray("vars", 6, 0, 3, true); + IntVar[] card = model.intVarArray("card", 4, 0, 6, true); + + int[] values = new int[4]; + for (int i = 0; i < values.length; i++) { + values[i] = i; + } + model.globalCardinality(vars, values, card, true, "BC").post(); + + vars[0].instantiateTo(0, Null); + vars[1].instantiateTo(1, Null); + vars[2].instantiateTo(3, Null); + vars[3].instantiateTo(2, Null); + vars[4].instantiateTo(0, Null); + vars[5].instantiateTo(0, Null); + + model.getSolver().setSearch(inputOrderLBSearch(append(vars, card))); + while (model.getSolver().solve()) { + // enumerate + } + assertTrue(model.getSolver().getSolutionCount() > 0); + } + + @Test(groups = "10s", timeOut = 60000) + public void testRandomBCEnumerated() { + checkAgainstDecomposition(true, false); + } + + @Test(groups = "10s", timeOut = 60000) + public void testRandomBCBounded() { + checkAgainstDecomposition(false, false); + } + + @Test(groups = "10s", timeOut = 60000) + public void testRandomBCClosed() { + checkAgainstDecomposition(true, true); + } + + private void checkAgainstDecomposition(boolean enumerated, boolean closed) { + Random random = new Random(); + for (int seed = 0; seed < 100; seed++) { + random.setSeed(seed); + int n = 1 + random.nextInt(6); + int m = 1 + random.nextInt(4); + int[] values = new int[m]; + for (int i = 0; i < values.length; i++) { + values[i] = i; + } + // model under test: GCC with BC filtering + Model model = new Model(SettingsBuilder.init().setCheckDeclaredConstraints(false)); + IntVar[] vars = model.intVarArray("vars", n, 0, m - 1, !enumerated); + IntVar[] cards = model.intVarArray("cards", m, 0, n, true); + model.globalCardinality(vars, values, cards, closed, "BC").post(); + model.getSolver().setSearch(inputOrderLBSearch(append(vars, cards))); + + // reference model: elementary decomposition + Model ref = new Model(SettingsBuilder.init().setCheckDeclaredConstraints(false)); + IntVar[] refVars = ref.intVarArray("vars", n, 0, m - 1, !enumerated); + IntVar[] refCards = ref.intVarArray("cards", m, 0, n, true); + reformulate(refVars, refCards, ref).post(); + if (closed) { + for (IntVar v : refVars) { + ref.member(v, values).post(); + } + } + ref.getSolver().setSearch(inputOrderLBSearch(append(refVars, refCards))); + + while (model.getSolver().solve()) { + // enumerate + } + while (ref.getSolver().solve()) { + // enumerate + } + assertEquals(model.getSolver().getSolutionCount(), ref.getSolver().getSolutionCount(), + "seed=" + seed + ", enumerated=" + enumerated + ", closed=" + closed); + } + } + + @Test(groups = "10s", timeOut = 60000, dataProviderClass = Providers.class, dataProvider = "random") + @Providers.Arguments(values = {"1", "50"}) + public void testSameSolutionsDefaultVsBC(int seed) { + Random random = new Random(seed); + int n = 1 + random.nextInt(6); + int m = 1 + random.nextInt(4); + int[] values = new int[m]; + for (int i = 0; i < values.length; i++) { + values[i] = i; + } + + Model defaultModel = new Model(SettingsBuilder.init().setCheckDeclaredConstraints(false)); + IntVar[] defaultVars = defaultModel.intVarArray("vars", n, 0, m - 1, true); + IntVar[] defaultCards = defaultModel.intVarArray("cards", m, 0, n, true); + defaultModel.globalCardinality(defaultVars, values, defaultCards, false, "DEFAULT").post(); + defaultModel.getSolver().setSearch(inputOrderLBSearch(append(defaultVars, defaultCards))); + + Model bcModel = new Model(SettingsBuilder.init().setCheckDeclaredConstraints(false)); + IntVar[] bcVars = bcModel.intVarArray("vars", n, 0, m - 1, true); + IntVar[] bcCards = bcModel.intVarArray("cards", m, 0, n, true); + bcModel.globalCardinality(bcVars, values, bcCards, false, "BC").post(); + bcModel.getSolver().setSearch(inputOrderLBSearch(append(bcVars, bcCards))); + + while (defaultModel.getSolver().solve()) { + // enumerate + } + while (bcModel.getSolver().solve()) { + // enumerate + } + assertEquals(bcModel.getSolver().getSolutionCount(), defaultModel.getSolver().getSolutionCount(), + "seed=" + seed); + } + + @Test(groups = "1s", timeOut = 60000) + public void testUnsat() { + // 5 variables, all forced to take values in {0, 1}, but the total capacity is only 3 + Model model = new Model(); + IntVar[] vars = model.intVarArray("vars", 5, 0, 1, true); + IntVar[] cards = model.intVarArray("cards", 2, 0, 1, true); // sum of upper bounds = 2 < 5 + model.globalCardinality(vars, new int[]{0, 1}, cards, true, "BC").post(); + assertFalse(model.getSolver().solve()); + } + + /** + * Regression test: a variable fixed to a value whose maximum occurrence is 0 (all other + * variables free) must be detected as infeasible, not hang. Found via a real FlatZinc + * instance ({@code blocks_16-4-5.fzn}): with several values having {@code maxOcc == 0}, a + * variable landing exactly on a value with an already-exhausted (from initialization, not + * from a decrement) capacity slot made {@code AlgoGccBC}'s union-find structure cycle + * forever in {@code pathset} instead of failing. + */ + @Test(groups = "1s", timeOut = 60000) + public void testForcedValueWithZeroCapacityFailsFast() { + int[] fixedVals = {4, 0, 9, 3, 7, 1, 11, 13, 8, 14, 0, 0, 0, 16, 6, 5}; + int[] minOcc = {4, 1, 0, 1, 1, 1, 0, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1}; + int[] maxOcc = {4, 1, 1, 1, 1, 1, 0, 1, 1, 1, 0, 1, 1, 1, 1, 0, 1}; // value 6: max 0 + int[] values = new int[maxOcc.length]; + for (int i = 0; i < values.length; i++) { + values[i] = i; + } + Model model = new Model(); + IntVar[] vars = new IntVar[fixedVals.length]; + for (int i = 0; i < fixedVals.length; i++) { + vars[i] = model.intVar("v" + i, fixedVals[i]); + } + IntVar[] cards = new IntVar[values.length]; + for (int i = 0; i < values.length; i++) { + cards[i] = model.intVar("c" + i, minOcc[i], maxOcc[i]); + } + model.globalCardinality(vars, values, cards, false, "BC").post(); + // variable 14 is fixed to 6, a value with maxOcc == 0: infeasible. + assertFalse(model.getSolver().solve()); + } + + /** + * Regression test: a run of consecutive values with {@code maxOcc == 0} must not cause BC to + * wrongly declare failure for an unrelated, genuinely feasible, wide-domain variable landing + * on that same (already-exhausted-from-initialization) slot. Found via a real FlatZinc + * instance ({@code handball_handball8.fzn}): the naive fail-fast fix for the hang above + * (failing whenever a capacity slot goes negative) was over-eager and rejected feasible + * states, silently proving a worse "optimum" than {@code "DEFAULT"}/{@code "AC"}. + */ + @Test(groups = "1s", timeOut = 60000) + public void testZeroCapacityRunsDoNotOverFilter() throws ContradictionException { + int[] minOcc = {2, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0, 2, 0, 2, 0, 2, 0, 2, 0, 2}; + int[] maxOcc = {2, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0, 2, 0, 2, 0, 2, 0, 2, 0, 2}; + int[] lb = {9, 9, 9, 9, 9, 9, 0, 0, 9, 0, 9, 0, 9, 0}; + int[] ub = {9, 19, 19, 19, 9, 19, 19, 19, 19, 19, 19, 19, 19, 19}; + int[] values = new int[minOcc.length]; + for (int i = 0; i < values.length; i++) { + values[i] = i; + } + Model model = new Model(); + IntVar[] vars = new IntVar[lb.length]; + for (int i = 0; i < lb.length; i++) { + vars[i] = model.intVar("v" + i, lb[i], ub[i], false); + } + IntVar[] cards = new IntVar[values.length]; + for (int i = 0; i < values.length; i++) { + cards[i] = model.intVar("c" + i, minOcc[i], maxOcc[i]); + } + model.globalCardinality(vars, values, cards, false, "BC").post(); + // must not throw: values 9, 11, 13, 15, 17, 19 each need exactly 2 occurrences (12 + // needed), the 12 free variables (all but v0/v4, already fixed to 9) can cover them. + model.getSolver().propagate(); + } + + @Test(groups = "1s", timeOut = 60000, dataProviderClass = Providers.class, dataProvider = "random") + @Providers.Arguments(values = {"1", "50"}) + public void testFixpoint(int seed) throws ContradictionException { + Random random = new Random(seed); + int n = 2 + random.nextInt(8); + int m = 1 + random.nextInt(5); + boolean bounded = random.nextBoolean(); + int[] values = new int[m]; + for (int i = 0; i < values.length; i++) { + values[i] = i; + } + Model model = new Model(); + IntVar[] vars = model.intVarArray("vars", n, 0, m - 1, bounded); + IntVar[] cards = model.intVarArray("cards", m, 0, n, true); + model.globalCardinality(vars, values, cards, false, "BC").post(); + + // apply a few random domain reductions, then check that a second propagation + // does not change anything anymore (fixpoint reached), as required by + // BEST_PRACTICES.md 3.4. + for (int i = 0; i < n; i++) { + if (random.nextInt(3) == 0) { + int v = values[random.nextInt(m)]; + if (vars[i].contains(v) && vars[i].getDomainSize() > 1) { + vars[i].removeValue(v, Null); + } + } + } + try { + model.getSolver().propagate(); + } catch (ContradictionException e) { + return; // a failure is a valid outcome + } + int[] before = snapshot(vars, cards); + model.getSolver().propagate(); + int[] after = snapshot(vars, cards); + assertEquals(after, before, "seed=" + seed + ", bounded=" + bounded); + } + + private static int[] snapshot(IntVar[] vars, IntVar[] cards) { + IntVar[] all = append(vars, cards); + int[] res = new int[2 * all.length]; + for (int i = 0; i < all.length; i++) { + res[2 * i] = all[i].getLB(); + res[2 * i + 1] = all[i].getUB(); + } + return res; + } +} From fbea0eda690b63eb7001b42d2878a09172538ca5 Mon Sep 17 00:00:00 2001 From: Charles Prud'homme Date: Tue, 29 Sep 2026 09:03:44 +0200 Subject: [PATCH 2/5] Default GlobalCardinality to BC consistency, overridable via property MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Benchmarked across three independent campaigns (macpro, srv/Slurm ×2) on real FlatZinc instances: BC matches AC on solution quality while being algorithmically cheaper, and both markedly outperform the previous DEFAULT (PropFastGCC-only) on tightly-constrained instances -- sometimes by orders of magnitude in nodes explored. Every caller of the 4-arg globalCardinality(...)/GlobalCardinality(...) overload (no explicit consistency string) now gets BC. The choice is centralized in GlobalCardinality.defaultConsistency() and overridable via the choco.gcc.consistency system property, so it can be swapped for benchmarking without touching calling code. --- .../constraints/IIntConstraintFactory.java | 8 +++-- .../globalcardinality/GlobalCardinality.java | 36 ++++++++++++++++++- 2 files changed, 40 insertions(+), 4 deletions(-) diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/IIntConstraintFactory.java b/solver/src/main/java/org/chocosolver/solver/constraints/IIntConstraintFactory.java index cf8f47cbae..6ba0ec8ab6 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/IIntConstraintFactory.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/IIntConstraintFactory.java @@ -1779,8 +1779,9 @@ default Constraint element(IntVar value, IntVar[] table, IntVar index, int offse * Creates a global cardinality constraint (GCC): * Each value values[i] should be taken by exactly occurrences[i] variables of vars. *
- * Uses the {@code "DEFAULT"} consistency level (see - * {@link #globalCardinality(IntVar[], int[], IntVar[], boolean, String)}). + * Uses {@link GlobalCardinality#defaultConsistency()} (see + * {@link #globalCardinality(IntVar[], int[], IntVar[], boolean, String)}) — {@code "BC"} + * unless overridden via the {@value GlobalCardinality#CONSISTENCY_PROPERTY} system property. * * @param vars collection of variables * @param values collection of constrained values @@ -1788,7 +1789,8 @@ default Constraint element(IntVar value, IntVar[] table, IntVar index, int offse * @param closed restricts domains of vars to values if set to true */ default Constraint globalCardinality(IntVar[] vars, int[] values, IntVar[] occurrences, boolean closed) { - return globalCardinality(vars, values, occurrences, closed, "DEFAULT"); + return globalCardinality(vars, values, occurrences, closed, + GlobalCardinality.defaultConsistency().name()); } /** diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/GlobalCardinality.java b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/GlobalCardinality.java index d2984af277..eba241c553 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/GlobalCardinality.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/GlobalCardinality.java @@ -49,8 +49,42 @@ public enum Consistency { AC } + /** + * System property used to override the default {@link Consistency} level, e.g. + * {@code -Dchoco.gcc.consistency=AC}. See {@link #defaultConsistency()}. + */ + public static final String CONSISTENCY_PROPERTY = "choco.gcc.consistency"; + + /** + * Returns the {@link Consistency} level used when none is explicitly specified, e.g. by + * {@link #GlobalCardinality(IntVar[], int[], IntVar[])} or by + * {@link org.chocosolver.solver.constraints.IIntConstraintFactory#globalCardinality(IntVar[], int[], IntVar[], boolean)}. + *

+ * Defaults to {@link Consistency#BC}, which matches or beats {@link Consistency#AC} on + * solution quality while being cheaper to propagate, and both markedly outperform + * {@link Consistency#DEFAULT} on tightly-constrained instances. + *

+ * Can be overridden via the {@value #CONSISTENCY_PROPERTY} system property (e.g. to + * benchmark alternative filtering levels without changing calling code). + * + * @return the default consistency level + * @throws IllegalArgumentException if the {@value #CONSISTENCY_PROPERTY} property is set to + * a value that is not a valid {@link Consistency} name + */ + public static Consistency defaultConsistency() { + return Consistency.valueOf(System.getProperty(CONSISTENCY_PROPERTY, Consistency.BC.name())); + } + + /** + * Creates a global cardinality constraint using the {@linkplain #defaultConsistency() default + * consistency level}. + * + * @param vars collection of variables + * @param values collection of constrained values + * @param cards collection of cardinality variables + */ public GlobalCardinality(IntVar[] vars, int[] values, IntVar[] cards) { - this(vars, values, cards, Consistency.DEFAULT.name()); + this(vars, values, cards, defaultConsistency().name()); } public GlobalCardinality(IntVar[] vars, int[] values, IntVar[] cards, String consistency) { From 4e8ac6179d53e56851d029cf6f56c7c94d96456e Mon Sep 17 00:00:00 2001 From: Charles Prud'homme Date: Tue, 29 Sep 2026 09:03:56 +0200 Subject: [PATCH 3/5] Add GCC to the AC/BC/correctness constraint checkers Modeler.modelGCC_AC/modelGCC_BC mirror the existing modelAllDiffAC/modelAllDiffBC pattern: only the decision variables are exposed to ConsistencyChecker, since PropGccAC/PropGccBC only guarantee their consistency level on decision variables (cardinality variables are left to PropFastGCC's weaker bound reasoning, see PropGccAC's javadoc) -- testing cardinality domains the same way would flag intentional, documented behavior as a false failure. The restricted value set is fixed by the (call-invariant) variable count, never derived from the incoming domains' actual content, since the checker re-invokes the modeler with one variable narrowed to a single value at a time and the constraint being tested must stay the same constraint across those calls. TestConsistency gains testGCC_AC/testGCC_BC; TestCorrectness's existing testGCC() is extended to also check modelGCC_AC/modelGCC_BC against the decomposition. --- .../solver/constraints/checker/Modeler.java | 63 +++++++++++++++++++ .../checker/consistency/TestConsistency.java | 24 +++++++ .../checker/correctness/TestCorrectness.java | 2 + 3 files changed, 89 insertions(+) diff --git a/solver/src/test/java/org/chocosolver/solver/constraints/checker/Modeler.java b/solver/src/test/java/org/chocosolver/solver/constraints/checker/Modeler.java index 9fb7441b9f..eea0f31bdf 100644 --- a/solver/src/test/java/org/chocosolver/solver/constraints/checker/Modeler.java +++ b/solver/src/test/java/org/chocosolver/solver/constraints/checker/Modeler.java @@ -204,6 +204,69 @@ public String name() { } }; + // GCC's AC/BC propagator only filters the decision variables to the given consistency level + // (cardinality variables are left to PropFastGCC's weaker bound reasoning -- see + // PropGccAC's javadoc), so only the decision variables are exposed/mapped for testing here. + // `values` = [0, n-1] is fixed by the (structural, call-invariant) nbVar parameter, never + // derived from the incoming domains' actual content: the checker re-invokes model() with a + // single variable narrowed to one value at a time, and `values` must stay the SAME restricted + // set across every one of those calls for the check to mean anything. Tests are run with + // lowerB=0 so generated domains fall inside/around this range; any value >= n acts as a + // genuine escape value (forbidden when closed, free/untracked otherwise). + Modeler modelGCC_AC = new Modeler() { + @Override + public Model model(int n, int[][] domains, THashMap map, Object parameters) { + Model s = new Model("GCC_AC_" + n); + boolean closed = (Boolean) parameters; + IntVar[] vars = new IntVar[n]; + for (int i = 0; i < n; i++) { + vars[i] = s.intVar("v_" + i, domains[i]); + if (map != null) map.put(domains[i], vars[i]); + } + int[] values = new int[n]; + IntVar[] cards = new IntVar[n]; + for (int i = 0; i < n; i++) { + values[i] = i; + cards[i] = s.intVar("c_" + i, 0, n, true); + } + s.globalCardinality(vars, values, cards, closed, "AC").post(); + s.getSolver().setSearch(randomSearch(vars, 0)); + return s; + } + + @Override + public String name() { + return "modelGCC_AC"; + } + }; + + Modeler modelGCC_BC = new Modeler() { + @Override + public Model model(int n, int[][] domains, THashMap map, Object parameters) { + Model s = new Model("GCC_BC_" + n); + boolean closed = (Boolean) parameters; + IntVar[] vars = new IntVar[n]; + for (int i = 0; i < n; i++) { + vars[i] = s.intVar("v_" + i, domains[i][0], domains[i][domains[i].length - 1], true); + if (map != null) map.put(domains[i], vars[i]); + } + int[] values = new int[n]; + IntVar[] cards = new IntVar[n]; + for (int i = 0; i < n; i++) { + values[i] = i; + cards[i] = s.intVar("c_" + i, 0, n, true); + } + s.globalCardinality(vars, values, cards, closed, "BC").post(); + s.getSolver().setSearch(randomSearch(vars, 0)); + return s; + } + + @Override + public String name() { + return "modelGCC_BC"; + } + }; + Modeler modelTimes = new Modeler() { @Override public Model model(int n, int[][] domains, THashMap map, Object parameters) { diff --git a/solver/src/test/java/org/chocosolver/solver/constraints/checker/consistency/TestConsistency.java b/solver/src/test/java/org/chocosolver/solver/constraints/checker/consistency/TestConsistency.java index 67f0df2076..a7ba3ea529 100644 --- a/solver/src/test/java/org/chocosolver/solver/constraints/checker/consistency/TestConsistency.java +++ b/solver/src/test/java/org/chocosolver/solver/constraints/checker/consistency/TestConsistency.java @@ -75,6 +75,30 @@ public void testALLDIFFERENTBC() { } } + // GlobalCardinality ******************************************************* + + @Test(groups="checker", timeOut=60000) + public void testGCC_AC() { + long seed = System.currentTimeMillis(); + for (int i = 0; i < 20; i++) { + for (int n = 2; n < (1 << 3) + 1; n *= 2) { + checkConsistency(Modeler.modelGCC_AC, n, 0, n, true, seed + i, "ac"); + checkConsistency(Modeler.modelGCC_AC, n, 0, n, false, seed + i, "ac"); + } + } + } + + @Test(groups="checker", timeOut=60000) + public void testGCC_BC() { + long seed = System.currentTimeMillis(); + for (int i = 0; i < 10; i++) { + for (int n = 2; n < (1 << 4) + 1; n *= 2) { + checkConsistency(Modeler.modelGCC_BC, n, 0, n, true, seed + i, "bc"); + checkConsistency(Modeler.modelGCC_BC, n, 0, n, false, seed + i, "bc"); + } + } + } + // Absolute ******************************************************* @Test(groups="checker", timeOut=60000) diff --git a/solver/src/test/java/org/chocosolver/solver/constraints/checker/correctness/TestCorrectness.java b/solver/src/test/java/org/chocosolver/solver/constraints/checker/correctness/TestCorrectness.java index 1b5bd27f6b..3fb97a8d7f 100644 --- a/solver/src/test/java/org/chocosolver/solver/constraints/checker/correctness/TestCorrectness.java +++ b/solver/src/test/java/org/chocosolver/solver/constraints/checker/correctness/TestCorrectness.java @@ -99,6 +99,8 @@ public void testGCC() { long seed = System.currentTimeMillis(); for (int n = 2; n < (1 << 5) + 1; n *= 2) { CorrectnessChecker.checkCorrectness(Modeler.modelGCC, n, 0, n, seed, true); + CorrectnessChecker.checkCorrectness(Modeler.modelGCC_BC, n, 0, n, seed, true); + CorrectnessChecker.checkCorrectness(Modeler.modelGCC_AC, n, 0, n, seed, true); CorrectnessChecker.checkCorrectness(Modeler.modelGCC_alldiff, n, -n / 2, 2 * n, seed, false); } } From 3a6a377815584fd1c48db5d9e9447f9d038da5b6 Mon Sep 17 00:00:00 2001 From: Charles Prud'homme Date: Tue, 29 Sep 2026 12:52:17 +0200 Subject: [PATCH 4/5] Update parser performance test expectations for GCC BC default Switching GlobalCardinality's default consistency to BC changes the search statistics (nodes/fails) of the test instances relying on GCC. Solution counts and best values are unchanged. --- parsers/src/test/resources/flatzinc/hard_instances.csv | 2 +- parsers/src/test/resources/xcsp/instances.csv | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/parsers/src/test/resources/flatzinc/hard_instances.csv b/parsers/src/test/resources/flatzinc/hard_instances.csv index a667334ba2..b9a6ada39c 100644 --- a/parsers/src/test/resources/flatzinc/hard_instances.csv +++ b/parsers/src/test/resources/flatzinc/hard_instances.csv @@ -1,7 +1,7 @@ #year,name,solutions,best,nodes,fails 2020,skill_allocation+mzn_1m_1.fzn,1,2,6196,6195 2020,stable-goods-solution+s-d6.fzn,13,6264,146933,146908 -2018,rotating-workforce+ex1479.fzn,1,_,125855,125753 +2018,rotating-workforce+ex1479.fzn,1,_,125773,125671 2016,tpp+6_3_20_1.fzn,65,131,2813024,2812895 2012,still-life-wastage+still-life+09.fzn,5,43,109471,109462 2012,still-life-wastage+still-life+10.fzn,7,54,164574,164561 diff --git a/parsers/src/test/resources/xcsp/instances.csv b/parsers/src/test/resources/xcsp/instances.csv index 2f3932fd9a..2246427a6a 100644 --- a/parsers/src/test/resources/xcsp/instances.csv +++ b/parsers/src/test/resources/xcsp/instances.csv @@ -74,9 +74,9 @@ basics;Ramsey-12.xml.lzma;54;2;57445;33115 basics;Rcpsp-j30-01-01_c18.xml.lzma;7;43;199;162 basics;Rlfap-graph-04-opt_c18.xml.lzma;10;394;2651;1656 basics;RoomMate-sr0050-int.xml.lzma;1;_;2;0 -basics;SocialGolfers-4-3-4-cp.xml.lzma;1;_;249;177 +basics;SocialGolfers-4-3-4-cp.xml.lzma;1;_;227;161 #basics;Sonet-s2ring02.xml.lzma;9;14;815744;621835 -basics;SportsScheduling-08.xml.lzma;1;_;210;168 +basics;SportsScheduling-08.xml.lzma;1;_;181;150 basics;SteelMillSlab-m1-simple_c18.xml.lzma;4;0;221;180 basics;SteelMillSlab-m2-simple_c18.xml.lzma;2;0;228;196 basics;SteelMillSlab-m2s-mini-simple_c18.xml.lzma;1;0;127;50 @@ -99,6 +99,6 @@ basics;testObjective1.xml.lzma;2;11;8;5 basics;testPrimitive.xml.lzma;1;_;3;1 #basics;TestSchedulingM18-t30m10r3-15.xml.lzma;93;4149;3450;2650 basics;Tpp-3-3-20-1.xml.lzma;9;126;273;217 -basics;TravelingTournament-a3-galaxy04_c18.xml.lzma;6;416;3765;3425 +basics;TravelingTournament-a3-galaxy04_c18.xml.lzma;6;416;3693;3378 basics;Warehouse-opl.xml.lzma;19;383;130;90 basics;Zebra.xml.lzma;1;_;9;2 \ No newline at end of file From c642da11a5c1766e39ac3b97da027c6914385ce6 Mon Sep 17 00:00:00 2001 From: Charles Prud'homme Date: Wed, 30 Sep 2026 15:04:57 +0200 Subject: [PATCH 5/5] Merge PropGccBC/PropGccAC into a single PropGcc propagator Both propagators shared an identical propagate() (dense minOcc/maxOcc construction), a near-identical constructor, isEntailed() and toString(); the only real differences were the PropagatorPriority, the filtering algorithm, and the propagation conditions. Introduce a GccFilter interface implemented by AlgoGccBC/AlgoGccAC, and collapse the two propagators into one PropGcc class parameterized by GlobalCardinality.Consistency (BC/AC), which now decides the priority, the algorithm, and getPropagationConditions from that single field. --- .../globalcardinality/GlobalCardinality.java | 8 +- .../{PropGccBC.java => PropGcc.java} | 56 +++++++-- .../nary/globalcardinality/PropGccAC.java | 112 ------------------ .../globalcardinality/algo/AlgoGccAC.java | 4 +- .../globalcardinality/algo/AlgoGccBC.java | 4 +- .../globalcardinality/algo/GccFilter.java | 34 ++++++ .../solver/constraints/checker/Modeler.java | 2 +- .../nary/GlobalCardinalityACTest.java | 3 +- .../nary/GlobalCardinalityBCTest.java | 3 +- 9 files changed, 91 insertions(+), 135 deletions(-) rename solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/{PropGccBC.java => PropGcc.java} (56%) delete mode 100644 solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/PropGccAC.java create mode 100644 solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/GccFilter.java diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/GlobalCardinality.java b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/GlobalCardinality.java index eba241c553..45f76582d9 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/GlobalCardinality.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/GlobalCardinality.java @@ -36,14 +36,14 @@ public enum Consistency { */ DEFAULT, /** - * Bound-consistency (see {@link PropGccBC}), following: + * Bound-consistency (see {@link PropGcc}), following: * C.-G. Quimper, P. van Beek, A. Lopez-Ortiz, A. Golynski, and S.B. Sadjad. * "An efficient bounds consistency algorithm for the global cardinality constraint." * CP-2003. */ BC, /** - * Arc-consistency (see {@link PropGccAC}), following: + * Arc-consistency (see {@link PropGcc}), following: * J.-C. Regin. "Generalized Arc Consistency for Global Cardinality Constraint." AAAI-96. */ AC @@ -107,11 +107,9 @@ private static Propagator[] createProp(IntVar[] vars, int[] values, IntV PropFastGCC fast = new PropFastGCC(vars, values, map, cards); switch (consistency) { case BC: - //noinspection unchecked - return new Propagator[]{fast, new PropGccBC(vars, values, cards)}; case AC: //noinspection unchecked - return new Propagator[]{fast, new PropGccAC(vars, values, cards)}; + return new Propagator[]{fast, new PropGcc(vars, values, cards, consistency)}; default: //noinspection unchecked return new Propagator[]{fast}; diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/PropGccBC.java b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/PropGcc.java similarity index 56% rename from solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/PropGccBC.java rename to solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/PropGcc.java index 74a101a863..090ff5eb9a 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/PropGccBC.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/PropGcc.java @@ -8,7 +8,10 @@ import org.chocosolver.solver.constraints.Propagator; import org.chocosolver.solver.constraints.PropagatorPriority; +import org.chocosolver.solver.constraints.nary.globalcardinality.GlobalCardinality.Consistency; +import org.chocosolver.solver.constraints.nary.globalcardinality.algo.AlgoGccAC; import org.chocosolver.solver.constraints.nary.globalcardinality.algo.AlgoGccBC; +import org.chocosolver.solver.constraints.nary.globalcardinality.algo.GccFilter; import org.chocosolver.solver.exception.ContradictionException; import org.chocosolver.solver.variables.IntVar; import org.chocosolver.solver.variables.events.IntEventType; @@ -18,17 +21,26 @@ import java.util.Arrays; /** - * Bound-consistency propagator for the Global Cardinality Constraint (GCC), based on: - * C.-G. Quimper, P. van Beek, A. Lopez-Ortiz, A. Golynski, and S.B. Sadjad. - * "An efficient bounds consistency algorithm for the global cardinality constraint." CP-2003. + * Consistency propagator for the Global Cardinality Constraint (GCC), enforcing either: + *

+ * The two levels only differ in which {@link GccFilter} drives {@link #propagate(int)}, at which + * {@link PropagatorPriority}, and in which domain events wake this propagator up + * ({@link #getPropagationConditions(int)}); everything else, including the construction of the + * dense per-value occurrence bounds consumed by the filter, is shared. *

- * Meant to be posted alongside {@link PropFastGCC}, which is left in charge of tightening - * the bounds of the cardinality variables and of the soundness/completeness of the constraint; - * this propagator only brings bound-consistency on the decision variables. + * Meant to be posted alongside {@link PropFastGCC}, which is left in charge of tightening the + * bounds of the cardinality variables and of the soundness/completeness of the constraint; this + * propagator only brings its consistency level on the decision variables. * * @author Charles Prud'homme */ -public class PropGccBC extends Propagator { +public class PropGcc extends Propagator { //*********************************************************************************** // VARIABLES @@ -37,7 +49,8 @@ public class PropGccBC extends Propagator { private final int n; private final int n2; private final int[] values; - private final AlgoGccBC filter; + private final GccFilter filter; + private final Consistency consistency; //*********************************************************************************** // CONSTRUCTORS @@ -47,16 +60,31 @@ public class PropGccBC extends Propagator { * @param decvars array of decision variables * @param restrictedValues array of restricted values * @param valueCardinalities array of cardinality variables, one per restricted value + * @param consistency consistency level to enforce, {@link Consistency#BC} or + * {@link Consistency#AC} */ - public PropGccBC(IntVar[] decvars, int[] restrictedValues, IntVar[] valueCardinalities) { - super(ArrayUtils.append(decvars, valueCardinalities), PropagatorPriority.LINEAR, false); + public PropGcc(IntVar[] decvars, int[] restrictedValues, IntVar[] valueCardinalities, + Consistency consistency) { + super(ArrayUtils.append(decvars, valueCardinalities), priorityOf(consistency), false); this.values = restrictedValues; this.n = decvars.length; this.n2 = values.length; - this.filter = new AlgoGccBC(this); + this.consistency = consistency; + this.filter = switch (consistency) { + case BC -> new AlgoGccBC(this); + case AC -> new AlgoGccAC(this); + case DEFAULT -> throw new IllegalArgumentException( + "PropGcc only supports Consistency.BC or Consistency.AC, not DEFAULT " + + "(handled by PropFastGCC alone)"); + }; filter.reset(decvars); } + private static PropagatorPriority priorityOf(Consistency consistency) { + // BC (Quimper et al.) is near-linear; AC (Regin) rebuilds/repairs a flow, quadratic-ish. + return consistency == Consistency.BC ? PropagatorPriority.LINEAR : PropagatorPriority.QUADRATIC; + } + //*********************************************************************************** // PROPAGATION //*********************************************************************************** @@ -93,7 +121,9 @@ public void propagate(int evtmask) throws ContradictionException { @Override public int getPropagationConditions(int vIdx) { - return IntEventType.boundAndInst(); + // BC (Quimper et al.) only reasons on bounds; AC needs fine domain events to be sound + // on enumerated domains, so it keeps the default (all events). + return consistency == Consistency.BC ? IntEventType.boundAndInst() : super.getPropagationConditions(vIdx); } @Override @@ -104,7 +134,7 @@ public ESat isEntailed() { @Override public String toString() { StringBuilder st = new StringBuilder(); - st.append("PropGccBC_("); + st.append("PropGcc_").append(consistency).append("_("); int i = 0; for (; i < Math.min(4, vars.length); i++) { st.append(vars[i].getName()).append(", "); diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/PropGccAC.java b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/PropGccAC.java deleted file mode 100644 index 9b5e57701b..0000000000 --- a/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/PropGccAC.java +++ /dev/null @@ -1,112 +0,0 @@ -/* - * This file is part of choco-solver, http://choco-solver.org/ - * Copyright (c) 1999, IMT Atlantique. - * SPDX-License-Identifier: BSD-3-Clause. - * See LICENSE file in the project root for full license information. - */ -package org.chocosolver.solver.constraints.nary.globalcardinality; - -import org.chocosolver.solver.constraints.Propagator; -import org.chocosolver.solver.constraints.PropagatorPriority; -import org.chocosolver.solver.constraints.nary.globalcardinality.algo.AlgoGccAC; -import org.chocosolver.solver.exception.ContradictionException; -import org.chocosolver.solver.variables.IntVar; -import org.chocosolver.util.ESat; -import org.chocosolver.util.tools.ArrayUtils; - -import java.util.Arrays; - -/** - * Arc-consistency propagator for the Global Cardinality Constraint (GCC), based on: - * J.-C. Regin. "Generalized Arc Consistency for Global Cardinality Constraint." AAAI-96. - *

- * Meant to be posted alongside {@link PropFastGCC}, which is left in charge of tightening the - * bounds of the cardinality variables and of the soundness/completeness of the constraint; this - * propagator only brings arc-consistency on the decision variables. - * - * @author Charles Prud'homme - */ -public class PropGccAC extends Propagator { - - //*********************************************************************************** - // VARIABLES - //*********************************************************************************** - - private final int n; - private final int n2; - private final int[] values; - private final AlgoGccAC filter; - - //*********************************************************************************** - // CONSTRUCTORS - //*********************************************************************************** - - /** - * @param decvars array of decision variables - * @param restrictedValues array of restricted values - * @param valueCardinalities array of cardinality variables, one per restricted value - */ - public PropGccAC(IntVar[] decvars, int[] restrictedValues, IntVar[] valueCardinalities) { - super(ArrayUtils.append(decvars, valueCardinalities), PropagatorPriority.QUADRATIC, false); - this.values = restrictedValues; - this.n = decvars.length; - this.n2 = values.length; - this.filter = new AlgoGccAC(this); - filter.reset(decvars); - } - - //*********************************************************************************** - // PROPAGATION - //*********************************************************************************** - - @Override - public void propagate(int evtmask) throws ContradictionException { - int gMin = Integer.MAX_VALUE; - int gMax = Integer.MIN_VALUE; - for (int i = 0; i < n; i++) { - gMin = Math.min(gMin, vars[i].getLB()); - gMax = Math.max(gMax, vars[i].getUB()); - } - for (int v : values) { - gMin = Math.min(gMin, v); - gMax = Math.max(gMax, v); - } - int range = gMax - gMin + 1; - int[] minOcc = new int[range]; - int[] maxOcc = new int[range]; - // values out of the restricted list are unconstrained: [0, n] - Arrays.fill(maxOcc, n); - for (int i = 0; i < n2; i++) { - IntVar card = vars[n + i]; - int idx = values[i] - gMin; - minOcc[idx] = card.getLB(); - maxOcc[idx] = card.getUB(); - } - filter.filter(minOcc, maxOcc, gMin); - } - - //*********************************************************************************** - // INFO - //*********************************************************************************** - - @Override - public ESat isEntailed() { - return ESat.TRUE; // redundant propagator, PropFastGCC already checks correctness - } - - @Override - public String toString() { - StringBuilder st = new StringBuilder(); - st.append("PropGccAC_("); - int i = 0; - for (; i < Math.min(4, vars.length); i++) { - st.append(vars[i].getName()).append(", "); - } - if (i < vars.length - 2) { - st.append("...,"); - } - st.append(vars[vars.length - 1].getName()).append(")"); - return st.toString(); - } - -} diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/AlgoGccAC.java b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/AlgoGccAC.java index 0bf6583a8c..63c30265b4 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/AlgoGccAC.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/AlgoGccAC.java @@ -35,7 +35,7 @@ * * @author Charles Prud'homme */ -public class AlgoGccAC { +public class AlgoGccAC implements GccFilter { private static final int UNMATCHED = -1; private static final int FROM_SOURCE = -2; @@ -74,6 +74,7 @@ public AlgoGccAC(Propagator cause) { this.aCause = cause; } + @Override public void reset(IntVar[] variables) { this.vars = variables; this.n = vars.length; @@ -96,6 +97,7 @@ public void reset(IntVar[] variables) { * @param firstValue first value of the range covered by {@code minOcc}/{@code maxOcc} * @return {@code true} iff at least one domain update has been done */ + @Override public boolean filter(int[] minOcc, int[] maxOcc, int firstValue) throws ContradictionException { this.minOcc = minOcc; this.maxOcc = maxOcc; diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/AlgoGccBC.java b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/AlgoGccBC.java index e3cf0407dc..755326b0d4 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/AlgoGccBC.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/AlgoGccBC.java @@ -21,7 +21,7 @@ * * @author Charles Prud'homme */ -public class AlgoGccBC { +public class AlgoGccBC implements GccFilter { private final Propagator aCause; private IntVar[] vars; @@ -51,6 +51,7 @@ public AlgoGccBC(Propagator cause) { this.aCause = cause; } + @Override public void reset(IntVar[] variables) { this.vars = variables; this.n = vars.length; @@ -91,6 +92,7 @@ public void reset(IntVar[] variables) { * @param firstValue first value of the range covered by {@code minOcc}/{@code maxOcc} * @return {@code true} iff at least one bound update has been done */ + @Override public boolean filter(int[] minOcc, int[] maxOcc, int firstValue) throws ContradictionException { int range = minOcc.length; PartialSum l = new PartialSum(firstValue, range, minOcc); diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/GccFilter.java b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/GccFilter.java new file mode 100644 index 0000000000..c4793b569a --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/GccFilter.java @@ -0,0 +1,34 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.constraints.nary.globalcardinality.algo; + +import org.chocosolver.solver.exception.ContradictionException; +import org.chocosolver.solver.variables.IntVar; + +/** + * Common shape of the two consistency algorithms posted for the Global Cardinality Constraint + * ({@link AlgoGccBC}, {@link AlgoGccAC}), so that {@code PropGcc} can drive either one without + * knowing which consistency level it enforces. + * + * @author Charles Prud'homme + */ +public interface GccFilter { + + /** + * (Re)initializes the algorithm's internal structures for the current array of decision + * variables. Called once per propagator construction. + */ + void reset(IntVar[] variables); + + /** + * Filters the decision variables to (bound- or arc-) consistency, given the current bounds + * on the occurrence count of every value in {@code [firstValue, firstValue + minOcc.length)}. + * + * @return {@code true} if at least one variable was filtered + */ + boolean filter(int[] minOcc, int[] maxOcc, int firstValue) throws ContradictionException; +} diff --git a/solver/src/test/java/org/chocosolver/solver/constraints/checker/Modeler.java b/solver/src/test/java/org/chocosolver/solver/constraints/checker/Modeler.java index eea0f31bdf..cc67b50890 100644 --- a/solver/src/test/java/org/chocosolver/solver/constraints/checker/Modeler.java +++ b/solver/src/test/java/org/chocosolver/solver/constraints/checker/Modeler.java @@ -206,7 +206,7 @@ public String name() { // GCC's AC/BC propagator only filters the decision variables to the given consistency level // (cardinality variables are left to PropFastGCC's weaker bound reasoning -- see - // PropGccAC's javadoc), so only the decision variables are exposed/mapped for testing here. + // PropGcc's javadoc), so only the decision variables are exposed/mapped for testing here. // `values` = [0, n-1] is fixed by the (structural, call-invariant) nbVar parameter, never // derived from the incoming domains' actual content: the checker re-invokes model() with a // single variable narrowed to one value at a time, and `values` must stay the SAME restricted diff --git a/solver/src/test/java/org/chocosolver/solver/constraints/nary/GlobalCardinalityACTest.java b/solver/src/test/java/org/chocosolver/solver/constraints/nary/GlobalCardinalityACTest.java index d602012d7b..81c350dd33 100644 --- a/solver/src/test/java/org/chocosolver/solver/constraints/nary/GlobalCardinalityACTest.java +++ b/solver/src/test/java/org/chocosolver/solver/constraints/nary/GlobalCardinalityACTest.java @@ -26,7 +26,8 @@ /** * Tests for the arc-consistency ({@code "AC"}) filtering of the global cardinality constraint, - * i.e. {@link org.chocosolver.solver.constraints.nary.globalcardinality.PropGccAC}. + * i.e. {@link org.chocosolver.solver.constraints.nary.globalcardinality.PropGcc} with + * {@link org.chocosolver.solver.constraints.nary.globalcardinality.GlobalCardinality.Consistency#AC}. * * @author Charles Prud'homme */ diff --git a/solver/src/test/java/org/chocosolver/solver/constraints/nary/GlobalCardinalityBCTest.java b/solver/src/test/java/org/chocosolver/solver/constraints/nary/GlobalCardinalityBCTest.java index dc754241a9..10353fcc7a 100644 --- a/solver/src/test/java/org/chocosolver/solver/constraints/nary/GlobalCardinalityBCTest.java +++ b/solver/src/test/java/org/chocosolver/solver/constraints/nary/GlobalCardinalityBCTest.java @@ -25,7 +25,8 @@ /** * Tests for the bound-consistency ({@code "BC"}) filtering of the global cardinality constraint, - * i.e. {@link org.chocosolver.solver.constraints.nary.globalcardinality.PropGccBC}. + * i.e. {@link org.chocosolver.solver.constraints.nary.globalcardinality.PropGcc} with + * {@link org.chocosolver.solver.constraints.nary.globalcardinality.GlobalCardinality.Consistency#BC}. * * @author Charles Prud'homme */