From 146c09d06eba40c5dae2cc65d3ae68c8c5e82806 Mon Sep 17 00:00:00 2001 From: Daniel Le Berre Date: Mon, 16 Oct 2017 16:17:10 +0200 Subject: [PATCH] Refactoring to allow a better command line setup of the solvers. --- .../main/java/org/sat4j/pb/SolverFactory.java | 14 +-- .../sat4j/pb/constraints/pb/ConflictMap.java | 14 ++- .../pb/ConflictMapReduceByGCD.java | 20 +++-- .../pb/ConflictMapReduceByPowersOf2.java | 35 ++++---- .../pb/ConflictMapReduceToCard.java | 50 ++++------- .../pb/ConflictMapReduceToClause.java | 25 ++++-- .../pb/constraints/pb/IConflictFactory.java | 9 ++ .../java/org/sat4j/pb/core/PBSolverCP.java | 27 +++++- .../main/java/org/sat4j/sat/KTHLauncher.java | 87 ++++++++++++++++--- 9 files changed, 194 insertions(+), 87 deletions(-) create mode 100644 org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/IConflictFactory.java diff --git a/org.sat4j.pb/src/main/java/org/sat4j/pb/SolverFactory.java b/org.sat4j.pb/src/main/java/org/sat4j/pb/SolverFactory.java index f68fbbb3..159e07ee 100644 --- a/org.sat4j.pb/src/main/java/org/sat4j/pb/SolverFactory.java +++ b/org.sat4j.pb/src/main/java/org/sat4j/pb/SolverFactory.java @@ -736,28 +736,28 @@ public final class SolverFactory extends ASolverFactory { return newCompetPBCPMixedConstraintsMinObjective(); } - public static IPBSolver newCuttingPlanesReduceByPowersOf2() { + public static PBSolverCP newCuttingPlanesReduceByPowersOf2() { return newPBCPReduceByPowersOf2( new PBMaxClauseCardConstrDataStructure(), new VarOrderHeapObjective(), true, false); } - public static IPBSolver newCuttingPlanesReduceByGCD() { + public static PBSolverCP newCuttingPlanesReduceByGCD() { return newPBCPReduceByGCD(new PBMaxClauseCardConstrDataStructure(), new VarOrderHeapObjective(), true, false); } - public static IPBSolver newCuttingPlanesStar() { + public static PBSolverCP newCuttingPlanesStar() { return newPBCPStar(new PBMaxClauseCardConstrDataStructure(), new VarOrderHeapObjective(), true, false); } - public static IPBSolver newCuttingPlanesStarRounding() { + public static PBSolverCP newCuttingPlanesStarRounding() { return newPBCPStarRounding(new PBMaxClauseCardConstrDataStructure(), new VarOrderHeapObjective(), true, false); } - public static IPBSolver newCuttingPlanesStarReduceToCard() { + public static PBSolverCP newCuttingPlanesStarReduceToCard() { return newPBCPStarReduceToCard(new PBMaxClauseCardConstrDataStructure(), new VarOrderHeapObjective(), true, false); } @@ -773,12 +773,12 @@ public final class SolverFactory extends ASolverFactory { new VarOrderHeapObjective(), true, false); } - public static IPBSolver newCuttingPlanesStarDivideBy2() { + public static PBSolverCP newCuttingPlanesStarDivideBy2() { return newPBCPStarDivideBy2(new PBMaxClauseCardConstrDataStructure(), new VarOrderHeapObjective(), true, false); } - public static IPBSolver newCuttingPlanesStarDivideByGCD() { + public static PBSolverCP newCuttingPlanesStarDivideByGCD() { return newPBCPStarDivideByGCD(new PBMaxClauseCardConstrDataStructure(), new VarOrderHeapObjective(), true, false); } diff --git a/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMap.java b/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMap.java index 78a58587..3e75eaca 100644 --- a/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMap.java +++ b/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMap.java @@ -31,8 +31,6 @@ package org.sat4j.pb.constraints.pb; import java.math.BigInteger; -import java.util.*; - import org.sat4j.core.VecInt; import org.sat4j.minisat.constraints.cnf.Lits; import org.sat4j.minisat.core.ILits; @@ -111,6 +109,18 @@ public class ConflictMap extends MapPb implements IConflict { 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) { this(cpb, level, false, false, NoPostProcess.instance(), null); } diff --git a/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMapReduceByGCD.java b/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMapReduceByGCD.java index 8e9e3b6a..253cf3a1 100644 --- a/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMapReduceByGCD.java +++ b/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMapReduceByGCD.java @@ -6,18 +6,15 @@ public class ConflictMapReduceByGCD extends ConflictMap { public ConflictMapReduceByGCD(PBConstr cpb, int level) { super(cpb, level); - // TODO Auto-generated constructor stub } public ConflictMapReduceByGCD(PBConstr cpb, int level, boolean noRemove) { super(cpb, level, noRemove); - // TODO Auto-generated constructor stub } public ConflictMapReduceByGCD(PBConstr cpb, int level, boolean noRemove, 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, @@ -27,9 +24,22 @@ public class ConflictMapReduceByGCD extends ConflictMap { } 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, - 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 diff --git a/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMapReduceByPowersOf2.java b/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMapReduceByPowersOf2.java index 557331b7..fc54c223 100644 --- a/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMapReduceByPowersOf2.java +++ b/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMapReduceByPowersOf2.java @@ -4,34 +4,29 @@ 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, boolean noRemove, 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 ConflictMapReduceByPowersOf2(cpb, level, true, - // NoPostProcess.instance(), stats); - // } - 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, - 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 diff --git a/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMapReduceToCard.java b/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMapReduceToCard.java index 0d0f9e6c..a6f9ffc2 100644 --- a/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMapReduceToCard.java +++ b/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMapReduceToCard.java @@ -27,14 +27,15 @@ public class ConflictMapReduceToCard extends ConflictMap { } public ConflictMapReduceToCard(PBConstr cpb, int level, boolean noRemove, - boolean skip, PBSolverStats stats) { - super(cpb, level, noRemove, skip, stats); - // TODO Auto-generated constructor stub + boolean skip, IPostProcess postprocess, PBSolverStats stats) { + super(cpb, level, noRemove, skip, postprocess, stats); } public static IConflict createConflict(PBConstr cpb, int level, - boolean noRemove, boolean skip, PBSolverStats stats) { - return new ConflictMapReduceToCard(cpb, level, noRemove, skip, stats); + boolean noRemove, boolean skip, IPostProcess postprocess, + PBSolverStats stats) { + return new ConflictMapReduceToCard(cpb, level, noRemove, skip, + postprocess, stats); } public static IConflict createConflict(PBConstr cpb, int level) { @@ -46,6 +47,18 @@ public class ConflictMapReduceToCard extends ConflictMap { 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 * plane is a conflict. this reduction returns a cardinality. @@ -59,20 +72,11 @@ public class ConflictMapReduceToCard extends ConflictMap { @Override protected BigInteger reduceUntilConflict(int litImplied, int ind, 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); this.coefMultCons = this.weightedLits.get(litImplied ^ 1); this.coefMult = BigInteger.ONE; this.numberOfReductions++; return degreeReduced; - // } else - // return super.reduceUntilConflict(litImplied, ind, reducedCoefs, - // degreeReduced, wpb); } private BigInteger reduceToCard(int ind, IWatchPb wpb, @@ -102,22 +106,4 @@ public class ConflictMapReduceToCard extends ConflictMap { 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); - // } - } diff --git a/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMapReduceToClause.java b/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMapReduceToClause.java index d4e95e4a..303b5d47 100644 --- a/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMapReduceToClause.java +++ b/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/ConflictMapReduceToClause.java @@ -37,19 +37,16 @@ public final class ConflictMapReduceToClause extends ConflictMap { public ConflictMapReduceToClause(PBConstr cpb, int level) { super(cpb, level); - // TODO Auto-generated constructor stub } 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 + boolean skip, IPostProcess postprocess, PBSolverStats stats) { + super(cpb, level, noRemove, skip, postprocess, stats); } public static IConflict createConflict(PBConstr cpb, int level, @@ -58,14 +55,28 @@ public final class ConflictMapReduceToClause extends ConflictMap { } public static IConflict createConflict(PBConstr cpb, int level, - boolean noRemove, boolean skip, PBSolverStats stats) { - return new ConflictMapReduceToClause(cpb, level, noRemove, skip, stats); + boolean noRemove, boolean skip, IPostProcess postprocess, + PBSolverStats stats) { + return new ConflictMapReduceToClause(cpb, level, noRemove, skip, + postprocess, stats); } public static IConflict createConflict(PBConstr cpb, int 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 .valueOf(Long.MAX_VALUE); diff --git a/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/IConflictFactory.java b/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/IConflictFactory.java new file mode 100644 index 00000000..9b73974f --- /dev/null +++ b/org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/IConflictFactory.java @@ -0,0 +1,9 @@ +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); +} diff --git a/org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverCP.java b/org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverCP.java index e51e3782..37c9fc9b 100644 --- a/org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverCP.java +++ b/org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverCP.java @@ -39,6 +39,9 @@ import org.sat4j.minisat.core.SearchParams; import org.sat4j.minisat.restarts.MiniSATRestarts; import org.sat4j.pb.constraints.pb.ConflictMap; 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.specs.Constr; import org.sat4j.specs.IVec; @@ -64,6 +67,10 @@ public class PBSolverCP extends PBSolver { */ private boolean skipAllow = true; + private IConflictFactory conflictFactory = ConflictMap.factory(); + + private IPostProcess postprocess = NoPostProcess.instance(); + /** * @param acg * @param learner @@ -192,8 +199,8 @@ public class PBSolverCP extends PBSolver { } protected IConflict chooseConflict(PBConstr myconfl, int level) { - return ConflictMap.createConflict(myconfl, level, noRemove, skipAllow, - stats); + return conflictFactory.createConflict(myconfl, level, noRemove, + skipAllow, postprocess, stats); } @Override @@ -242,4 +249,20 @@ public class PBSolverCP extends PBSolver { 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; + } + } diff --git a/org.sat4j.sat/src/main/java/org/sat4j/sat/KTHLauncher.java b/org.sat4j.sat/src/main/java/org/sat4j/sat/KTHLauncher.java index 633ccaff..2fb0c416 100644 --- a/org.sat4j.sat/src/main/java/org/sat4j/sat/KTHLauncher.java +++ b/org.sat4j.sat/src/main/java/org/sat4j/sat/KTHLauncher.java @@ -4,7 +4,6 @@ import java.io.BufferedReader; import java.io.IOException; import java.io.InputStreamReader; import java.net.URL; -import java.util.Map; import org.apache.commons.cli.CommandLine; import org.apache.commons.cli.CommandLineParser; @@ -17,6 +16,12 @@ import org.sat4j.pb.OptToPBSATAdapter; import org.sat4j.pb.PBSolverHandle; import org.sat4j.pb.PseudoOptDecorator; 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.reader.OPBReader2012; import org.sat4j.reader.ParseFormatException; @@ -50,6 +55,8 @@ public class KTHLauncher { "Type of constraints learned. Legal values are general-linear, cardinality, clause"); 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."); + 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"); op.setArgName("limit"); op = options.getOption("coeflim-small"); @@ -106,6 +113,24 @@ public class KTHLauncher { PBSolverCP solver = SolverFactory.newCuttingPlanes(); solver.setNoRemove(true); 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")) { String value = line .getOptionValue("type-of-learned-constraint"); @@ -113,10 +138,10 @@ public class KTHLauncher { case "general-linear": // default case, do nothing break; case "cardinality": - solver = SolverFactory.newCuttingPlanesStarCardLearning(); + solver.setPostprocess(PostProcessToCard.instance()); break; case "clause": - solver = SolverFactory.newCuttingPlanesStarClauseLearning(); + solver.setPostprocess(PostProcessToClause.instance()); break; default: log(value @@ -139,7 +164,29 @@ public class KTHLauncher { return; } } - + if (line.hasOption("round-reason")) { + String value = line.getOptionValue("round-reason"); + switch (value) { + case "never": + // by default + break; + case "clausal": + solver.setConflictFactory(ConflictMapReduceToClause.factory()); + break; + case "cardinality": + solver.setConflictFactory(ConflictMapReduceToCard.factory()); + break; + case "divide-v1": + case "divide-unless-equal": + case "divide-unless-divisor": + case "round-to-gcd": + default: + log(value + + " is not a supported value for option round-reason"); + return; + } + return; + } // validate that block-size has been set if (line.hasOption("coeflim")) { log("coeflim option is unsupported at the moment"); @@ -155,17 +202,33 @@ public class KTHLauncher { log("find-best-divisor-when-dividing-for-overflow option is unsupported at the moment"); return; } - if (line.hasOption("round-reason")) { - log("round-reason option is unsupported at the moment"); - return; - } if (line.hasOption("rounding-weaken-priority")) { - log("rounding-weaken-priority option is unsupported at the moment"); - return; + String value = line.getOptionValue("rounding-weaken-priority"); + switch (value) { + case "unassigned": + // by default + break; + case "satisfied": + case "any": + default: + log(value + + " is not a supported value for option rounding-weaken-priority"); + return; + } } if (line.hasOption("weaken-nonimplied")) { - log("weaken-nonimplied option is unsupported at the moment"); - return; + String value = line.getOptionValue("rounding-weaken-priority"); + switch (value) { + case "false": + // by default + break; + case "true": + case "round": + default: + log(value + + " is not a supported value for option weaken-nonimplied"); + return; + } } System.out.println(solver.toString("c ")); String[] leftArgs = line.getArgs(); -- GitLab