Commit 1fc1c0dd authored by Anne Parrain's avatar Anne Parrain
Browse files

Add a solver with the "Divide by 2" feature. Correctthe previous version

and remove it from the standard process.
parent c5a99b7a
Pipeline #138 failed with stage
...@@ -68,6 +68,7 @@ import org.sat4j.pb.core.PBSolverCP; ...@@ -68,6 +68,7 @@ import org.sat4j.pb.core.PBSolverCP;
import org.sat4j.pb.core.PBSolverCPCardLearning; import org.sat4j.pb.core.PBSolverCPCardLearning;
import org.sat4j.pb.core.PBSolverCPClauseLearning; import org.sat4j.pb.core.PBSolverCPClauseLearning;
import org.sat4j.pb.core.PBSolverCPLong; import org.sat4j.pb.core.PBSolverCPLong;
import org.sat4j.pb.core.PBSolverCPLongDivideBy2;
import org.sat4j.pb.core.PBSolverCPLongReduceToCard; import org.sat4j.pb.core.PBSolverCPLongReduceToCard;
import org.sat4j.pb.core.PBSolverCPLongRounding; import org.sat4j.pb.core.PBSolverCPLongRounding;
//import org.sat4j.pb.core.PBSolverCard; //import org.sat4j.pb.core.PBSolverCard;
...@@ -632,6 +633,18 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> { ...@@ -632,6 +633,18 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
return solver; return solver;
} }
private static PBSolverCP newPBCPStarDivideBy2(PBDataStructureFactory dsf,
IOrder order, boolean noRemove) {
MiniSATLearning<PBDataStructureFactory> learning = new MiniSATLearning<PBDataStructureFactory>();
PBSolverCP solver = new PBSolverCPLongDivideBy2(learning, dsf, order,
noRemove);
learning.setDataStructureFactory(solver.getDSFactory());
learning.setVarActivityListener(solver);
solver.setRestartStrategy(new ArminRestarts());
solver.setLearnedConstraintsDeletionStrategy(solver.lbd_based);
return solver;
}
private static PBSolverCP newPBCPStarRounding(PBDataStructureFactory dsf, private static PBSolverCP newPBCPStarRounding(PBDataStructureFactory dsf,
IOrder order, boolean noRemove) { IOrder order, boolean noRemove) {
MiniSATLearning<PBDataStructureFactory> learning = new MiniSATLearning<PBDataStructureFactory>(); MiniSATLearning<PBDataStructureFactory> learning = new MiniSATLearning<PBDataStructureFactory>();
...@@ -704,6 +717,11 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> { ...@@ -704,6 +717,11 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
new VarOrderHeapObjective(), true); new VarOrderHeapObjective(), true);
} }
public static IPBSolver newCuttingPlanesStarDivideBy2() {
return newPBCPStarDivideBy2(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true);
}
/** /**
* Cutting Planes based solver. The inference during conflict analysis is * Cutting Planes based solver. The inference during conflict analysis is
* based on cutting planes instead of resolution as in a SAT solver. * based on cutting planes instead of resolution as in a SAT solver.
......
...@@ -35,6 +35,7 @@ import org.sat4j.core.VecInt; ...@@ -35,6 +35,7 @@ import org.sat4j.core.VecInt;
import org.sat4j.minisat.constraints.cnf.Lits; import org.sat4j.minisat.constraints.cnf.Lits;
import org.sat4j.minisat.core.ILits; import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.VarActivityListener; import org.sat4j.minisat.core.VarActivityListener;
import org.sat4j.pb.core.PBSolverStats;
import org.sat4j.specs.IVecInt; import org.sat4j.specs.IVecInt;
import org.sat4j.specs.IteratorInt; import org.sat4j.specs.IteratorInt;
...@@ -49,6 +50,9 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -49,6 +50,9 @@ public class ConflictMap extends MapPb implements IConflict {
public static final int NOPOSTPROCESS = 0; public static final int NOPOSTPROCESS = 0;
public static final int POSTPROCESSTOCLAUSE = 1; public static final int POSTPROCESSTOCLAUSE = 1;
public static final int POSTPROCESSTOCARD = 2; public static final int POSTPROCESSTOCARD = 2;
public static final int POSTPROCESSDIVIDEBY2 = 3;
private static final int NOTCOMPUTED = -2;
protected boolean hasBeenReduced = false; protected boolean hasBeenReduced = false;
protected long numberOfReductions = 0; protected long numberOfReductions = 0;
...@@ -59,6 +63,9 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -59,6 +63,9 @@ public class ConflictMap extends MapPb implements IConflict {
protected BigInteger currentSlack; protected BigInteger currentSlack;
protected int currentLevel; protected int currentLevel;
private int backtrackLevel = NOTCOMPUTED;
private final PBSolverStats stats;
/** /**
* allows to access directly to all variables belonging to a particular * allows to access directly to all variables belonging to a particular
...@@ -82,24 +89,31 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -82,24 +89,31 @@ public class ConflictMap extends MapPb implements IConflict {
public static IConflict createConflict(PBConstr cpb, int level, public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove) { boolean noRemove) {
return new ConflictMap(cpb, level, noRemove, NOPOSTPROCESS); return new ConflictMap(cpb, level, noRemove, NOPOSTPROCESS, null);
} }
public static IConflict createConflict(PBConstr cpb, int level, public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, int postProcessing) { boolean noRemove, int postProcessing) {
return new ConflictMap(cpb, level, noRemove, postProcessing); return new ConflictMap(cpb, level, noRemove, postProcessing, null);
}
public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, int postProcessing, PBSolverStats stats) {
return new ConflictMap(cpb, level, noRemove, postProcessing, stats);
} }
ConflictMap(PBConstr cpb, int level) { ConflictMap(PBConstr cpb, int level) {
this(cpb, level, false, NOPOSTPROCESS); this(cpb, level, false, NOPOSTPROCESS, null);
} }
ConflictMap(PBConstr cpb, int level, boolean noRemove) { ConflictMap(PBConstr cpb, int level, boolean noRemove) {
this(cpb, level, noRemove, NOPOSTPROCESS); this(cpb, level, noRemove, NOPOSTPROCESS, null);
} }
ConflictMap(PBConstr cpb, int level, boolean noRemove, int postProcessing) { ConflictMap(PBConstr cpb, int level, boolean noRemove, int postProcessing,
PBSolverStats stats) {
super(cpb, level, noRemove); super(cpb, level, noRemove);
this.stats = stats;
this.voc = cpb.getVocabulary(); this.voc = cpb.getVocabulary();
this.currentLevel = level; this.currentLevel = level;
initStructures(); initStructures();
...@@ -110,10 +124,14 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -110,10 +124,14 @@ public class ConflictMap extends MapPb implements IConflict {
case POSTPROCESSTOCARD: case POSTPROCESSTOCARD:
this.postProcess = new PostProcessToCard(); this.postProcess = new PostProcessToCard();
break; break;
case POSTPROCESSDIVIDEBY2:
this.postProcess = new PostProcessDivideBy2();
break;
default: default:
this.postProcess = new NoPostProcess(); this.postProcess = new NoPostProcess();
break; break;
} }
if (noRemove) if (noRemove)
this.rmSatLit = new NoRemoveSatisfied(); this.rmSatLit = new NoRemoveSatisfied();
else else
...@@ -224,18 +242,6 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -224,18 +242,6 @@ public class ConflictMap extends MapPb implements IConflict {
*/ */
private interface IPostProcess { private interface IPostProcess {
void postProcess(int dl); void postProcess(int dl);
/**
* retourne le niveau de backtrack : c'est-?-dire le niveau le plus haut
* pour lequel la contrainte est assertive
*
* @param maxLevel
* le plus bas niveau pour lequel la contrainte est assertive
* @return the highest level (smaller int) for which the constraint is
* assertive.
*/
int getBacktrackLevel(int maxLevel);
} }
private final IPostProcess postProcess; private final IPostProcess postProcess;
...@@ -245,56 +251,6 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -245,56 +251,6 @@ public class ConflictMap extends MapPb implements IConflict {
} }
/**
* computes the level for the backtrack : the highest decision level for
* which the conflict is assertive.
*
* @param maxLevel
* the lowest level for which the conflict is assertive
* @return the highest level (smaller int) for which the constraint is
* assertive.
*/
public int getBacktrackLevel(int maxLevel) {
// we are looking for a level higher than maxLevel
// where the constraint is still assertive
VecInt lits;
int level;
int indStop = levelToIndex(maxLevel) - 1;
int indStart = levelToIndex(0);
BigInteger slack = computeSlack(0)
.subtract(ConflictMap.this.degree);
int previous = 0;
for (int indLevel = indStart; indLevel <= indStop; indLevel++) {
if (ConflictMap.this.byLevel[indLevel] != null) {
level = indexToLevel(indLevel);
assert ConflictMap.this.computeSlack(level)
.subtract(ConflictMap.this.degree).equals(slack);
if (ConflictMap.this.isImplyingLiteralOrdered(level,
slack)) {
break;
}
// updating the new slack
lits = ConflictMap.this.byLevel[indLevel];
int lit;
for (IteratorInt iterator = lits.iterator(); iterator
.hasNext();) {
lit = iterator.next();
if (ConflictMap.this.voc.isFalsified(lit)
&& ConflictMap.this.voc.getLevel(
lit) == indexToLevel(indLevel)) {
slack = slack.subtract(
ConflictMap.this.weightedLits.get(lit));
}
}
if (!lits.isEmpty()) {
previous = level;
}
}
}
assert previous == oldGetBacktrackLevel(maxLevel);
return previous;
}
} }
private class PostProcessToClause implements IPostProcess { private class PostProcessToClause implements IPostProcess {
...@@ -303,7 +259,8 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -303,7 +259,8 @@ public class ConflictMap extends MapPb implements IConflict {
&& (!ConflictMap.this.degree.equals(BigInteger.ONE))) { && (!ConflictMap.this.degree.equals(BigInteger.ONE))) {
int litLevel, ilit; int litLevel, ilit;
if (ConflictMap.this.assertiveLiteral != -1) { if (ConflictMap.this.assertiveLiteral != -1) {
this.chooseAssertiveLiteral(dl); ConflictMap.this.assertiveLiteral = this
.chooseAssertiveLiteral(dl);
int lit = ConflictMap.this.weightedLits int lit = ConflictMap.this.weightedLits
.getLit(ConflictMap.this.assertiveLiteral); .getLit(ConflictMap.this.assertiveLiteral);
...@@ -330,23 +287,21 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -330,23 +287,21 @@ public class ConflictMap extends MapPb implements IConflict {
ConflictMap.this.degree = BigInteger.ONE; ConflictMap.this.degree = BigInteger.ONE;
ConflictMap.this.assertiveLiteral = ConflictMap.this.weightedLits ConflictMap.this.assertiveLiteral = ConflictMap.this.weightedLits
.getFromAllLits(lit); .getFromAllLits(lit);
// ConflictMap.this.currentSlack = ConflictMap.this assert ConflictMap.this.backtrackLevel == oldGetBacktrackLevel(
// .computeSlack(this.assertiveLevel); dl);
// assert ConflictMap.this.isAssertive(this.backtrackLevel);
assert this.backtrackLevel == oldGetBacktrackLevel(dl);
} }
} }
} }
private int assertiveLevel; private int assertiveLevel;
private int backtrackLevel;
public void chooseAssertiveLiteral(int maxLevel) { public int chooseAssertiveLiteral(int maxLevel) {
// we are looking for a level higher than maxLevel // we are looking for a level higher than maxLevel
// where the constraint is still assertive // where the constraint is still assertive
// update ConflictMap.this.assertiveLiteral // update ConflictMap.this.assertiveLiteral
VecInt lits; VecInt lits;
int level; int level;
int indStop = levelToIndex(maxLevel); // ou maxLevel - 1 ??? int indStop = levelToIndex(maxLevel); // ou maxLevel - 1 ???
int indStart = levelToIndex(0); int indStart = levelToIndex(0);
BigInteger slack = ConflictMap.this.computeSlack(0) BigInteger slack = ConflictMap.this.computeSlack(0)
...@@ -359,8 +314,8 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -359,8 +314,8 @@ public class ConflictMap extends MapPb implements IConflict {
.subtract(ConflictMap.this.degree).equals(slack); .subtract(ConflictMap.this.degree).equals(slack);
if (ConflictMap.this.isImplyingLiteralOrdered(level, if (ConflictMap.this.isImplyingLiteralOrdered(level,
slack)) { slack)) {
this.backtrackLevel = previous; ConflictMap.this.backtrackLevel = previous;
this.assertiveLevel = level; assertiveLevel = level;
break; break;
} }
// updating the new slack // updating the new slack
...@@ -382,11 +337,9 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -382,11 +337,9 @@ public class ConflictMap extends MapPb implements IConflict {
} }
} }
assert this.backtrackLevel == oldGetBacktrackLevel(maxLevel); assert ConflictMap.this.backtrackLevel == oldGetBacktrackLevel(
} maxLevel);
return assertiveLiteral;
public int getBacktrackLevel(int maxLevel) {
return this.backtrackLevel;
} }
} }
...@@ -469,13 +422,13 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -469,13 +422,13 @@ public class ConflictMap extends MapPb implements IConflict {
ConflictMap.this.assertiveLiteral = ConflictMap.this.weightedLits ConflictMap.this.assertiveLiteral = ConflictMap.this.weightedLits
.getFromAllLits(lit); .getFromAllLits(lit);
assert this.backtrackLevel == oldGetBacktrackLevel(dl); assert ConflictMap.this.backtrackLevel == oldGetBacktrackLevel(
dl);
} }
} }
} }
private int assertiveLevel; private int assertiveLevel;
private int backtrackLevel;
public int chooseAssertiveLiteral(int maxLevel) { public int chooseAssertiveLiteral(int maxLevel) {
// we are looking for a level higher than maxLevel // we are looking for a level higher than maxLevel
...@@ -493,10 +446,10 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -493,10 +446,10 @@ public class ConflictMap extends MapPb implements IConflict {
level = indexToLevel(indLevel); level = indexToLevel(indLevel);
assert ConflictMap.this.computeSlack(level) assert ConflictMap.this.computeSlack(level)
.subtract(ConflictMap.this.degree).equals(slack); .subtract(ConflictMap.this.degree).equals(slack);
if (ConflictMap.this.isImplyingLiteralOrderedIndexes(level, if (ConflictMap.this.isImplyingLiteralOrdered(level, slack,
slack, literals)) { literals)) {
this.assertiveLevel = level; this.assertiveLevel = level;
this.backtrackLevel = previous; ConflictMap.this.backtrackLevel = previous;
break; break;
} }
// updating the new slack // updating the new slack
...@@ -530,13 +483,23 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -530,13 +483,23 @@ public class ConflictMap extends MapPb implements IConflict {
} }
} }
assert this.backtrackLevel == oldGetBacktrackLevel(maxLevel); assert ConflictMap.this.backtrackLevel == oldGetBacktrackLevel(
maxLevel);
assert literals.size() > 0; assert literals.size() > 0;
return maxLit; return maxLit;
} }
public int getBacktrackLevel(int maxLevel) { }
return this.backtrackLevel;
private class PostProcessDivideBy2 implements IPostProcess {
public void postProcess(int dl) {
int nbBits = ConflictMap.this.reduceCoeffsByPower2();
if (nbBits > 0) {
stats.numberOfReductionsByPower2++;
stats.numberOfRightShiftsForCoeffs = stats.numberOfRightShiftsForCoeffs
+ nbBits;
}
} }
} }
...@@ -905,21 +868,6 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -905,21 +868,6 @@ public class ConflictMap extends MapPb implements IConflict {
// a particular level // a particular level
// uses the coefs data structure (where coefficients are decreasing ordered) // uses the coefs data structure (where coefficients are decreasing ordered)
// to parse each literal // to parse each literal
private boolean isImplyingLiteralOrderedIndexes(int dl, BigInteger slack,
IVecInt literals) {
assert literals.size() == 0;
int ilit, litLevel;
for (int i = 0; i < size(); i++) {
ilit = this.weightedLits.getLit(i);
litLevel = this.voc.getLevel(ilit);
if ((litLevel >= dl || this.voc.isUnassigned(ilit))
&& slack.compareTo(this.weightedLits.getCoef(i)) < 0) {
literals.push(i);
}
}
return literals.size() > 0;
}
private boolean isImplyingLiteralOrdered(int dl, BigInteger slack, private boolean isImplyingLiteralOrdered(int dl, BigInteger slack,
IVecInt literals) { IVecInt literals) {
assert literals.size() == 0; assert literals.size() == 0;
...@@ -929,7 +877,7 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -929,7 +877,7 @@ public class ConflictMap extends MapPb implements IConflict {
litLevel = this.voc.getLevel(ilit); litLevel = this.voc.getLevel(ilit);
if ((litLevel >= dl || this.voc.isUnassigned(ilit)) if ((litLevel >= dl || this.voc.isUnassigned(ilit))
&& slack.compareTo(this.weightedLits.getCoef(i)) < 0) { && slack.compareTo(this.weightedLits.getCoef(i)) < 0) {
literals.push(ilit); literals.push(i);
} }
} }
return literals.size() > 0; return literals.size() > 0;
...@@ -1068,7 +1016,46 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -1068,7 +1016,46 @@ public class ConflictMap extends MapPb implements IConflict {
* assertive. * assertive.
*/ */
public int getBacktrackLevel(int maxLevel) { public int getBacktrackLevel(int maxLevel) {
return this.postProcess.getBacktrackLevel(maxLevel); if (this.backtrackLevel == NOTCOMPUTED) {
// we are looking for a level higher than maxLevel
// where the constraint is still assertive
VecInt lits;
int level;
int indStop = levelToIndex(maxLevel) - 1;
int indStart = levelToIndex(0);
BigInteger slack = computeSlack(0)
.subtract(ConflictMap.this.degree);
int previous = 0;
for (int indLevel = indStart; indLevel <= indStop; indLevel++) {
if (ConflictMap.this.byLevel[indLevel] != null) {
level = indexToLevel(indLevel);
assert ConflictMap.this.computeSlack(level)
.subtract(ConflictMap.this.degree).equals(slack);
if (ConflictMap.this.isImplyingLiteralOrdered(level, slack))
break;
// updating the new slack
lits = ConflictMap.this.byLevel[indLevel];
int lit;
for (IteratorInt iterator = lits.iterator(); iterator
.hasNext();) {
lit = iterator.next();
if (ConflictMap.this.voc.isFalsified(lit)
&& ConflictMap.this.voc.getLevel(
lit) == indexToLevel(indLevel))
slack = slack.subtract(
ConflictMap.this.weightedLits.get(lit));
}
if (!lits.isEmpty())
previous = level;
}
}
assert previous == oldGetBacktrackLevel(maxLevel);
return previous;
} else
return this.backtrackLevel;
} }
public int oldGetBacktrackLevel(int maxLevel) { public int oldGetBacktrackLevel(int maxLevel) {
......
...@@ -75,10 +75,14 @@ public class MapPb implements IDataStructurePB { ...@@ -75,10 +75,14 @@ public class MapPb implements IDataStructurePB {
} }
public int reduceCoeffsByPower2() { public int reduceCoeffsByPower2() {
int nbBits = 1; assert this.weightedLits.size() > 0;
for (int i = 0; i < this.weightedLits.size() && nbBits > 0; i++) int nbBits = this.weightedLits.getCoef(0).bitLength();
for (int i = 0; i < this.weightedLits.size() && nbBits > 0; i++) {
nbBits = Math.min(nbBits, nbBits = Math.min(nbBits,
this.weightedLits.getCoef(i).getLowestSetBit()); this.weightedLits.getCoef(i).getLowestSetBit());
if (nbBits == 0)
break;
}
if (nbBits > 0) { if (nbBits > 0) {
for (int i = 0; i < this.weightedLits.size(); i++) { for (int i = 0; i < this.weightedLits.size(); i++) {
this.weightedLits.changeCoef(i, this.weightedLits.changeCoef(i,
......
...@@ -164,12 +164,6 @@ public class PBSolverCP extends PBSolver { ...@@ -164,12 +164,6 @@ public class PBSolverCP extends PBSolver {
} }
// assertive PB-constraint is build and referenced // assertive PB-constraint is build and referenced
int nbBits = confl.reduceCoeffsByPower2();
if (nbBits > 0) {
stats.numberOfReductionsByPower2++;
stats.numberOfRightShiftsForCoeffs = stats.numberOfRightShiftsForCoeffs
+ nbBits;
}
confl.postProcess(currentLevel); confl.postProcess(currentLevel);
PBConstr resConstr = (PBConstr) this.dsfactory PBConstr resConstr = (PBConstr) this.dsfactory
.createUnregisteredPseudoBooleanConstraint(confl); .createUnregisteredPseudoBooleanConstraint(confl);
......
package org.sat4j.pb.core;
import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.LearningStrategy;
import org.sat4j.minisat.core.RestartStrategy;
import org.sat4j.minisat.core.SearchParams;
import org.sat4j.pb.constraints.pb.ConflictMap;
import org.sat4j.pb.constraints.pb.ConflictMapReduceToClause;
import org.sat4j.pb.constraints.pb.IConflict;
import org.sat4j.pb.constraints.pb.PBConstr;
public class PBSolverCPLongDivideBy2 extends PBSolverCPLong {
public PBSolverCPLongDivideBy2(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, IOrder order) {
super(learner, dsf, order);
// TODO Auto-generated constructor stub
}
public PBSolverCPLongDivideBy2(
LearningStrategy<PBDataStructureFactory> learner,