Commit d0bd4984 authored by Anne Parrain's avatar Anne Parrain

Skipping resolutions steps during conflict analysis is now allowed,

using Jan's algorithm. 

New solvers in the solver factory and new class for unit tests are
added.  
parent a07b1f0a
......@@ -51,6 +51,8 @@ public class ConflictMap extends MapPb implements IConflict {
protected boolean hasBeenReduced = false;
protected long numberOfReductions = 0;
private boolean allowSkipping = false;
private boolean endingSkipping = true;
/**
* to store the slack of the current resolvant
......@@ -84,33 +86,47 @@ public class ConflictMap extends MapPb implements IConflict {
public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove) {
return new ConflictMap(cpb, level, noRemove, NoPostProcess.instance(),
null);
return new ConflictMap(cpb, level, noRemove, false,
NoPostProcess.instance(), null);
}
public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, PBSolverStats stats) {
return new ConflictMap(cpb, level, noRemove, skip,
NoPostProcess.instance(), stats);
}
public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, IPostProcess postProcessing) {
return new ConflictMap(cpb, level, noRemove, postProcessing, null);
return new ConflictMap(cpb, level, noRemove, false, postProcessing,
null);
}
public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, IPostProcess postProcessing,
boolean noRemove, boolean skip, IPostProcess postProcessing,
PBSolverStats stats) {
return new ConflictMap(cpb, level, noRemove, postProcessing, stats);
return new ConflictMap(cpb, level, noRemove, skip, postProcessing,
stats);
}
ConflictMap(PBConstr cpb, int level) {
this(cpb, level, false, NoPostProcess.instance(), null);
this(cpb, level, false, false, NoPostProcess.instance(), null);
}
ConflictMap(PBConstr cpb, int level, boolean noRemove) {
this(cpb, level, noRemove, NoPostProcess.instance(), null);
this(cpb, level, noRemove, false, NoPostProcess.instance(), null);
}
ConflictMap(PBConstr cpb, int level, boolean noRemove, boolean skip,
PBSolverStats stats) {
this(cpb, level, noRemove, skip, NoPostProcess.instance(), stats);
}
ConflictMap(PBConstr cpb, int level, boolean noRemove,
ConflictMap(PBConstr cpb, int level, boolean noRemove, boolean skip,
IPostProcess postProcessing, PBSolverStats stats) {
super(cpb, level, noRemove);
this.stats = stats;
this.allowSkipping = skip;
this.voc = cpb.getVocabulary();
this.currentLevel = level;
initStructures();
......@@ -272,6 +288,29 @@ public class ConflictMap extends MapPb implements IConflict {
return this.degree;
}
if (this.allowSkipping) {
if (this.weightedLits.get(nLitImplied).negate()
.compareTo(currentSlack.subtract(degree)) > 0) {
if (this.endingSkipping)
stats.numberOfEndingSkipping++;
else
stats.numberOfInternalSkipping++;
// no resolution
// undo operation should be anticipated
int litLevel = levelToIndex(this.voc.getLevel(litImplied));
this.byLevel[litLevel].remove(nLitImplied);
if (this.byLevel[0] == null) {
this.byLevel[0] = new VecInt();
}
this.byLevel[0].push(nLitImplied);
assert slackConflict().signum() < 0;
return this.degree;
} else
this.endingSkipping = false;
}
assert slackConflict().signum() < 0;
assert this.degree.signum() >= 0;
......
......@@ -15,20 +15,20 @@ public class ConflictMapReduceByGCD extends ConflictMap {
}
public ConflictMapReduceByGCD(PBConstr cpb, int level, boolean noRemove,
IPostProcess postProcessing, PBSolverStats stats) {
super(cpb, level, noRemove, postProcessing, stats);
boolean skip, IPostProcess postProcessing, PBSolverStats stats) {
super(cpb, level, noRemove, skip, postProcessing, stats);
// TODO Auto-generated constructor stub
}
public static IConflict createConflict(PBConstr cpb, int level,
PBSolverStats stats) {
return new ConflictMapReduceByGCD(cpb, level, true,
return new ConflictMapReduceByGCD(cpb, level, true, false,
NoPostProcess.instance(), stats);
}
public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, PBSolverStats stats) {
return new ConflictMapReduceByGCD(cpb, level, noRemove,
boolean noRemove, boolean skip, PBSolverStats stats) {
return new ConflictMapReduceByGCD(cpb, level, noRemove, skip,
NoPostProcess.instance(), stats);
}
......
......@@ -4,33 +4,33 @@ import org.sat4j.pb.core.PBSolverStats;
public class ConflictMapReduceByPowersOf2 extends ConflictMap {
public ConflictMapReduceByPowersOf2(PBConstr cpb, int level) {
super(cpb, level);
// TODO Auto-generated constructor stub
}
public ConflictMapReduceByPowersOf2(PBConstr cpb, int level,
boolean noRemove) {
super(cpb, level, noRemove);
// TODO Auto-generated constructor stub
}
// public ConflictMapReduceByPowersOf2(PBConstr cpb, int level) {
// super(cpb, level);
// // TODO Auto-generated constructor stub
// }
//
// public ConflictMapReduceByPowersOf2(PBConstr cpb, int level,
// boolean noRemove) {
// super(cpb, level, noRemove);
// // TODO Auto-generated constructor stub
// }
public ConflictMapReduceByPowersOf2(PBConstr cpb, int level,
boolean noRemove, IPostProcess postProcessing,
boolean noRemove, boolean skip, IPostProcess postProcessing,
PBSolverStats stats) {
super(cpb, level, noRemove, postProcessing, stats);
super(cpb, level, noRemove, skip, postProcessing, stats);
// TODO Auto-generated constructor stub
}
public static IConflict createConflict(PBConstr cpb, int level,
PBSolverStats stats) {
return new ConflictMapReduceByPowersOf2(cpb, level, true,
NoPostProcess.instance(), stats);
}
// public static IConflict createConflict(PBConstr cpb, int level,
// PBSolverStats stats) {
// return new ConflictMapReduceByPowersOf2(cpb, level, true,
// NoPostProcess.instance(), stats);
// }
public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, PBSolverStats stats) {
return new ConflictMapReduceByPowersOf2(cpb, level, noRemove,
boolean noRemove, boolean skip, PBSolverStats stats) {
return new ConflictMapReduceByPowersOf2(cpb, level, noRemove, skip,
NoPostProcess.instance(), stats);
}
......
......@@ -2,6 +2,8 @@ package org.sat4j.pb.constraints.pb;
import java.math.BigInteger;
import org.sat4j.pb.core.PBSolverStats;
/**
* This class implements the reduction to cardinality algorithm proposed by
* Heidi Dixon in her dissertation. Procedure 4.3.9 page 67, in Automating
......@@ -24,6 +26,17 @@ public class ConflictMapReduceToCard extends ConflictMap {
super(cpb, level, noRemove);
}
public ConflictMapReduceToCard(PBConstr cpb, int level, boolean noRemove,
boolean skip, PBSolverStats stats) {
super(cpb, level, noRemove, skip, stats);
// TODO Auto-generated constructor stub
}
public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, PBSolverStats stats) {
return new ConflictMapReduceToCard(cpb, level, noRemove, skip, stats);
}
public static IConflict createConflict(PBConstr cpb, int level) {
return new ConflictMapReduceToCard(cpb, level);
}
......
......@@ -31,6 +31,8 @@ package org.sat4j.pb.constraints.pb;
import java.math.BigInteger;
import org.sat4j.pb.core.PBSolverStats;
public final class ConflictMapReduceToClause extends ConflictMap {
public ConflictMapReduceToClause(PBConstr cpb, int level) {
......@@ -38,16 +40,28 @@ public final class ConflictMapReduceToClause extends ConflictMap {
// TODO Auto-generated constructor stub
}
public ConflictMapReduceToClause(PBConstr cpb, int level, boolean noRemove) {
public ConflictMapReduceToClause(PBConstr cpb, int level,
boolean noRemove) {
super(cpb, level, noRemove);
// TODO Auto-generated constructor stub
}
public ConflictMapReduceToClause(PBConstr cpb, int level, boolean noRemove,
boolean skip, PBSolverStats stats) {
super(cpb, level, noRemove, skip, stats);
// TODO Auto-generated constructor stub
}
public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove) {
return new ConflictMapReduceToClause(cpb, level, noRemove);
}
public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, PBSolverStats stats) {
return new ConflictMapReduceToClause(cpb, level, noRemove, skip, stats);
}
public static IConflict createConflict(PBConstr cpb, int level) {
return new ConflictMapReduceToClause(cpb, level);
}
......
......@@ -58,6 +58,12 @@ public class PBSolverCP extends PBSolver {
*/
protected boolean noRemove = true;
/**
* skipping as much as possible avoidable cutting planes during analysis
* conflict
*/
protected boolean skipAllow = true;
/**
* @param acg
* @param learner
......@@ -81,23 +87,27 @@ public class PBSolverCP extends PBSolver {
}
public PBSolverCP(LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, IOrder order, boolean noRemove) {
PBDataStructureFactory dsf, IOrder order, boolean noRemove,
boolean skipAllow) {
this(learner, dsf, order);
this.noRemove = noRemove;
this.skipAllow = skipAllow;
}
public PBSolverCP(LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order,
RestartStrategy restarter, boolean noRemove) {
RestartStrategy restarter, boolean noRemove, boolean skipAllow) {
this(learner, dsf, params, order, restarter);
this.noRemove = noRemove;
this.skipAllow = skipAllow;
}
public PBSolverCP(LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order,
boolean noRemove) {
boolean noRemove, boolean skipAllow) {
this(learner, dsf, params, order);
this.noRemove = noRemove;
this.skipAllow = skipAllow;
}
@Override
......@@ -182,7 +192,8 @@ public class PBSolverCP extends PBSolver {
}
protected IConflict chooseConflict(PBConstr myconfl, int level) {
return ConflictMap.createConflict(myconfl, level, noRemove);
return ConflictMap.createConflict(myconfl, level, noRemove, skipAllow,
stats);
}
@Override
......@@ -191,6 +202,9 @@ public class PBSolverCP extends PBSolver {
+ this.getClass().getName() + ")"
+ (this.noRemove ? ""
: " - removing satisfied literals at a higher level before CP -")
+ (this.skipAllow
? " - skipping as much as possible cutting planes during analysis conflict- Jan Elffers's algorithm -"
: "")
+ "\n" + super.toString(prefix);
}
......
......@@ -66,28 +66,29 @@ public class PBSolverCPCardLearning extends PBSolverCPLong {
public PBSolverCPCardLearning(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, IOrder order, boolean noRemove) {
super(learner, dsf, order, noRemove);
PBDataStructureFactory dsf, IOrder order, boolean noRemove,
boolean skipAllow) {
super(learner, dsf, order, noRemove, skipAllow);
}
public PBSolverCPCardLearning(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order,
RestartStrategy restarter, boolean noRemove) {
super(learner, dsf, params, order, restarter, noRemove);
RestartStrategy restarter, boolean noRemove, boolean skipAllow) {
super(learner, dsf, params, order, restarter, noRemove, skipAllow);
}
public PBSolverCPCardLearning(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order,
boolean noRemove) {
super(learner, dsf, params, order, noRemove);
boolean noRemove, boolean skipAllow) {
super(learner, dsf, params, order, noRemove, skipAllow);
}
@Override
protected IConflict chooseConflict(PBConstr myconfl, int level) {
return ConflictMapReduceToClause.createConflict(myconfl, level,
noRemove, PostProcessToCard.instance());
noRemove, skipAllow, PostProcessToCard.instance(), stats);
}
@Override
......
......@@ -71,28 +71,29 @@ public class PBSolverCPClauseLearning extends PBSolverCPLong {
public PBSolverCPClauseLearning(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, IOrder order, boolean noRemove) {
super(learner, dsf, order, noRemove);
PBDataStructureFactory dsf, IOrder order, boolean noRemove,
boolean skipAllow) {
super(learner, dsf, order, noRemove, skipAllow);
}
public PBSolverCPClauseLearning(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order,
RestartStrategy restarter, boolean noRemove) {
super(learner, dsf, params, order, restarter, noRemove);
RestartStrategy restarter, boolean noRemove, boolean skipAllow) {
super(learner, dsf, params, order, restarter, noRemove, skipAllow);
}
public PBSolverCPClauseLearning(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order,
boolean noRemove) {
super(learner, dsf, params, order, noRemove);
boolean noRemove, boolean skipAllow) {
super(learner, dsf, params, order, noRemove, skipAllow);
}
@Override
protected IConflict chooseConflict(PBConstr myconfl, int level) {
return ConflictMapReduceToClause.createConflict(myconfl, level,
noRemove, PostProcessToClause.instance());
noRemove, skipAllow, PostProcessToClause.instance(), stats);
}
@Override
......
......@@ -61,32 +61,33 @@ public class PBSolverCPLong extends PBSolverCP {
}
public PBSolverCPLong(LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, IOrder order, boolean noRemove) {
super(learner, dsf, order, noRemove);
PBDataStructureFactory dsf, IOrder order, boolean noRemove,
boolean skipAllow) {
super(learner, dsf, order, noRemove, skipAllow);
}
public PBSolverCPLong(LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order,
RestartStrategy restarter, boolean noRemove) {
super(learner, dsf, params, order, restarter, noRemove);
RestartStrategy restarter, boolean noRemove, boolean skipAllow) {
super(learner, dsf, params, order, restarter, noRemove, skipAllow);
}
public PBSolverCPLong(LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order,
boolean noRemove) {
super(learner, dsf, params, order, noRemove);
boolean noRemove, boolean skipAllow) {
super(learner, dsf, params, order, noRemove, skipAllow);
}
@Override
protected IConflict chooseConflict(PBConstr myconfl, int level) {
return ConflictMapReduceToClause.createConflict(myconfl, level,
noRemove);
noRemove, skipAllow, stats);
}
@Override
public String toString(String prefix) {
return super.toString(prefix) + "\n" + prefix
+ "Reduce coefficients of asserted PB constraints from BigInteger to Long and reduce to clauses during conflict analysis if necessary";
+ "Reduce coefficients of asserted PB constraints from BigInteger to Long and reduce to clauses during conflict analysis if necessary (ConflictMapReduceToClause) ";
}
}
......@@ -66,27 +66,28 @@ public class PBSolverCPLongDivideBy2 extends PBSolverCPLong {
public PBSolverCPLongDivideBy2(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, IOrder order, boolean noRemove) {
super(learner, dsf, order, noRemove);
PBDataStructureFactory dsf, IOrder order, boolean noRemove,
boolean skipAllow) {
super(learner, dsf, order, noRemove, skipAllow);
}
public PBSolverCPLongDivideBy2(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order,
RestartStrategy restarter, boolean noRemove) {
super(learner, dsf, params, order, restarter, noRemove);
RestartStrategy restarter, boolean noRemove, boolean skipAllow) {
super(learner, dsf, params, order, restarter, noRemove, skipAllow);
}
public PBSolverCPLongDivideBy2(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order,
boolean noRemove) {
super(learner, dsf, params, order, noRemove);
boolean noRemove, boolean skipAllow) {
super(learner, dsf, params, order, noRemove, skipAllow);
}
@Override
protected IConflict chooseConflict(PBConstr myconfl, int level) {
return ConflictMap.createConflict(myconfl, level, noRemove,
return ConflictMap.createConflict(myconfl, level, noRemove, skipAllow,
PostProcessDivideBy2.instance(), stats);
}
......
......@@ -11,6 +11,11 @@ import org.sat4j.pb.constraints.pb.PostProcessDivideBy2;
public class PBSolverCPLongDivideByGCD extends PBSolverCPLong {
/**
*
*/
private static final long serialVersionUID = 1L;
public PBSolverCPLongDivideByGCD(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, IOrder order) {
......@@ -35,30 +40,31 @@ public class PBSolverCPLongDivideByGCD extends PBSolverCPLong {
public PBSolverCPLongDivideByGCD(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, IOrder order, boolean noRemove) {
super(learner, dsf, order, noRemove);
PBDataStructureFactory dsf, IOrder order, boolean noRemove,
boolean skipAllow) {
super(learner, dsf, order, noRemove, skipAllow);
// TODO Auto-generated constructor stub
}
public PBSolverCPLongDivideByGCD(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order,
RestartStrategy restarter, boolean noRemove) {
super(learner, dsf, params, order, restarter, noRemove);
RestartStrategy restarter, boolean noRemove, boolean skipAllow) {
super(learner, dsf, params, order, restarter, noRemove, skipAllow);
// TODO Auto-generated constructor stub
}
public PBSolverCPLongDivideByGCD(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order,
boolean noRemove) {
super(learner, dsf, params, order, noRemove);
boolean noRemove, boolean skipAllow) {
super(learner, dsf, params, order, noRemove, skipAllow);
// TODO Auto-generated constructor stub
}
@Override
protected IConflict chooseConflict(PBConstr myconfl, int level) {
return ConflictMap.createConflict(myconfl, level, noRemove,
return ConflictMap.createConflict(myconfl, level, noRemove, skipAllow,
PostProcessDivideBy2.instance(), stats);
}
......
......@@ -38,7 +38,7 @@ import org.sat4j.pb.constraints.pb.IConflict;
import org.sat4j.pb.constraints.pb.PBConstr;
@SuppressWarnings("serial")
public class PBSolverCPLongReduceToCard extends PBSolverCP {
public class PBSolverCPLongReduceToCard extends PBSolverCPLong {
public PBSolverCPLongReduceToCard(
LearningStrategy<PBDataStructureFactory> learner,
......@@ -64,36 +64,38 @@ public class PBSolverCPLongReduceToCard extends PBSolverCP {
public PBSolverCPLongReduceToCard(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, IOrder order, boolean noRemove) {
super(learner, dsf, order, noRemove);
PBDataStructureFactory dsf, IOrder order, boolean noRemove,
boolean skipAllow) {
super(learner, dsf, order, noRemove, skipAllow);
// TODO Auto-generated constructor stub
}
public PBSolverCPLongReduceToCard(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order,
RestartStrategy restarter, boolean noRemove) {
super(learner, dsf, params, order, restarter, noRemove);
RestartStrategy restarter, boolean noRemove, boolean skipAllow) {
super(learner, dsf, params, order, restarter, noRemove, skipAllow);
// TODO Auto-generated constructor stub
}
public PBSolverCPLongReduceToCard(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order,
boolean noRemove) {
super(learner, dsf, params, order, noRemove);
boolean noRemove, boolean skipAllow) {
super(learner, dsf, params, order, noRemove, skipAllow);
// TODO Auto-generated constructor stub
}
@Override
protected IConflict chooseConflict(PBConstr myconfl, int level) {
return ConflictMapReduceToCard.createConflict(myconfl, level, noRemove);
return ConflictMapReduceToCard.createConflict(myconfl, level, noRemove,
skipAllow, stats);
}
@Override
public String toString(String prefix) {
return super.toString(prefix) + "\n" + prefix
+ "Reduce to cardinality constraint during conflict analysis if necessary";
+ "Reduce to cardinality constraint during conflict analysis if necessary (ConflictMapReduceToCard)";
}
}
......@@ -65,28 +65,35 @@ public class PBSolverCPLongRounding extends PBSolverCPLong {
public PBSolverCPLongRounding(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, IOrder order, boolean noRemove) {
super(learner, dsf, order, noRemove);
PBDataStructureFactory dsf, IOrder order, boolean noRemove,
boolean skipAllow) {
super(learner, dsf, order, noRemove, skipAllow);
}
public PBSolverCPLongRounding(
LearningStrategy<PBDataStructureFactory> learner,
PBDataStructureFactory dsf, SearchParams params, IOrder order,
RestartStrategy restarter, boolean noRemove) {
super(learner, dsf, params, order, restarter, noRemove);
RestartStrategy restarter, boolean noRemove, boolean skipAllow) {
super(learner, dsf, params, order, restarter, noRemove, skipAllow);
}
public PBSolverCPLongRounding(