Commit 3dfc50b4 authored by Daniel Le Berre's avatar Daniel Le Berre

Allow MaxHS to be used on the command line of the maxsat solver (-hs

option).
parent ca8ba743
......@@ -86,7 +86,8 @@ public class GenericOptLauncher extends AbstractLauncher {
"kind of problem: minone, maxsat, etc.");
options.addOption("i", "incomplete", false,
"incomplete mode for maxsat");
options.addOption("I", "inner mode", false, "optimize using inner mode");
options.addOption("I", "inner mode", false,
"optimize using inner mode");
options.addOption("c", "clean databases", false,
"clean up the database at root level");
options.addOption("k", "keep Hot", false,
......@@ -99,8 +100,11 @@ public class GenericOptLauncher extends AbstractLauncher {
"Do not display a solution line (useful if the solution is large)");
options.addOption("l", "lower bounding", false,
"search solution by lower bounding instead of by upper bounding");
options.addOption("hs", "MaxHS Like", false,
"search solution using a MaxHS like approach");
options.addOption("m", "mystery", false, "mystery option");
options.addOption("B", "External&Internal", false, "External&Internal optimization");
options.addOption("B", "External&Internal", false,
"External&Internal optimization");
return options;
}
......@@ -127,7 +131,6 @@ public class GenericOptLauncher extends AbstractLauncher {
return reader;
}
@Override
protected String getInstanceName(String[] args) {
return args[args.length - 1];
......@@ -179,6 +182,9 @@ public class GenericOptLauncher extends AbstractLauncher {
if (cmd.hasOption("l")) {
asolver = new ConstraintRelaxingPseudoOptDecorator(
this.wmsd);
} else if (cmd.hasOption("hs")) {
asolver = org.sat4j.maxsat.SolverFactory.newMaxHSLike();
setLauncherMode(ILauncherMode.DECISION);
} else if (cmd.hasOption("I")){
this.wmsd.setSearchListener(new SearchOptimizerListener(ILauncherMode.DECISION));
setLauncherMode(ILauncherMode.DECISION);
......@@ -231,8 +237,7 @@ public class GenericOptLauncher extends AbstractLauncher {
@Override
protected IProblem readProblem(String problemname)
throws ParseFormatException, IOException,
ContradictionException {
throws ParseFormatException, IOException, ContradictionException {
super.readProblem(problemname);
return solver;
}
......
......@@ -220,6 +220,9 @@ public class MaxHSLikeSolver extends SolverDecorator<ISolver>
public boolean isSatisfiable() throws TimeoutException {
IVecInt hs = new VecInt(hsfinder.findModel());
while (!decorated().isSatisfiable(hs)) {
if (isVerbose()) {
System.out.print(".");
}
IVecInt core = decorated().unsatExplanation();
IVecInt clause = new VecInt(core.size());
for (IteratorInt it = core.iterator(); it.hasNext();) {
......@@ -245,4 +248,14 @@ public class MaxHSLikeSolver extends SolverDecorator<ISolver>
return hsfinder.getObjectiveFunction().calculateDegree(hsfinder);
}
@Override
public String toString(String prefix) {
return prefix+"MaxHS like optimization"+System.lineSeparator()+super.toString(prefix);
}
@Override
public String toString() {
return "MaxHS like optimization "+super.toString();
}
}
......@@ -38,6 +38,7 @@ import org.sat4j.minisat.learning.MiniSATLearning;
import org.sat4j.minisat.orders.VarOrderHeap;
import org.sat4j.minisat.restarts.MiniSATRestarts;
import org.sat4j.pb.IPBSolver;
import org.sat4j.specs.ISolver;
public class SolverFactory extends ASolverFactory<IPBSolver> {
......@@ -105,4 +106,8 @@ public class SolverFactory extends ASolverFactory<IPBSolver> {
public static IPBSolver newLight() {
return org.sat4j.pb.SolverFactory.newLight();
}
public static ISolver newMaxHSLike() {
return new MaxHSLikeSolver(newDefault(), newDefault());
}
}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment