Commit 63107adc authored by Daniel Le Berre's avatar Daniel Le Berre

Allow a more sober CPU consumption in Both PB solver.

parent c091d768
Pipeline #9336 passed with stages
in 112 minutes and 26 seconds
package org.sat4j.tools;
import org.sat4j.specs.ISolver;
/**
* Solver Decorator to prevent the solver to receive a programmatic timeout
* change.
*
* It is expected to be useful when using {@link org.sat4j.tools.ManyCore} to
* isolate the timeout of a particular solver compared to the general timeout
* given to the other solvers.
*
* @author leberre
*
*/
public class TimeoutIsolator<T extends ISolver> extends SolverDecorator<T> {
/**
*
*/
private static final long serialVersionUID = 1L;
public TimeoutIsolator(T solver) {
super(solver);
}
@Override
public void setTimeoutOnConflicts(int count) {
// ignore
}
@Override
public void setTimeout(int t) {
// ignore
}
@Override
public void setTimeoutMs(long t) {
// ignore
}
}
package org.sat4j.pb;
/**
* Solver Decorator to prevent the solver to receive a programmatic timeout
* change.
*
* It is expected to be useful when using {@link org.sat4j.tools.ManyCore} to
* isolate the timeout of a particular solver compared to the general timeout
* given to the other solvers.
*
* @author leberre
*
*/
public class PBTimeoutIsolator extends PBSolverDecorator {
/**
*
*/
private static final long serialVersionUID = 1L;
public PBTimeoutIsolator(IPBSolver solver) {
super(solver);
}
@Override
public void setTimeoutOnConflicts(int count) {
// ignore
}
@Override
public void setTimeout(int t) {
// ignore
}
@Override
public void setTimeoutMs(long t) {
// ignore
}
}
......@@ -869,6 +869,20 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
return new ManyCorePB<IPBSolver>(newResolution(), newCuttingPlanes());
}
/**
* Resolution and CuttingPlanes based solvers running in parallel. Does only
* make sense if run on a computer with several cores.
*
* @return a parallel solver using both resolution and cutting planes proof
* system.
*/
public static IPBSolver newSoberBoth() {
PBSolverCP cp = newCuttingPlanes();
cp.setTimeout(60);
return new ManyCorePB<IPBSolver>(newResolution(),
new PBTimeoutIsolator(cp));
}
/**
* Resolution and CuttingPlanesStar based solvers running in parallel. Does
* only make sense if run on a computer with several cores.
......
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