Commit a5ae1b29 authored by Daniel Le Berre's avatar Daniel Le Berre

Rebuilt random solver.

parent aea58944
......@@ -46,6 +46,7 @@ import org.sat4j.minisat.learning.PercentLengthLearning;
import org.sat4j.minisat.orders.PhaseCachingAutoEraseStrategy;
import org.sat4j.minisat.orders.RSATLastLearnedClausesPhaseSelectionStrategy;
import org.sat4j.minisat.orders.RSATPhaseSelectionStrategy;
import org.sat4j.minisat.orders.RandomLiteralSelectionStrategy;
import org.sat4j.minisat.orders.RandomWalkDecorator;
import org.sat4j.minisat.orders.VarOrderHeap;
import org.sat4j.minisat.restarts.ArminRestarts;
......@@ -177,6 +178,23 @@ public final class SolverFactory extends ASolverFactory<ISolver> {
return solver;
}
/**
*
* @since 2.3.6
*/
public static ICDCL<DataStructureFactory> newRandomSolver() {
MiniSATLearning<DataStructureFactory> learning = new MiniSATLearning<DataStructureFactory>();
Solver<DataStructureFactory> solver = new Solver<DataStructureFactory>(
learning, new MixedDataStructureDanielWL(),
new RandomWalkDecorator(
new VarOrderHeap(new RandomLiteralSelectionStrategy()),
1.0),
new NoRestarts());
// solver.setSearchParams(new SearchParams(1.1, 100));
solver.setSimplifier(solver.EXPENSIVE_SIMPLIFICATION);
return solver;
}
/**
* @since 2.2
*/
......
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