From d11b7de46697fb1150b43e2bcf1d08646ab397a5 Mon Sep 17 00:00:00 2001 From: Arthur Godet Date: Tue, 2 Aug 2022 23:00:39 +0200 Subject: [PATCH 1/6] fix citation for AllDiffPrecMoreThanBc.java --- .../nary/alldifferentprec/AllDiffPrecMoreThanBc.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/nary/alldifferentprec/AllDiffPrecMoreThanBc.java b/solver/src/main/java/org/chocosolver/solver/constraints/nary/alldifferentprec/AllDiffPrecMoreThanBc.java index f85d970de9..5d8f8a2d58 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/nary/alldifferentprec/AllDiffPrecMoreThanBc.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/nary/alldifferentprec/AllDiffPrecMoreThanBc.java @@ -31,7 +31,7 @@ /** * Filtering algorithm for the AllDiffPrec constraint introduced in the following thesis : - * TODO: add the thesis citation when it is fixed (and/or the CP paper if accepted) + * Godet, A.: On the use of tasks ordering to solve scheduling problems with constraint programming. Thesis dissertation, 2021. * * @author Arthur Godet */ From 5b7b50f206089c52daf6ab7d59b1b9829e5a6bda Mon Sep 17 00:00:00 2001 From: Jean-Guillaume Fages Date: Fri, 21 Jul 2023 17:55:18 +0200 Subject: [PATCH 2/6] use square when possible and stronger filtering practical interest to be confirmed by experiments --- .../constraints/IIntConstraintFactory.java | 4 +- .../solver/constraints/binary/PropSquare.java | 44 ++++++++++--------- 2 files changed, 26 insertions(+), 22 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 e857536d7b..fc844e9b25 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/IIntConstraintFactory.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/IIntConstraintFactory.java @@ -736,7 +736,9 @@ default Constraint mod(IntVar X, IntVar Y, IntVar Z) { */ @SuppressWarnings("SuspiciousNameCombination") default Constraint times(IntVar X, IntVar Y, IntVar Z) { - if (Y.isInstantiated()) { + if (X == Y) { + return square(Z, X); + } else if (Y.isInstantiated()) { return times(X, Y.getValue(), Z); } else if (X.isInstantiated()) { return times(Y, X.getValue(), Z); diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropSquare.java b/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropSquare.java index 1daf550ad1..00aa828474 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropSquare.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropSquare.java @@ -117,7 +117,6 @@ protected void updateLowerBoundofX() throws ContradictionException { protected void updateUpperBoundofX() throws ContradictionException { vars[0].updateUpperBound(Math.max(sqr(vars[1].getLB()), sqr(vars[1].getUB())), this); - } protected boolean updateHolesinX() throws ContradictionException { @@ -158,7 +157,11 @@ protected boolean updateHolesinX() throws ContradictionException { } protected boolean updateLowerBoundofY() throws ContradictionException { - return vars[1].updateLowerBound(-ceil_sqrt(vars[0].getUB()), this); + if (vars[1].getLB() >= 0) { + return vars[1].updateLowerBound(ceil_sqrt(vars[0].getLB()), this); + } else { + return vars[1].updateLowerBound(-floor_sqrt(vars[0].getUB()), this); + } } protected boolean updateUpperBoundofY() throws ContradictionException { @@ -166,8 +169,19 @@ protected boolean updateUpperBoundofY() throws ContradictionException { } protected boolean updateHolesinY() throws ContradictionException { - // remove intervals to deal with consecutive value removal and upper bound modification - if (bothEnum) { + if (vars[0].isInstantiatedTo(0)) { + return vars[1].instantiateTo(0, this); + } + boolean impact = false; + // remove interval around 0 based on X LB + if (vars[1].hasEnumeratedDomain()) { + int val = ceil_sqrt(vars[0].getLB()) - 1; + if (val >= 0) { + impact = vars[1].removeInterval(-val, val, this); + } + } + // remove values based on X holes + if (bothEnum && hasHoles(vars[0])) { int ub = vars[1].getUB(); vrms.clear(); vrms.setOffset(vars[1].getLB()); @@ -176,24 +190,12 @@ protected boolean updateHolesinY() throws ContradictionException { vrms.add(value); } } - return vars[1].removeValues(vrms, this); - } else if (vars[1].hasEnumeratedDomain()) { - int lb = vars[1].getLB(); - int ub = vars[1].getUB(); - while (!vars[0].contains(sqr(lb))) { - lb = vars[1].nextValue(lb); - if (lb > ub) break; - } - boolean filter = vars[1].updateLowerBound(lb, this); - - while (!vars[0].contains(sqr(ub))) { - ub = vars[1].nextValue(ub); - if (ub < lb) break; - } - return filter | vars[1].updateUpperBound(ub, this); + impact |= vars[1].removeValues(vrms, this); } - return false; + return impact; } - + private boolean hasHoles(IntVar var) { + return (var.getUB() - var.getLB() + 1) > var.getDomainSize(); + } } From 7701fe8916aef448eb382f2e4c113ed5086baf75 Mon Sep 17 00:00:00 2001 From: Jean-Guillaume Fages Date: Mon, 24 Jul 2023 22:42:15 +0200 Subject: [PATCH 3/6] propsquare filtering + test --- .../solver/constraints/binary/PropSquare.java | 31 +++++------ .../solver/constraints/binary/SquareTest.java | 51 +++++++++++++++++++ 2 files changed, 64 insertions(+), 18 deletions(-) diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropSquare.java b/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropSquare.java index 00aa828474..0aad53d61f 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropSquare.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropSquare.java @@ -57,22 +57,11 @@ public void propagate(int evtmask) throws ContradictionException { public ESat isEntailed() { if (vars[0].getUB() < 0) { return ESat.FALSE; - } else if (vars[0].isInstantiated()) { - if (vars[1].isInstantiated()) { - return ESat.eval(vars[0].getValue() == sqr(vars[1].getValue())); - } else if (vars[1].getDomainSize() == 2 && - vars[1].contains(-floor_sqrt(vars[0].getValue())) && - vars[1].contains(-floor_sqrt(vars[0].getValue()))) { - return ESat.TRUE; - } else if (!vars[1].contains(floor_sqrt(vars[0].getValue())) && - !vars[1].contains(-floor_sqrt(vars[0].getValue()))) { - return ESat.FALSE; - } else { - return ESat.UNDEFINED; - } - } else { - return ESat.UNDEFINED; } + if (isCompletelyInstantiated()) { + return ESat.eval(vars[0].getValue() == sqr(vars[1].getValue())); + } + return ESat.UNDEFINED; } @Override @@ -89,14 +78,16 @@ private void setBounds() throws ContradictionException { } private static int floor_sqrt(int n) { - if (n < 0) + if (n < 0) { return 0; + } return (int) Math.floor(Math.sqrt(n)); } private static int ceil_sqrt(int n) { - if (n < 0) + if (n < 0) { return 0; + } return (int) Math.ceil(Math.sqrt(n)); } @@ -165,7 +156,11 @@ protected boolean updateLowerBoundofY() throws ContradictionException { } protected boolean updateUpperBoundofY() throws ContradictionException { - return vars[1].updateUpperBound(floor_sqrt(vars[0].getUB()), this); + if (vars[1].getUB() < 0) { + return vars[1].updateUpperBound(-ceil_sqrt(vars[0].getLB()), this); + } else { + return vars[1].updateUpperBound(floor_sqrt(vars[0].getUB()), this); + } } protected boolean updateHolesinY() throws ContradictionException { diff --git a/solver/src/test/java/org/chocosolver/solver/constraints/binary/SquareTest.java b/solver/src/test/java/org/chocosolver/solver/constraints/binary/SquareTest.java index e5db51c6e1..63a3704a52 100644 --- a/solver/src/test/java/org/chocosolver/solver/constraints/binary/SquareTest.java +++ b/solver/src/test/java/org/chocosolver/solver/constraints/binary/SquareTest.java @@ -23,6 +23,57 @@ */ public class SquareTest { + @Test(groups = "10s", timeOut = 60000) + public void testBigBoundBound() { + Model m = new Model(); + int n = 6; + IntVar[] x = m.intVarArray(n, -n, n, true); + IntVar[] x2 = m.intVarArray(n, -n*n,n*n, true); + for (int i=0;i Date: Mon, 24 Jul 2023 22:53:36 +0200 Subject: [PATCH 4/6] propsquare filter perfect squares at root node once and for all --- .../solver/constraints/binary/PropSquare.java | 38 ++++++++++++++----- 1 file changed, 29 insertions(+), 9 deletions(-) diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropSquare.java b/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropSquare.java index 0aad53d61f..36d6c5807e 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropSquare.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropSquare.java @@ -111,40 +111,60 @@ protected void updateUpperBoundofX() throws ContradictionException { } protected boolean updateHolesinX() throws ContradictionException { + if (!vars[0].hasEnumeratedDomain()) { + return false; + } + boolean impact = false; + boolean isFirstPropagation = model.getSolver().getNodeCount() == 0; + if (isFirstPropagation) { + // check perfect squares once and for all + int ub = vars[0].getUB(); + vrms.clear(); + vrms.setOffset(vars[0].getLB()); + for (int value = vars[0].getLB(); value <= ub; value = vars[0].nextValue(value)) { + if (!MathUtils.isPerfectSquare(value)) { + vrms.add(value); + } + } + impact = vars[0].removeValues(vrms, this); + } + // remove intervals to deal with consecutive value removal and upper bound modification if (bothEnum) { int ub = vars[0].getUB(); vrms.clear(); vrms.setOffset(vars[0].getLB()); for (int value = vars[0].getLB(); value <= ub; value = vars[0].nextValue(value)) { - if (!(MathUtils.isPerfectSquare(value) && - (vars[1].contains(floor_sqrt(value)) || vars[1].contains(-floor_sqrt(value))))) { + int sqrt = floor_sqrt(value); + if (!vars[1].contains(sqrt) && !vars[1].contains(-sqrt)) { vrms.add(value); } } - return vars[0].removeValues(vrms, this); - } else if (vars[0].hasEnumeratedDomain()) { + impact |= vars[0].removeValues(vrms, this); + } else { int value = vars[0].getLB(); int nlb = value - 1; while (nlb == value - 1) { - if (!vars[1].contains(floor_sqrt(value)) && !vars[1].contains(-floor_sqrt(value))) { + int sqrt = floor_sqrt(value); + if (!vars[1].contains(sqrt) && !vars[1].contains(-sqrt)) { nlb = value; } value = vars[0].nextValue(value); } - boolean filter = vars[0].updateLowerBound(nlb, this); + impact |= vars[0].updateLowerBound(nlb, this); value = vars[0].getUB(); int nub = value + 1; while (nub == value + 1) { - if (!vars[1].contains(floor_sqrt(value)) && !vars[1].contains(-floor_sqrt(value))) { + int sqrt = floor_sqrt(value); + if (!vars[1].contains(sqrt) && !vars[1].contains(-sqrt)) { nub = value; } value = vars[0].previousValue(value); } - return filter | vars[0].updateUpperBound(nub, this); + impact |= vars[0].updateUpperBound(nub, this); } - return false; + return impact; } protected boolean updateLowerBoundofY() throws ContradictionException { From 42bfc35c8d21a959a4deae00f9ae7997f732af5b Mon Sep 17 00:00:00 2001 From: Jean-Guillaume Fages Date: Tue, 25 Jul 2023 09:52:03 +0200 Subject: [PATCH 5/6] squaretest independant of default search --- .../solver/constraints/binary/SquareTest.java | 35 ++++++++++++------- 1 file changed, 23 insertions(+), 12 deletions(-) diff --git a/solver/src/test/java/org/chocosolver/solver/constraints/binary/SquareTest.java b/solver/src/test/java/org/chocosolver/solver/constraints/binary/SquareTest.java index 63a3704a52..4a7c72264a 100644 --- a/solver/src/test/java/org/chocosolver/solver/constraints/binary/SquareTest.java +++ b/solver/src/test/java/org/chocosolver/solver/constraints/binary/SquareTest.java @@ -10,9 +10,11 @@ package org.chocosolver.solver.constraints.binary; import org.chocosolver.solver.Model; +import org.chocosolver.solver.Solver; import org.chocosolver.solver.exception.ContradictionException; import org.chocosolver.solver.search.strategy.Search; import org.chocosolver.solver.variables.IntVar; +import org.chocosolver.util.tools.ArrayUtils; import org.testng.Assert; import org.testng.annotations.Test; @@ -34,10 +36,13 @@ public void testBigBoundBound() { } m.allDifferent(x).post(); m.allDifferent(x2).post(); - while (m.getSolver().solve()) ; - assertEquals(m.getSolver().getSolutionCount(), 184320); - assertEquals(m.getSolver().getFailCount(), 209153); - assertEquals(m.getSolver().getNodeCount(), 577792); + + Solver solver = m.getSolver(); + solver.setSearch(Search.randomSearch(ArrayUtils.append(x,x2), 0)); + while (solver.solve()) ; + assertEquals(solver.getSolutionCount(), 184320); + assertEquals(solver.getFailCount(), 412230); + assertEquals(solver.getNodeCount(), 780869); } @Test(groups = "10s", timeOut = 60000) @@ -51,10 +56,13 @@ public void testBigEnumBound() { } m.allDifferent(x).post(); m.allDifferent(x2).post(); - while (m.getSolver().solve()) ; - assertEquals(m.getSolver().getSolutionCount(), 184320); - assertEquals(m.getSolver().getFailCount(), 28397); - assertEquals(m.getSolver().getNodeCount(), 397036); + + Solver solver = m.getSolver(); + solver.setSearch(Search.randomSearch(ArrayUtils.append(x,x2), 0)); + while (solver.solve()) ; + assertEquals(solver.getSolutionCount(), 184320); + assertEquals(solver.getFailCount(), 11417); + assertEquals(solver.getNodeCount(), 380056); } @Test(groups = "10s", timeOut = 60000) @@ -68,10 +76,13 @@ public void testBigEnumEnum() { } m.allDifferent(x).post(); m.allDifferent(x2).post(); - while (m.getSolver().solve()) ; - assertEquals(m.getSolver().getSolutionCount(), 184320); - assertEquals(m.getSolver().getFailCount(), 0); - assertEquals(m.getSolver().getNodeCount(), 368639); + + Solver solver = m.getSolver(); + solver.setSearch(Search.randomSearch(ArrayUtils.append(x,x2), 0)); + while (solver.solve()) ; + assertEquals(solver.getSolutionCount(), 184320); + assertEquals(solver.getFailCount(), 247); + assertEquals(solver.getNodeCount(), 368886); } @Test(groups = "1s", timeOut = 60000) From 4e266e5797a5e020d99c1c32648f309585d6381e Mon Sep 17 00:00:00 2001 From: Arthur Godet Date: Tue, 1 Aug 2023 12:28:29 +0200 Subject: [PATCH 6/6] simplify code and add propagation tests --- .../solver/constraints/binary/PropSquare.java | 49 ++--------- .../solver/constraints/binary/SquareTest.java | 83 ++++++++++++++++++- 2 files changed, 90 insertions(+), 42 deletions(-) diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropSquare.java b/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropSquare.java index 36d6c5807e..2fc68b2a08 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropSquare.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropSquare.java @@ -47,12 +47,8 @@ public void propagate(int evtmask) throws ContradictionException { do { setBounds(); } while (updateHolesinX() | updateHolesinY()); - if (vars[1].isInstantiated()) { - vars[0].instantiateTo(sqr(vars[1].getValue()), this); - } } - @Override public ESat isEntailed() { if (vars[0].getUB() < 0) { @@ -115,8 +111,7 @@ protected boolean updateHolesinX() throws ContradictionException { return false; } boolean impact = false; - boolean isFirstPropagation = model.getSolver().getNodeCount() == 0; - if (isFirstPropagation) { + if (model.getSolver().getNodeCount() == 0) { // only at root node propagation // check perfect squares once and for all int ub = vars[0].getUB(); vrms.clear(); @@ -141,28 +136,6 @@ protected boolean updateHolesinX() throws ContradictionException { } } impact |= vars[0].removeValues(vrms, this); - } else { - int value = vars[0].getLB(); - int nlb = value - 1; - while (nlb == value - 1) { - int sqrt = floor_sqrt(value); - if (!vars[1].contains(sqrt) && !vars[1].contains(-sqrt)) { - nlb = value; - } - value = vars[0].nextValue(value); - } - impact |= vars[0].updateLowerBound(nlb, this); - - value = vars[0].getUB(); - int nub = value + 1; - while (nub == value + 1) { - int sqrt = floor_sqrt(value); - if (!vars[1].contains(sqrt) && !vars[1].contains(-sqrt)) { - nub = value; - } - value = vars[0].previousValue(value); - } - impact |= vars[0].updateUpperBound(nub, this); } return impact; } @@ -184,19 +157,17 @@ protected boolean updateUpperBoundofY() throws ContradictionException { } protected boolean updateHolesinY() throws ContradictionException { - if (vars[0].isInstantiatedTo(0)) { - return vars[1].instantiateTo(0, this); + if (!vars[1].hasEnumeratedDomain()) { + return false; } boolean impact = false; // remove interval around 0 based on X LB - if (vars[1].hasEnumeratedDomain()) { - int val = ceil_sqrt(vars[0].getLB()) - 1; - if (val >= 0) { - impact = vars[1].removeInterval(-val, val, this); - } + int val = ceil_sqrt(vars[0].getLB()) - 1; + if (val >= 0) { + impact = vars[1].removeInterval(-val, val, this); } - // remove values based on X holes - if (bothEnum && hasHoles(vars[0])) { + // remove values based on X domain + if (bothEnum) { int ub = vars[1].getUB(); vrms.clear(); vrms.setOffset(vars[1].getLB()); @@ -209,8 +180,4 @@ protected boolean updateHolesinY() throws ContradictionException { } return impact; } - - private boolean hasHoles(IntVar var) { - return (var.getUB() - var.getLB() + 1) > var.getDomainSize(); - } } diff --git a/solver/src/test/java/org/chocosolver/solver/constraints/binary/SquareTest.java b/solver/src/test/java/org/chocosolver/solver/constraints/binary/SquareTest.java index 4a7c72264a..41b9a3713e 100644 --- a/solver/src/test/java/org/chocosolver/solver/constraints/binary/SquareTest.java +++ b/solver/src/test/java/org/chocosolver/solver/constraints/binary/SquareTest.java @@ -9,6 +9,7 @@ */ package org.chocosolver.solver.constraints.binary; +import org.chocosolver.solver.Cause; import org.chocosolver.solver.Model; import org.chocosolver.solver.Solver; import org.chocosolver.solver.exception.ContradictionException; @@ -19,12 +20,92 @@ import org.testng.annotations.Test; import static org.testng.Assert.assertEquals; +import static org.testng.Assert.assertTrue; +import static org.testng.Assert.fail; /** * @author Jean-Guillaume Fages */ public class SquareTest { + @Test(groups = "1s", timeOut = 60000) + public void testInstZero() { + Model m = new Model(); + IntVar x = m.intVar(0); + IntVar y = m.intVar(-5, 5, false); + IntVar z = m.intVar(-5, 5, true); + m.square(x, y).post(); + m.square(x, z).post(); + + try { + m.getSolver().propagate(); + } catch (ContradictionException ex) { + fail(); + } + assertTrue(y.isInstantiatedTo(0)); + assertTrue(z.isInstantiatedTo(0)); + } + + @Test(groups = "1s", timeOut = 60000) + public void testInst() { + Model m = new Model(); + IntVar x1 = m.intVar(9); + IntVar y1 = m.intVar(-5, 5, false); + IntVar z1 = m.intVar(-5, 5, true); + m.square(x1, y1).post(); + m.square(x1, z1).post(); + + IntVar x2 = m.intVar(-50, 50, false); + IntVar y2 = m.intVar(-50, 50, true); + IntVar z2 = m.intVar(-3); + m.square(x2, z2).post(); + m.square(y2, z2).post(); + + try { + m.getSolver().propagate(); + } catch (ContradictionException ex) { + fail(); + } + + assertEquals(y1.getLB(), -3); + assertEquals(y1.getUB(), 3); + assertEquals(y1.getDomainSize(), 2); + assertEquals(z1.getLB(), -3); + assertEquals(z1.getUB(), 3); + assertEquals(z1.getDomainSize(), 7); + + assertTrue(x2.isInstantiatedTo(9)); + assertTrue(y2.isInstantiatedTo(9)); + } + + @Test(groups = "1s", timeOut = 60000) + public void testPropBounds() { + Model m = new Model(); + IntVar x = m.intVar(0, 50, false); + IntVar y = m.intVar(3, 5, false); + m.square(x, y).post(); + m.arithm(x, "!=", 16).post(); + + try { + m.getSolver().propagate(); + } catch (ContradictionException ex) { + fail(); + } + assertEquals(x.getLB(), 9); + assertEquals(x.getUB(), 25); + assertEquals(y.getLB(), 3); + assertEquals(y.getUB(), 5); + + try { + y.updateLowerBound(4, Cause.Null); + m.getSolver().propagate(); + } catch (ContradictionException ex) { + fail(); + } + assertTrue(x.isInstantiatedTo(25)); + assertTrue(y.isInstantiatedTo(5)); + } + @Test(groups = "10s", timeOut = 60000) public void testBigBoundBound() { Model m = new Model(); @@ -197,7 +278,7 @@ public void testSquare() { totalSum = model.intVar(0, LANDSCAPE_SIZE); model.sum(sumOfPatchSizes, "=", totalSum).post(); model.getSolver().setSearch(Search.inputOrderLBSearch(model.retrieveIntVars(true))); - model.getSolver().showStatistics(); +// model.getSolver().showStatistics(); model.getSolver().solve(); Assert.assertEquals(1, model.getSolver().getSolutionCount()); Assert.assertEquals(83, model.getSolver().getNodeCount());