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 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..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,7 +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. *
- * This constraint does not ensure any well-defined level of consistency, yet. + * 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 @@ -1787,6 +1789,41 @@ 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, + GlobalCardinality.defaultConsistency().name()); + } + + /** + * 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 +1864,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..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 @@ -25,11 +25,74 @@ */ 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 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 PropGcc}), following: + * J.-C. Regin. "Generalized Arc Consistency for Global Cardinality Constraint." AAAI-96. + */ + 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) { - super(ConstraintsName.GCC, createProp(vars, values, cards)); + this(vars, values, cards, defaultConsistency().name()); + } + + 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) { + 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 +104,16 @@ 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: + case AC: + //noinspection unchecked + return new Propagator[]{fast, new PropGcc(vars, values, cards, consistency)}; + 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/PropGcc.java b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/PropGcc.java new file mode 100644 index 0000000000..090ff5eb9a --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/PropGcc.java @@ -0,0 +1,149 @@ +/* + * 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.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; +import org.chocosolver.util.ESat; +import org.chocosolver.util.tools.ArrayUtils; + +import java.util.Arrays; + +/** + * 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 its consistency level on the decision variables. + * + * @author Charles Prud'homme + */ +public class PropGcc extends Propagator { + + //*********************************************************************************** + // VARIABLES + //*********************************************************************************** + + private final int n; + private final int n2; + private final int[] values; + private final GccFilter filter; + private final Consistency consistency; + + //*********************************************************************************** + // CONSTRUCTORS + //*********************************************************************************** + + /** + * @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 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.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 + //*********************************************************************************** + + @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) { + // 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 + public ESat isEntailed() { + return ESat.TRUE; // redundant propagator, PropFastGCC already checks correctness + } + + @Override + public String toString() { + StringBuilder st = new StringBuilder(); + st.append("PropGcc_").append(consistency).append("_("); + 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..63c30265b4 --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/AlgoGccAC.java @@ -0,0 +1,359 @@ +/* + * 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 implements GccFilter { + + 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; + } + + @Override + 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 + */ + @Override + 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..755326b0d4 --- /dev/null +++ b/solver/src/main/java/org/chocosolver/solver/constraints/nary/globalcardinality/algo/AlgoGccBC.java @@ -0,0 +1,531 @@ +/* + * 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 implements GccFilter { + + 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; + } + + @Override + 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 + */ + @Override + 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/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 9fb7441b9f..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 @@ -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 + // 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 + // 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); } } 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..81c350dd33 --- /dev/null +++ b/solver/src/test/java/org/chocosolver/solver/constraints/nary/GlobalCardinalityACTest.java @@ -0,0 +1,319 @@ +/* + * 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.PropGcc} with + * {@link org.chocosolver.solver.constraints.nary.globalcardinality.GlobalCardinality.Consistency#AC}. + * + * @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..10353fcc7a --- /dev/null +++ b/solver/src/test/java/org/chocosolver/solver/constraints/nary/GlobalCardinalityBCTest.java @@ -0,0 +1,271 @@ +/* + * 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.PropGcc} with + * {@link org.chocosolver.solver.constraints.nary.globalcardinality.GlobalCardinality.Consistency#BC}. + * + * @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; + } +}