Commit 24b06390 authored by Daniel Le Berre's avatar Daniel Le Berre
Browse files

Greedy OPB solver

parent 9c04ce7c
Pipeline #15789 passed with stages
in 40 minutes and 39 seconds
...@@ -39,6 +39,7 @@ import org.sat4j.minisat.learning.MiniSATLearning; ...@@ -39,6 +39,7 @@ import org.sat4j.minisat.learning.MiniSATLearning;
import org.sat4j.minisat.learning.NoLearningButHeuristics; import org.sat4j.minisat.learning.NoLearningButHeuristics;
import org.sat4j.minisat.orders.PhaseInLastLearnedClauseSelectionStrategy; import org.sat4j.minisat.orders.PhaseInLastLearnedClauseSelectionStrategy;
import org.sat4j.minisat.orders.RSATPhaseSelectionStrategy; import org.sat4j.minisat.orders.RSATPhaseSelectionStrategy;
import org.sat4j.minisat.orders.RandomWalkDecorator;
import org.sat4j.minisat.orders.UserFixedPhaseSelectionStrategy; import org.sat4j.minisat.orders.UserFixedPhaseSelectionStrategy;
import org.sat4j.minisat.orders.VarOrderHeap; import org.sat4j.minisat.orders.VarOrderHeap;
import org.sat4j.minisat.restarts.ArminRestarts; import org.sat4j.minisat.restarts.ArminRestarts;
...@@ -1207,6 +1208,13 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> { ...@@ -1207,6 +1208,13 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
return solver; return solver;
} }
public static IPBSolver newCuttingPlanesGreedy() {
PBSolverCP solver = newCuttingPlanes();
solver.setOrder(
new RandomWalkDecorator((VarOrderHeap) solver.getOrder(), 1.0));
return solver;
}
public static IPBSolver newPartialRoundingSatPOS2020() { public static IPBSolver newPartialRoundingSatPOS2020() {
PBSolverCP solver = (PBSolverCP) newPartialRoundingSat(); PBSolverCP solver = (PBSolverCP) newPartialRoundingSat();
......
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