Commit af075098 authored by Daniel Le Berre's avatar Daniel Le Berre
Browse files

Merge branch 'master' of https://gitlab.ow2.org/sat4j/sat4j

parents 5c40b7d8 6370076a
......@@ -189,7 +189,7 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
public static PBSolverCP newCompetPBCPRemoveSatisfiedMixedConstraintsLongMaxObjective() {
PBSolverCP s = newPBCP(new PBLongMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), false);
new VarOrderHeapObjective(), false, false);
return s;
}
......@@ -589,9 +589,10 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
}
private static PBSolverCP newPBCP(PBDataStructureFactory dsf, IOrder order,
boolean noRemove) {
boolean noRemove, boolean skipAllow) {
MiniSATLearning<PBDataStructureFactory> learning = new MiniSATLearning<PBDataStructureFactory>();
PBSolverCP solver = new PBSolverCP(learning, dsf, order, noRemove);
PBSolverCP solver = new PBSolverCP(learning, dsf, order, noRemove,
skipAllow);
learning.setDataStructureFactory(solver.getDSFactory());
learning.setVarActivityListener(solver);
solver.setRestartStrategy(new ArminRestarts());
......@@ -600,10 +601,11 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
}
private static PBSolverCP newPBCPReduceByPowersOf2(
PBDataStructureFactory dsf, IOrder order, boolean noRemove) {
PBDataStructureFactory dsf, IOrder order, boolean noRemove,
boolean skipAllow) {
MiniSATLearning<PBDataStructureFactory> learning = new MiniSATLearning<PBDataStructureFactory>();
PBSolverCP solver = new PBSolverCPReduceByPowersOf2(learning, dsf,
order, noRemove);
order, noRemove, skipAllow);
learning.setDataStructureFactory(solver.getDSFactory());
learning.setVarActivityListener(solver);
solver.setRestartStrategy(new ArminRestarts());
......@@ -612,10 +614,10 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
}
private static PBSolverCP newPBCPReduceByGCD(PBDataStructureFactory dsf,
IOrder order, boolean noRemove) {
IOrder order, boolean noRemove, boolean skipAllow) {
MiniSATLearning<PBDataStructureFactory> learning = new MiniSATLearning<PBDataStructureFactory>();
PBSolverCP solver = new PBSolverCPReduceByGCD(learning, dsf, order,
noRemove);
noRemove, skipAllow);
learning.setDataStructureFactory(solver.getDSFactory());
learning.setVarActivityListener(solver);
solver.setRestartStrategy(new ArminRestarts());
......@@ -624,9 +626,10 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
}
private static PBSolverCP newPBCPStar(PBDataStructureFactory dsf,
IOrder order, boolean noRemove) {
IOrder order, boolean noRemove, boolean skipAllow) {
MiniSATLearning<PBDataStructureFactory> learning = new MiniSATLearning<PBDataStructureFactory>();
PBSolverCP solver = new PBSolverCPLong(learning, dsf, order, noRemove);
PBSolverCP solver = new PBSolverCPLong(learning, dsf, order, noRemove,
skipAllow);
// PBSolverCP solver = new PBSolverCautious(learning, dsf, order,
// PBSolverCautious.BOUND);
learning.setDataStructureFactory(solver.getDSFactory());
......@@ -637,10 +640,11 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
}
private static PBSolverCP newPBCPStarClauseLearning(
PBDataStructureFactory dsf, IOrder order, boolean noRemove) {
PBDataStructureFactory dsf, IOrder order, boolean noRemove,
boolean skipAllow) {
MiniSATLearning<PBDataStructureFactory> learning = new MiniSATLearning<PBDataStructureFactory>();
PBSolverCP solver = new PBSolverCPClauseLearning(learning, dsf, order,
noRemove);
noRemove, skipAllow);
learning.setDataStructureFactory(solver.getDSFactory());
learning.setVarActivityListener(solver);
solver.setRestartStrategy(new ArminRestarts());
......@@ -649,10 +653,11 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
}
private static PBSolverCP newPBCPStarCardLearning(
PBDataStructureFactory dsf, IOrder order, boolean noRemove) {
PBDataStructureFactory dsf, IOrder order, boolean noRemove,
boolean skipAllow) {
MiniSATLearning<PBDataStructureFactory> learning = new MiniSATLearning<PBDataStructureFactory>();
PBSolverCP solver = new PBSolverCPCardLearning(learning, dsf, order,
noRemove);
noRemove, skipAllow);
learning.setDataStructureFactory(solver.getDSFactory());
learning.setVarActivityListener(solver);
solver.setRestartStrategy(new ArminRestarts());
......@@ -661,10 +666,10 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
}
private static PBSolverCP newPBCPStarDivideBy2(PBDataStructureFactory dsf,
IOrder order, boolean noRemove) {
IOrder order, boolean noRemove, boolean skipAllow) {
MiniSATLearning<PBDataStructureFactory> learning = new MiniSATLearning<PBDataStructureFactory>();
PBSolverCP solver = new PBSolverCPLongDivideBy2(learning, dsf, order,
noRemove);
noRemove, skipAllow);
learning.setDataStructureFactory(solver.getDSFactory());
learning.setVarActivityListener(solver);
solver.setRestartStrategy(new ArminRestarts());
......@@ -673,10 +678,10 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
}
private static PBSolverCP newPBCPStarDivideByGCD(PBDataStructureFactory dsf,
IOrder order, boolean noRemove) {
IOrder order, boolean noRemove, boolean skipAllow) {
MiniSATLearning<PBDataStructureFactory> learning = new MiniSATLearning<PBDataStructureFactory>();
PBSolverCP solver = new PBSolverCPLongDivideByGCD(learning, dsf, order,
noRemove);
noRemove, skipAllow);
learning.setDataStructureFactory(solver.getDSFactory());
learning.setVarActivityListener(solver);
solver.setRestartStrategy(new ArminRestarts());
......@@ -685,10 +690,10 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
}
private static PBSolverCP newPBCPStarRounding(PBDataStructureFactory dsf,
IOrder order, boolean noRemove) {
IOrder order, boolean noRemove, boolean skipAllow) {
MiniSATLearning<PBDataStructureFactory> learning = new MiniSATLearning<PBDataStructureFactory>();
PBSolverCP solver = new PBSolverCPLongRounding(learning, dsf, order,
noRemove);
noRemove, skipAllow);
learning.setDataStructureFactory(solver.getDSFactory());
learning.setVarActivityListener(solver);
solver.setRestartStrategy(new ArminRestarts());
......@@ -697,10 +702,11 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
}
private static PBSolverCP newPBCPStarReduceToCard(
PBDataStructureFactory dsf, IOrder order, boolean noRemove) {
PBDataStructureFactory dsf, IOrder order, boolean noRemove,
boolean skipAllow) {
MiniSATLearning<PBDataStructureFactory> learning = new MiniSATLearning<PBDataStructureFactory>();
PBSolverCP solver = new PBSolverCPLongReduceToCard(learning, dsf, order,
noRemove);
noRemove, skipAllow);
learning.setDataStructureFactory(solver.getDSFactory());
learning.setVarActivityListener(solver);
solver.setRestartStrategy(new ArminRestarts());
......@@ -709,7 +715,7 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
}
public static PBSolverCP newPBCP(PBDataStructureFactory dsf, IOrder order) {
return newPBCP(dsf, order, true);
return newPBCP(dsf, order, true, true);
}
private static PBSolverCP newPBCP(PBDataStructureFactory dsf) {
......@@ -733,48 +739,101 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
public static IPBSolver newCuttingPlanesReduceByPowersOf2() {
return newPBCPReduceByPowersOf2(
new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true);
new VarOrderHeapObjective(), true, false);
}
public static IPBSolver newCuttingPlanesReduceByGCD() {
return newPBCPReduceByGCD(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true);
new VarOrderHeapObjective(), true, false);
}
public static IPBSolver newCuttingPlanesStar() {
return newPBCPStar(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true);
new VarOrderHeapObjective(), true, false);
}
public static IPBSolver newCuttingPlanesStarRounding() {
return newPBCPStarRounding(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true);
new VarOrderHeapObjective(), true, false);
}
public static IPBSolver newCuttingPlanesStarReduceToCard() {
return newPBCPStarReduceToCard(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true);
new VarOrderHeapObjective(), true, false);
}
public static IPBSolver newCuttingPlanesStarClauseLearning() {
return newPBCPStarClauseLearning(
new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true);
new VarOrderHeapObjective(), true, false);
}
public static IPBSolver newCuttingPlanesStarCardLearning() {
return newPBCPStarCardLearning(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true);
new VarOrderHeapObjective(), true, false);
}
public static IPBSolver newCuttingPlanesStarDivideBy2() {
return newPBCPStarDivideBy2(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true);
new VarOrderHeapObjective(), true, false);
}
public static IPBSolver newCuttingPlanesStarDivideByGCD() {
return newPBCPStarDivideByGCD(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true);
new VarOrderHeapObjective(), true, false);
}
/**
* Same cutting planes based solver, with jan Elffer's skip of cutting
* planes activated
*
*/
public static IPBSolver newCuttingPlanesReduceByPowersOf2Skip() {
return newPBCPReduceByPowersOf2(
new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true, true);
}
public static IPBSolver newCuttingPlanesReduceByGCDSkip() {
return newPBCPReduceByGCD(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true, true);
}
public static IPBSolver newCuttingPlanesStarSkip() {
return newPBCPStar(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true, true);
}
public static IPBSolver newCuttingPlanesStarRoundingSkip() {
return newPBCPStarRounding(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true, true);
}
public static IPBSolver newCuttingPlanesStarReduceToCardSkip() {
return newPBCPStarReduceToCard(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true, true);
}
public static IPBSolver newCuttingPlanesStarClauseLearningSkip() {
return newPBCPStarClauseLearning(
new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true, true);
}
public static IPBSolver newCuttingPlanesStarCardLearningSkip() {
return newPBCPStarCardLearning(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true, true);
}
public static IPBSolver newCuttingPlanesStarDivideBy2Skip() {
return newPBCPStarDivideBy2(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true, true);
}
public static IPBSolver newCuttingPlanesStarDivideByGCDSkip() {
return newPBCPStarDivideByGCD(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true, true);
}
/**
......@@ -1059,11 +1118,25 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
return solver;
}
public static IPBSolver newInprocDetectCardsSkip() {
InprocCardConstrLearningSolver solver = (InprocCardConstrLearningSolver) SolverFactory
.newLazyInprocDetectCardsSkip();
solver.setDetectCardFromAllConstraintsInCflAnalysis(true);
return solver;
}
public static IPBSolver newLazyInprocDetectCards() {
return new InprocCardConstrLearningSolver(
new MiniSATLearning<PBDataStructureFactory>(),
new PBMaxClauseCardConstrDataStructure(), new VarOrderHeap(),
true);
true, false);
}
public static IPBSolver newLazyInprocDetectCardsSkip() {
return new InprocCardConstrLearningSolver(
new MiniSATLearning<PBDataStructureFactory>(),
new PBMaxClauseCardConstrDataStructure(), new VarOrderHeap(),
true, true);
}
}
\ No newline at end of file
......@@ -53,6 +53,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
......@@ -86,33 +88,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();
......@@ -274,6 +290,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 {
}