Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make propagation stops sooner if time limit is met (fix issue #1062) #1064

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
26 changes: 24 additions & 2 deletions solver/src/main/java/org/chocosolver/solver/Solver.java
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@
import org.chocosolver.solver.propagation.PropagationEngine;
import org.chocosolver.solver.search.SearchState;
import org.chocosolver.solver.search.limits.ICounter;
import org.chocosolver.solver.search.limits.TimeCounter;
import org.chocosolver.solver.search.loop.Reporting;
import org.chocosolver.solver.search.loop.learn.Learn;
import org.chocosolver.solver.search.loop.learn.LearnNothing;
Expand Down Expand Up @@ -169,6 +170,8 @@ public enum Action {
*/
protected List<Criterion> criteria;

protected TimeCounter timeCounter;

/**
* Indicates if the default search loop is in use (set to <tt>true</tt> in that case).
*/
Expand Down Expand Up @@ -1007,11 +1010,21 @@ public boolean hasEndedUnexpectedly() {
return mMeasures.getSearchState() == SearchState.KILLED;
}

/**
* @return <tt>true</tt> if the time limit is met.
*/
public boolean isTimeLimitMet() {
if (timeCounter != null) {
return timeCounter.isMet();
}
return false;
}

/**
* @return <tt>true</tt> if the search loops encountered at least one of the stop criteria declared.
*/
public boolean isStopCriterionMet() {
boolean ismet = false;
boolean ismet = isTimeLimitMet();
for (int i = 0; i < criteria.size() && !ismet; i++) {
ismet = criteria.get(i).isMet();
}
Expand Down Expand Up @@ -1311,7 +1324,16 @@ public void removeHints() {
*/
public void addStopCriterion(Criterion... criterion) {
if (criterion != null) {
Collections.addAll(criteria, criterion);
for (int i = 0; i < criterion.length; i++) {
if (criterion[i] instanceof TimeCounter) {
TimeCounter tc = (TimeCounter) criterion[i];
if (timeCounter == null || timeCounter.getLimitValue() > tc.getLimitValue()) {
timeCounter = tc;
}
} else {
criteria.add(criterion[i]);
}
}
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -189,6 +189,9 @@ public void propagate() throws ContradictionException {
manageModifications();
for (int i = nextNotEmpty(); i > -1; i = nextNotEmpty()) {
assert !pro_queue[i].isEmpty() : "try to pop a propagator from an empty queue";
if (model.getSolver().isTimeLimitMet()) {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why not calling model.getSolver().isStopCriterionMet() ?
This would avoid modifying the Solver class.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The idea was to have a simple check on the time limit, and not check all the stopping criterion before the propagation of each propagator.
Indeed, all stopping criterion but the time limit do not depend on the problem's state outside of fixpoint. Unless you can think of one that would.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Personnaly, I would have move the code to the end of the while-loop just to keep the main purpose (ie, propagating) clear

return;
}
lastProp = pro_queue[i].pollFirst();
if (pro_queue[i].isEmpty()) {
notEmpty &= ~(1 << i);
Expand Down
32 changes: 32 additions & 0 deletions solver/src/test/java/org/chocosolver/solver/LimitsTest.java
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,15 @@
*/
package org.chocosolver.solver;

import org.chocosolver.solver.exception.SolverException;
import org.chocosolver.solver.variables.IntVar;
import org.chocosolver.util.tools.TimeUtils;
import org.testng.Assert;
import org.testng.annotations.Test;

import static org.chocosolver.util.ProblemMaker.makeNQueenWithBinaryConstraints;
import static org.testng.Assert.assertEquals;
import static org.testng.Assert.assertFalse;
import static org.testng.Assert.assertTrue;

/**
Expand All @@ -35,6 +38,35 @@ public void testTime() {
assertTrue(tl - (tl * 5 / 100) <= tc && tc <= tl + (tl * 5 / 100), tl + " vs. " + tc);
}

@Test(groups="1s", timeOut=60000)
public void testTime2() throws SolverException {
Model model = new Model();

IntVar v7 = model.intVar("@v7", IntVar.MIN_INT_BOUND, IntVar.MAX_INT_BOUND, true);

model.post(
model.arithm(v7, ">", v7),
model.arithm(v7, "<", v7)
);
// TODO : such a simple case should be detected within the constraint declaration
// TODO : this test might need to be changed if better model analysis is done during model declaration

Solver solver = model.getSolver();
solver.limitTime(250);

long start = System.currentTimeMillis();
boolean solved = solver.solve();
long took = System.currentTimeMillis() - start;

assertFalse(solved);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good to check that solve() returns false;

assertEquals(solver.getNodeCount(), 1);
assertEquals(solver.getBackTrackCount(), 0);
assertEquals(solver.getFailCount(), 0);
assertEquals(solver.getSolutionCount(), 0);
assertTrue(solver.isStopCriterionMet());
assertTrue(took <= 1000); // less than 1 second
}

@Test(groups="1s", timeOut=60000)
public void testNode() {
Model s = makeNQueenWithBinaryConstraints(12);
Expand Down