Commit 4dce0671 authored by leberre's avatar leberre

Fixed another issue reported by Miroslav.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@299 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent 2d6547bc
......@@ -461,6 +461,27 @@ public class SolverFactory extends ASolverFactory<IPBSolver> {
return newPBCP(dsf, new VarOrderHeap<ILits>());
}
/**
* Cutting Planes based solver.
* The inference during conflict analysis is based on cutting planes instead of resolution
* as in a SAT solver.
*
* @return the best available cutting planes based solver of the library.
*/
public static IPBSolver newCuttingPlanes() {
return newCompetPBCPMixedConstraintsObjective();
}
/**
* Resolution based solver (i.e. classic SAT solver able to handle generic constraints.
* No specific inference mechanism.
*
* @return the best available resolution based solver of the library.
*/
public static IPBSolver newResolution() {
return newCompetPBCPMixedConstraintsObjective();
}
/**
* Default solver of the SolverFactory. This solver is meant to be used on
* challenging SAT benchmarks.
......@@ -470,8 +491,7 @@ public class SolverFactory extends ASolverFactory<IPBSolver> {
* instance of ASolverFactory.
*/
public static IPBSolver newDefault() {
return newCompetPBCPMixedConstraintsObjective();
//return newCompetPBKillerClassic();
return newCompetPBResMixedConstraintsObjectiveExpSimp();
}
@Override
......
......@@ -221,8 +221,8 @@ public class OPBReader2007 extends OPBReader2006 {
String[] splitted = rest.trim().split(" ");
if (splitted[0].equals("#product=")) {
nbProducts = Integer.parseInt(splitted[1]);
nbVars += nbProducts;
nbConstr += 2 * nbProducts;
// nbVars += nbProducts;
// nbConstr += 2 * nbProducts;
}
// if (splitted[2].equals("sizeproduct="))
......
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