Skip to content

Commit

Permalink
#293: fix same ID requirement for Portfolio
Browse files Browse the repository at this point in the history
  • Loading branch information
cprudhom committed Jun 7, 2015
1 parent b68a954 commit 165bd42
Show file tree
Hide file tree
Showing 32 changed files with 255 additions and 118 deletions.
1 change: 1 addition & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ NEXT MILESTONE
- Remove MasterSolver and SlaveSolver (#293)
- Add unplugSearchMonitor() to SearchLoop, Solver ans SearchMonitorList (#300)
- Modify 'ISearchLoop.interrupt()', add new parameter 'avoidable' to qualify the strength of the interruption (#304)
- lazy creation of ZERO, ONE, TRUE and FALSE through methods of Solver (#293)

Bug fixes: #296, #297, #298

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -188,7 +188,7 @@ static Constraint precedence(IntVar x, int duration, IntVar y) {
@Override
public void configureSearch() {
prtfl.carbonCopy();
Solver[] solvers = prtfl.getWorkers();
Solver[] solvers = prtfl.workers;
solvers[1].set(ISF.activity(prtfl.retrieveVarIn(1, prtfl._fes_().retrieveIntVars()), 0));
Arrays.sort(planes, new Comparator<IntVar>() {
@Override
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ public void buildModel() {
@Override
public void configureSearch() {
prtfl.carbonCopy();
Solver[] solvers = prtfl.getWorkers();
Solver[] solvers = prtfl.workers;
solvers[0].set(ISF.activity(prtfl.retrieveVarIn(0, vars), 0));
solvers[1].set(ISF.lexico_LB(prtfl.retrieveVarIn(1, vars)));
solvers[2].set(ISF.minDom_LB(prtfl.retrieveVarIn(2, vars)));
Expand Down
20 changes: 20 additions & 0 deletions choco-solver/src/main/java/org/chocosolver/solver/ISolver.java
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,8 @@
package org.chocosolver.solver;

import org.chocosolver.solver.constraints.Constraint;
import org.chocosolver.solver.constraints.nary.cnf.SatConstraint;
import org.chocosolver.solver.constraints.nary.nogood.NogoodConstraint;
import org.chocosolver.solver.search.measure.IMeasures;
import org.chocosolver.solver.search.strategy.strategy.AbstractStrategy;
import org.chocosolver.solver.variables.IntVar;
Expand Down Expand Up @@ -77,6 +79,24 @@ public interface ISolver {
*/
public IMeasures getMeasures();

/**
* Return a constraint embedding a minisat solver.
* It is highly recommended that there is only once instance of this constraint in a solver.
* So a call to this method will create and post the constraint if it does not exist.
*
* @return the minisat constraint
*/
public SatConstraint getMinisat();

/**
* Return a constraint embedding a nogood store (based on a sat solver).
* It is highly recommended that there is only once instance of this constraint in a solver.
* So a call to this method will create and post the constraint if it does not exist.
*
* @return the minisat constraint
*/
public NogoodConstraint getNogoodStore();

/**
* Override the default search strategies to use in the solver.
* In case many strategies are given, they will be called in sequence:
Expand Down
103 changes: 75 additions & 28 deletions choco-solver/src/main/java/org/chocosolver/solver/Portfolio.java
Original file line number Diff line number Diff line change
Expand Up @@ -30,12 +30,15 @@
import org.chocosolver.memory.Environments;
import org.chocosolver.solver.constraints.Constraint;
import org.chocosolver.solver.constraints.Propagator;
import org.chocosolver.solver.constraints.nary.cnf.SatConstraint;
import org.chocosolver.solver.constraints.nary.nogood.NogoodConstraint;
import org.chocosolver.solver.exception.SolverException;
import org.chocosolver.solver.objective.ObjectiveManager;
import org.chocosolver.solver.search.loop.monitors.IMonitorSolution;
import org.chocosolver.solver.search.measure.IMeasures;
import org.chocosolver.solver.search.solution.LastSolutionRecorder;
import org.chocosolver.solver.search.solution.Solution;
import org.chocosolver.solver.search.strategy.ISF;
import org.chocosolver.solver.search.strategy.strategy.AbstractStrategy;
import org.chocosolver.solver.variables.IntVar;
import org.chocosolver.solver.variables.Variable;
Expand Down Expand Up @@ -115,11 +118,7 @@ public Portfolio(String name, int nthreads) {
this.barrier = new CyclicBarrier(nthreads + 1);
this.new_solutions = new long[nthreads];
this.cmo = new ArrayList<>();
this.cmo.add(workers[lco].ZERO);
this.cmo.add(workers[lco].ONE);
this.cmo.add(workers[lco].TRUE);
this.cmo.add(workers[lco].FALSE);
this.lco = 4;
this.lco = 0;
}

/**
Expand Down Expand Up @@ -161,14 +160,34 @@ public IMeasures getMeasures() {
throw new SolverException("Solver Portfolio does not yet enable to get global measures.");
}

@Override
public SatConstraint getMinisat() {
SatConstraint sc = _fes_().minisat;
if (sc == null) {
sc = _fes_().getMinisat();
cmo.add(sc);
}
return sc;
}

@Override
public NogoodConstraint getNogoodStore() {
NogoodConstraint ngc = _fes_().nogoods;
if (ngc == null) {
ngc = _fes_().getNogoodStore();
cmo.add(ngc);
}
return ngc;
}

/**
* Set the search strategy of the front-end solver
*
* @param strategies the search strategies to use.
*/
@Override
public void set(AbstractStrategy... strategies) {
workers[FRONTEND].set(strategies);
_fes_().set(strategies);
}

private boolean needCopy() {
Expand Down Expand Up @@ -202,6 +221,10 @@ public void carbonCopy() {
for (int j = 0; j < ops.length; j++) {
ops[j].duplicate(workers[i], imaps[i]);
cps[j] = (Propagator) imaps[i].get(ops[j]);
assert cps[j].getId() == ops[j].getId() :
String.format("%s [%d]: wrong ID",
ops[j].getClass().getSimpleName(),
ops[j].getId());
}
Constraint cc = new Constraint(c.getName(), cps);
workers[i].post(cc);
Expand All @@ -210,6 +233,7 @@ public void carbonCopy() {
Variable v = (Variable) o;
for (int i = 1; i < nthreads; i++) {
v.duplicate(workers[i], imaps[i]);
assert v.getId() == ((Variable) imaps[i].get(v)).getId();
}
}
}
Expand All @@ -224,25 +248,6 @@ public void carbonCopy() {
}
}

// private boolean assertCarbonCopy() {
// for (int i = 0; i < workers[0].getNbVars(); i++) {
// Variable v = workers[0].getVar(i);
// for (int j = 1; j < nthreads; j++) {
// assert workers[j].getVar(i).getId() == v.getId();
// }
// }
// for (int i = 0; i < workers[0].getNbCstrs(); i++) {
// Constraint c = workers[0].getCstrs()[i];
// for (int k = 0; k < c.getPropagators().length; k++) {
// Propagator p = c.getPropagator(k);
// for (int j = 1; j < nthreads; j++) {
//
// }
// }
// }
// return true;
// }

private long countNewSolutions() {
long nsol = 0;
for (int i = 0; i < nthreads; i++) {
Expand Down Expand Up @@ -480,7 +485,6 @@ private void stopAll() {
}

@SuppressWarnings("unchecked")
@Deprecated
public <V extends Variable> V retrieveVarIn(int i, V var) {
if (i == FRONTEND) {
return var;
Expand All @@ -489,7 +493,6 @@ public <V extends Variable> V retrieveVarIn(int i, V var) {
}

@SuppressWarnings("unchecked")
@Deprecated
public <V extends Variable> V[] retrieveVarIn(int i, V... vars) {
if (i == FRONTEND) {
return vars;
Expand Down Expand Up @@ -568,6 +571,50 @@ public synchronized void onSolution() {
* @param policy resolution policy, among SATISFACTION, MINIMIZE and MAXIMIZE
*/
private void setStrategies(ResolutionPolicy policy) {
//TODO
//TODO deal with other type of variables
IntVar[] dvars = new IntVar[_fes_().getNbVars()];
Variable[] vars = _fes_().getVars();
if (_fes_().getStrategy() != null
&& _fes_().getStrategy().getVariables().length > 0) {
vars = _fes_().getStrategy().getVariables();
}
assert vars.length > 0;
int k = 0;
for (int i = 0; i < vars.length; i++) {
if ((vars[i].getTypeAndKind() & Variable.INT) > 0) {
dvars[k++] = (IntVar) vars[i];
}
}
dvars = Arrays.copyOf(dvars, k);
int t = 1;
switch (policy) {
default:
// 2nd worker
if (t < nthreads) {
IntVar[] mvars = retrieveVarIn(t, dvars);
workers[t].set(ISF.activity(mvars, 0));
t++;
}
// 3rd worker
if (t < nthreads) {
IntVar[] mvars = retrieveVarIn(t, dvars);
workers[t].set(ISF.domOverWDeg(mvars, 0));
t++;
}
// 4th worker
if (t < nthreads) {
IntVar[] mvars = retrieveVarIn(t, dvars);
workers[t].set(
ISF.lastConflict(workers[t], ISF.minDom_LB(mvars))
);
t++;
}
// then I'm feeling lucky
for (; t < nthreads; t++) {
IntVar[] mvars = retrieveVarIn(t, dvars);
workers[t].set(ISF.activity(mvars, t));
}
break;
}
}
}
64 changes: 56 additions & 8 deletions choco-solver/src/main/java/org/chocosolver/solver/Solver.java
Original file line number Diff line number Diff line change
Expand Up @@ -141,12 +141,12 @@ public class Solver implements Serializable, ISolver {
/**
* Two basic constraints TRUE and FALSE, cached to avoid multiple useless occurrences
*/
public final Constraint TRUE, FALSE;
private Constraint TRUE, FALSE;

/**
* Two basic constants ZERO and ONE, cached to avoid multiple useless occurrences.
*/
public final BoolVar ZERO, ONE;
private BoolVar ZERO, ONE;

/**
* A MiniSat instance, useful to deal with clauses
Expand Down Expand Up @@ -184,12 +184,6 @@ public Solver(IEnvironment environment, String name) {
this.creationTime -= System.nanoTime();
this.cachedConstants = new TIntObjectHashMap<>(16, 1.5f, Integer.MAX_VALUE);
this.engine = NoPropagationEngine.SINGLETON;
ZERO = (BoolVar) VF.fixed(0, this);
ONE = (BoolVar) VF.fixed(1, this);
ZERO._setNot(ONE);
ONE._setNot(ZERO);
TRUE = new Constraint("TRUE cstr", new PropTrue(ONE));
FALSE = new Constraint("FALSE cstr", new PropFalse(ZERO));
solutionRecorder = new LastSolutionRecorder(new Solution(), false, this);
set(ObjectiveManager.SAT());
}
Expand Down Expand Up @@ -227,6 +221,60 @@ public Solver _fes_() {
/////////////////////////////////////// GETTERS ////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////////////////////////////////////////

/**
* The basic constant "0"
*
* @return a boolean variable set to 0
*/
public BoolVar ZERO() {
if (ZERO == null) {
ZERO = (BoolVar) VF.fixed(0, this);
ONE = (BoolVar) VF.fixed(1, this);
ZERO._setNot(ONE);
ONE._setNot(ZERO);
}
return ZERO;
}

/**
* The basic constant "1"
*
* @return a boolean variable set to 1
*/
public BoolVar ONE() {
if (ONE == null) {
ZERO = (BoolVar) VF.fixed(0, this);
ONE = (BoolVar) VF.fixed(1, this);
ZERO._setNot(ONE);
ONE._setNot(ZERO);
}
return ONE;
}

/**
* The basic "true" constraint
*
* @return a "true" constraint
*/
public Constraint TRUE() {
if (TRUE == null) {
TRUE = new Constraint("TRUE cstr", new PropTrue(ONE()));
}
return TRUE;
}

/**
* The basic "false" constraint
*
* @return a "false" constraint
*/
public Constraint FALSE() {
if (FALSE == null) {
FALSE = new Constraint("FALSE cstr", new PropFalse(ZERO()));
}
return FALSE;
}


/**
* Returns the unique and internal search loop.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,7 @@ public class IntConstraintFactory {
* @return a true constraint
*/
public static Constraint TRUE(Solver solver) {
return solver.TRUE;
return solver.TRUE();
}

/**
Expand All @@ -138,7 +138,7 @@ public static Constraint TRUE(Solver solver) {
* @return a false constraint
*/
public static Constraint FALSE(Solver solver) {
return solver.FALSE;
return solver.FALSE();
}

//##################################################################################################################
Expand Down Expand Up @@ -1209,7 +1209,7 @@ public static Constraint[] path(IntVar[] VARS, IntVar START, IntVar END, int OFF
};
default:
if (START == END) {
return new Constraint[]{START.getSolver().FALSE};
return new Constraint[]{START.getSolver().FALSE()};
} else {
return new Constraint[]{
arithm(START, "!=", END),
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -266,9 +266,9 @@ public static Constraint ifThen_reifiable(BoolVar BVAR, Constraint CSTR) {
// PRESOLVE
ESat entail = CSTR.isSatisfied();
if (BVAR.isInstantiatedTo(0) || (BVAR.isInstantiatedTo(1) && entail == ESat.TRUE)) {
return s.TRUE;
return s.TRUE();
}else if (BVAR.isInstantiatedTo(1) && entail == ESat.FALSE) {
return s.FALSE;
return s.FALSE();
}
// END PRESOLVE
return ICF.arithm(BVAR, "<=", CSTR.reif());
Expand All @@ -286,9 +286,9 @@ public static Constraint reification_reifiable(BoolVar BVAR, Constraint CSTR) {
if (BVAR.isInstantiated() && entail != ESat.UNDEFINED) {
if ((BVAR.getValue() == 1 && entail == ESat.TRUE)
|| (BVAR.getValue() == 0 && entail == ESat.FALSE)) {
return s.TRUE;
return s.TRUE();
} else {
return s.FALSE;
return s.FALSE();
}
}
// END PRESOLVE
Expand Down
Loading

0 comments on commit 165bd42

Please sign in to comment.