Commit 146c09d0 authored by Daniel Le Berre's avatar Daniel Le Berre

Refactoring to allow a better command line setup of the solvers.

parent 6cb70377
Pipeline #277 passed with stages
in 23 minutes and 45 seconds
...@@ -736,28 +736,28 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> { ...@@ -736,28 +736,28 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
return newCompetPBCPMixedConstraintsMinObjective(); return newCompetPBCPMixedConstraintsMinObjective();
} }
public static IPBSolver newCuttingPlanesReduceByPowersOf2() { public static PBSolverCP newCuttingPlanesReduceByPowersOf2() {
return newPBCPReduceByPowersOf2( return newPBCPReduceByPowersOf2(
new PBMaxClauseCardConstrDataStructure(), new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true, false); new VarOrderHeapObjective(), true, false);
} }
public static IPBSolver newCuttingPlanesReduceByGCD() { public static PBSolverCP newCuttingPlanesReduceByGCD() {
return newPBCPReduceByGCD(new PBMaxClauseCardConstrDataStructure(), return newPBCPReduceByGCD(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true, false); new VarOrderHeapObjective(), true, false);
} }
public static IPBSolver newCuttingPlanesStar() { public static PBSolverCP newCuttingPlanesStar() {
return newPBCPStar(new PBMaxClauseCardConstrDataStructure(), return newPBCPStar(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true, false); new VarOrderHeapObjective(), true, false);
} }
public static IPBSolver newCuttingPlanesStarRounding() { public static PBSolverCP newCuttingPlanesStarRounding() {
return newPBCPStarRounding(new PBMaxClauseCardConstrDataStructure(), return newPBCPStarRounding(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true, false); new VarOrderHeapObjective(), true, false);
} }
public static IPBSolver newCuttingPlanesStarReduceToCard() { public static PBSolverCP newCuttingPlanesStarReduceToCard() {
return newPBCPStarReduceToCard(new PBMaxClauseCardConstrDataStructure(), return newPBCPStarReduceToCard(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true, false); new VarOrderHeapObjective(), true, false);
} }
...@@ -773,12 +773,12 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> { ...@@ -773,12 +773,12 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
new VarOrderHeapObjective(), true, false); new VarOrderHeapObjective(), true, false);
} }
public static IPBSolver newCuttingPlanesStarDivideBy2() { public static PBSolverCP newCuttingPlanesStarDivideBy2() {
return newPBCPStarDivideBy2(new PBMaxClauseCardConstrDataStructure(), return newPBCPStarDivideBy2(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true, false); new VarOrderHeapObjective(), true, false);
} }
public static IPBSolver newCuttingPlanesStarDivideByGCD() { public static PBSolverCP newCuttingPlanesStarDivideByGCD() {
return newPBCPStarDivideByGCD(new PBMaxClauseCardConstrDataStructure(), return newPBCPStarDivideByGCD(new PBMaxClauseCardConstrDataStructure(),
new VarOrderHeapObjective(), true, false); new VarOrderHeapObjective(), true, false);
} }
......
...@@ -31,8 +31,6 @@ package org.sat4j.pb.constraints.pb; ...@@ -31,8 +31,6 @@ package org.sat4j.pb.constraints.pb;
import java.math.BigInteger; import java.math.BigInteger;
import java.util.*;
import org.sat4j.core.VecInt; 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;
...@@ -111,6 +109,18 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -111,6 +109,18 @@ public class ConflictMap extends MapPb implements IConflict {
stats); stats);
} }
public static IConflictFactory factory() {
return new IConflictFactory() {
@Override
public IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postprocess,
PBSolverStats stats) {
return ConflictMap.createConflict(cpb, level, noRemove, skip,
postprocess, stats);
}
};
}
ConflictMap(PBConstr cpb, int level) { ConflictMap(PBConstr cpb, int level) {
this(cpb, level, false, false, NoPostProcess.instance(), null); this(cpb, level, false, false, NoPostProcess.instance(), null);
} }
......
...@@ -6,18 +6,15 @@ public class ConflictMapReduceByGCD extends ConflictMap { ...@@ -6,18 +6,15 @@ public class ConflictMapReduceByGCD extends ConflictMap {
public ConflictMapReduceByGCD(PBConstr cpb, int level) { public ConflictMapReduceByGCD(PBConstr cpb, int level) {
super(cpb, level); super(cpb, level);
// TODO Auto-generated constructor stub
} }
public ConflictMapReduceByGCD(PBConstr cpb, int level, boolean noRemove) { public ConflictMapReduceByGCD(PBConstr cpb, int level, boolean noRemove) {
super(cpb, level, noRemove); super(cpb, level, noRemove);
// TODO Auto-generated constructor stub
} }
public ConflictMapReduceByGCD(PBConstr cpb, int level, boolean noRemove, public ConflictMapReduceByGCD(PBConstr cpb, int level, boolean noRemove,
boolean skip, IPostProcess postProcessing, PBSolverStats stats) { boolean skip, IPostProcess postProcessing, PBSolverStats stats) {
super(cpb, level, noRemove, skip, postProcessing, stats); super(cpb, level, noRemove, skip, postProcessing, stats);
// TODO Auto-generated constructor stub
} }
public static IConflict createConflict(PBConstr cpb, int level, public static IConflict createConflict(PBConstr cpb, int level,
...@@ -27,9 +24,22 @@ public class ConflictMapReduceByGCD extends ConflictMap { ...@@ -27,9 +24,22 @@ public class ConflictMapReduceByGCD extends ConflictMap {
} }
public static IConflict createConflict(PBConstr cpb, int level, public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, PBSolverStats stats) { boolean noRemove, boolean skip, IPostProcess postprocess,
PBSolverStats stats) {
return new ConflictMapReduceByGCD(cpb, level, noRemove, skip, return new ConflictMapReduceByGCD(cpb, level, noRemove, skip,
NoPostProcess.instance(), stats); postprocess, stats);
}
public static IConflictFactory factory() {
return new IConflictFactory() {
@Override
public IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postprocess,
PBSolverStats stats) {
return ConflictMapReduceByGCD.createConflict(cpb, level,
noRemove, skip, postprocess, stats);
}
};
} }
@Override @Override
......
...@@ -4,34 +4,29 @@ import org.sat4j.pb.core.PBSolverStats; ...@@ -4,34 +4,29 @@ import org.sat4j.pb.core.PBSolverStats;
public class ConflictMapReduceByPowersOf2 extends ConflictMap { 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, public ConflictMapReduceByPowersOf2(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postProcessing, boolean noRemove, boolean skip, IPostProcess postProcessing,
PBSolverStats stats) { PBSolverStats stats) {
super(cpb, level, noRemove, skip, 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, public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, PBSolverStats stats) { boolean noRemove, boolean skip, IPostProcess postprocess,
PBSolverStats stats) {
return new ConflictMapReduceByPowersOf2(cpb, level, noRemove, skip, return new ConflictMapReduceByPowersOf2(cpb, level, noRemove, skip,
NoPostProcess.instance(), stats); postprocess, stats);
}
public static IConflictFactory factory() {
return new IConflictFactory() {
@Override
public IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postprocess,
PBSolverStats stats) {
return ConflictMapReduceByPowersOf2.createConflict(cpb, level,
noRemove, skip, postprocess, stats);
}
};
} }
@Override @Override
......
...@@ -27,14 +27,15 @@ public class ConflictMapReduceToCard extends ConflictMap { ...@@ -27,14 +27,15 @@ public class ConflictMapReduceToCard extends ConflictMap {
} }
public ConflictMapReduceToCard(PBConstr cpb, int level, boolean noRemove, public ConflictMapReduceToCard(PBConstr cpb, int level, boolean noRemove,
boolean skip, PBSolverStats stats) { boolean skip, IPostProcess postprocess, PBSolverStats stats) {
super(cpb, level, noRemove, skip, stats); super(cpb, level, noRemove, skip, postprocess, stats);
// TODO Auto-generated constructor stub
} }
public static IConflict createConflict(PBConstr cpb, int level, public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, PBSolverStats stats) { boolean noRemove, boolean skip, IPostProcess postprocess,
return new ConflictMapReduceToCard(cpb, level, noRemove, skip, stats); PBSolverStats stats) {
return new ConflictMapReduceToCard(cpb, level, noRemove, skip,
postprocess, stats);
} }
public static IConflict createConflict(PBConstr cpb, int level) { public static IConflict createConflict(PBConstr cpb, int level) {
...@@ -46,6 +47,18 @@ public class ConflictMapReduceToCard extends ConflictMap { ...@@ -46,6 +47,18 @@ public class ConflictMapReduceToCard extends ConflictMap {
return new ConflictMapReduceToCard(cpb, level, noRemove); return new ConflictMapReduceToCard(cpb, level, noRemove);
} }
public static IConflictFactory factory() {
return new IConflictFactory() {
@Override
public IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postprocess,
PBSolverStats stats) {
return ConflictMapReduceToCard.createConflict(cpb, level,
noRemove, skip, postprocess, stats);
}
};
}
/** /**
* reduces the constraint defined by wpb until the result of the cutting * reduces the constraint defined by wpb until the result of the cutting
* plane is a conflict. this reduction returns a cardinality. * plane is a conflict. this reduction returns a cardinality.
...@@ -59,20 +72,11 @@ public class ConflictMapReduceToCard extends ConflictMap { ...@@ -59,20 +72,11 @@ public class ConflictMapReduceToCard extends ConflictMap {
@Override @Override
protected BigInteger reduceUntilConflict(int litImplied, int ind, protected BigInteger reduceUntilConflict(int litImplied, int ind,
BigInteger[] reducedCoefs, BigInteger degreeReduced, IWatchPb wpb) { BigInteger[] reducedCoefs, BigInteger degreeReduced, IWatchPb wpb) {
// BigInteger coefLitImplied = this.weightedLits.get(litImplied ^ 1);
// if ((reducedCoefs[0].multiply(coefLitImplied).compareTo(MAXVALUE) >
// 0)
// || (reducedCoefs[ind].multiply(this.weightedLits.getCoef(0))
// .compareTo(MAXVALUE) > 0)) {
degreeReduced = reduceToCard(ind, wpb, reducedCoefs, degreeReduced); degreeReduced = reduceToCard(ind, wpb, reducedCoefs, degreeReduced);
this.coefMultCons = this.weightedLits.get(litImplied ^ 1); this.coefMultCons = this.weightedLits.get(litImplied ^ 1);
this.coefMult = BigInteger.ONE; this.coefMult = BigInteger.ONE;
this.numberOfReductions++; this.numberOfReductions++;
return degreeReduced; return degreeReduced;
// } else
// return super.reduceUntilConflict(litImplied, ind, reducedCoefs,
// degreeReduced, wpb);
} }
private BigInteger reduceToCard(int ind, IWatchPb wpb, private BigInteger reduceToCard(int ind, IWatchPb wpb,
...@@ -102,22 +106,4 @@ public class ConflictMapReduceToCard extends ConflictMap { ...@@ -102,22 +106,4 @@ public class ConflictMapReduceToCard extends ConflictMap {
return BigInteger.valueOf(cpt + 1); return BigInteger.valueOf(cpt + 1);
} }
// private BigInteger reduceToCard(int ind, IWatchPb wpb,
// BigInteger[] reducedCoefs, BigInteger degreeReduced) {
// BigInteger somCoefs = BigInteger.ZERO;
// int cpt = 0;
// for (int i = 0; i < reducedCoefs.length; i++) {
// if (somCoefs.compareTo(degreeReduced) < 0) {
// somCoefs = somCoefs.add(reducedCoefs[i]);
// cpt++;
// }
// if (i == ind || wpb.getVocabulary().isFalsified(wpb.get(i))) {
// reducedCoefs[i] = BigInteger.ONE;
// } else {
// reducedCoefs[i] = BigInteger.ZERO;
// }
// }
// return BigInteger.valueOf(cpt);
// }
} }
...@@ -37,19 +37,16 @@ public final class ConflictMapReduceToClause extends ConflictMap { ...@@ -37,19 +37,16 @@ public final class ConflictMapReduceToClause extends ConflictMap {
public ConflictMapReduceToClause(PBConstr cpb, int level) { public ConflictMapReduceToClause(PBConstr cpb, int level) {
super(cpb, level); super(cpb, level);
// TODO Auto-generated constructor stub
} }
public ConflictMapReduceToClause(PBConstr cpb, int level, public ConflictMapReduceToClause(PBConstr cpb, int level,
boolean noRemove) { boolean noRemove) {
super(cpb, level, noRemove); super(cpb, level, noRemove);
// TODO Auto-generated constructor stub
} }
public ConflictMapReduceToClause(PBConstr cpb, int level, boolean noRemove, public ConflictMapReduceToClause(PBConstr cpb, int level, boolean noRemove,
boolean skip, PBSolverStats stats) { boolean skip, IPostProcess postprocess, PBSolverStats stats) {
super(cpb, level, noRemove, skip, stats); super(cpb, level, noRemove, skip, postprocess, stats);
// TODO Auto-generated constructor stub
} }
public static IConflict createConflict(PBConstr cpb, int level, public static IConflict createConflict(PBConstr cpb, int level,
...@@ -58,14 +55,28 @@ public final class ConflictMapReduceToClause extends ConflictMap { ...@@ -58,14 +55,28 @@ public final class ConflictMapReduceToClause extends ConflictMap {
} }
public static IConflict createConflict(PBConstr cpb, int level, public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, PBSolverStats stats) { boolean noRemove, boolean skip, IPostProcess postprocess,
return new ConflictMapReduceToClause(cpb, level, noRemove, skip, stats); PBSolverStats stats) {
return new ConflictMapReduceToClause(cpb, level, noRemove, skip,
postprocess, stats);
} }
public static IConflict createConflict(PBConstr cpb, int level) { public static IConflict createConflict(PBConstr cpb, int level) {
return new ConflictMapReduceToClause(cpb, level); return new ConflictMapReduceToClause(cpb, level);
} }
public static IConflictFactory factory() {
return new IConflictFactory() {
@Override
public IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postprocess,
PBSolverStats stats) {
return ConflictMapReduceToClause.createConflict(cpb, level,
noRemove, skip, postprocess, stats);
}
};
}
public static final BigInteger MAXVALUE = BigInteger public static final BigInteger MAXVALUE = BigInteger
.valueOf(Long.MAX_VALUE); .valueOf(Long.MAX_VALUE);
......
package org.sat4j.pb.constraints.pb;
import org.sat4j.pb.core.PBSolverStats;
public interface IConflictFactory {
IConflict createConflict(PBConstr cpb, int level, boolean noRemove,
boolean skip, IPostProcess postprocess, PBSolverStats stats);
}
...@@ -39,6 +39,9 @@ import org.sat4j.minisat.core.SearchParams; ...@@ -39,6 +39,9 @@ import org.sat4j.minisat.core.SearchParams;
import org.sat4j.minisat.restarts.MiniSATRestarts; import org.sat4j.minisat.restarts.MiniSATRestarts;
import org.sat4j.pb.constraints.pb.ConflictMap; import org.sat4j.pb.constraints.pb.ConflictMap;
import org.sat4j.pb.constraints.pb.IConflict; import org.sat4j.pb.constraints.pb.IConflict;
import org.sat4j.pb.constraints.pb.IConflictFactory;
import org.sat4j.pb.constraints.pb.IPostProcess;
import org.sat4j.pb.constraints.pb.NoPostProcess;
import org.sat4j.pb.constraints.pb.PBConstr; import org.sat4j.pb.constraints.pb.PBConstr;
import org.sat4j.specs.Constr; import org.sat4j.specs.Constr;
import org.sat4j.specs.IVec; import org.sat4j.specs.IVec;
...@@ -64,6 +67,10 @@ public class PBSolverCP extends PBSolver { ...@@ -64,6 +67,10 @@ public class PBSolverCP extends PBSolver {
*/ */
private boolean skipAllow = true; private boolean skipAllow = true;
private IConflictFactory conflictFactory = ConflictMap.factory();
private IPostProcess postprocess = NoPostProcess.instance();
/** /**
* @param acg * @param acg
* @param learner * @param learner
...@@ -192,8 +199,8 @@ public class PBSolverCP extends PBSolver { ...@@ -192,8 +199,8 @@ public class PBSolverCP extends PBSolver {
} }
protected IConflict chooseConflict(PBConstr myconfl, int level) { protected IConflict chooseConflict(PBConstr myconfl, int level) {
return ConflictMap.createConflict(myconfl, level, noRemove, skipAllow, return conflictFactory.createConflict(myconfl, level, noRemove,
stats); skipAllow, postprocess, stats);
} }
@Override @Override
...@@ -242,4 +249,20 @@ public class PBSolverCP extends PBSolver { ...@@ -242,4 +249,20 @@ public class PBSolverCP extends PBSolver {
this.noRemove = noRemove; this.noRemove = noRemove;
} }
public IConflictFactory getConflictFactory() {
return conflictFactory;
}
public void setConflictFactory(IConflictFactory conflictFactory) {
this.conflictFactory = conflictFactory;
}
public IPostProcess getPostprocess() {
return postprocess;
}
public void setPostprocess(IPostProcess postprocess) {
this.postprocess = postprocess;
}
} }
...@@ -4,7 +4,6 @@ import java.io.BufferedReader; ...@@ -4,7 +4,6 @@ import java.io.BufferedReader;
import java.io.IOException; import java.io.IOException;
import java.io.InputStreamReader; import java.io.InputStreamReader;
import java.net.URL; import java.net.URL;
import java.util.Map;
import org.apache.commons.cli.CommandLine; import org.apache.commons.cli.CommandLine;
import org.apache.commons.cli.CommandLineParser; import org.apache.commons.cli.CommandLineParser;
...@@ -17,6 +16,12 @@ import org.sat4j.pb.OptToPBSATAdapter; ...@@ -17,6 +16,12 @@ import org.sat4j.pb.OptToPBSATAdapter;
import org.sat4j.pb.PBSolverHandle; import org.sat4j.pb.PBSolverHandle;
import org.sat4j.pb.PseudoOptDecorator; import org.sat4j.pb.PseudoOptDecorator;
import org.sat4j.pb.SolverFactory; import org.sat4j.pb.SolverFactory;
import org.sat4j.pb.constraints.pb.ConflictMapReduceByGCD;
import org.sat4j.pb.constraints.pb.ConflictMapReduceByPowersOf2;
import org.sat4j.pb.constraints.pb.ConflictMapReduceToCard;
import org.sat4j.pb.constraints.pb.ConflictMapReduceToClause;
import org.sat4j.pb.constraints.pb.PostProcessToCard;
import org.sat4j.pb.constraints.pb.PostProcessToClause;
import org.sat4j.pb.core.PBSolverCP; import org.sat4j.pb.core.PBSolverCP;
import org.sat4j.pb.reader.OPBReader2012; import org.sat4j.pb.reader.OPBReader2012;
import org.sat4j.reader.ParseFormatException; import org.sat4j.reader.ParseFormatException;
...@@ -50,6 +55,8 @@ public class KTHLauncher { ...@@ -50,6 +55,8 @@ public class KTHLauncher {
"Type of constraints learned. Legal values are general-linear, cardinality, clause"); "Type of constraints learned. Legal values are general-linear, cardinality, clause");
options.addOption("wni", "weaken-nonimplied", true, options.addOption("wni", "weaken-nonimplied", true,
"Remove literals that are not implied/propagated by the assignment at the backjump level. Legal values are true or false."); "Remove literals that are not implied/propagated by the assignment at the backjump level. Legal values are true or false.");
options.addOption("division", "division-strategy", true,
"Detect if all the coefficients can be divided by a common number. Legal values are two, gcd or none.");
Option op = options.getOption("coeflim"); Option op = options.getOption("coeflim");
op.setArgName("limit"); op.setArgName("limit");
op = options.getOption("coeflim-small"); op = options.getOption("coeflim-small");
...@@ -106,6 +113,24 @@ public class KTHLauncher { ...@@ -106,6 +113,24 @@ public class KTHLauncher {
PBSolverCP solver = SolverFactory.newCuttingPlanes(); PBSolverCP solver = SolverFactory.newCuttingPlanes();
solver.setNoRemove(true); solver.setNoRemove(true);
solver.setSkipAllow(false); solver.setSkipAllow(false);
if (line.hasOption("division-strategy")) {
String value = line.getOptionValue("division-strategy");
switch (value.toLowerCase()) {
case "two":
solver.setConflictFactory(ConflictMapReduceByPowersOf2.factory());
break;
case "gcd":
solver.setConflictFactory(ConflictMapReduceByGCD.factory());
break;
case "none":
break;
default:
log(value
+ " is not a supported value for option division");
return;
}
}
if (line.hasOption("type-of-learned-constraint")) { if (line.hasOption("type-of-learned-constraint")) {
String value = line String value = line
.getOptionValue("type-of-learned-constraint"); .getOptionValue("type-of-learned-constraint");
...@@ -113,10 +138,10 @@ public class KTHLauncher { ...@@ -113,10 +138,10 @@ public class KTHLauncher {
case "general-linear": // default case, do nothing case "general-linear": // default case, do nothing
break; break;
case "cardinality": case "cardinality":
solver = SolverFactory.newCuttingPlanesStarCardLearning(); solver.setPostprocess(PostProcessToCard.instance());