Commit f4790fb8 authored by Romain Wallon's avatar Romain Wallon

Adds a slack based LCDS

parent a5f75884
Pipeline #9327 canceled with stages
......@@ -79,6 +79,12 @@ public class PBGlucoseLCDS<D extends DataStructureFactory>
new RatioCoefficientsDegreeLBDComputerStrategy());
}
public static <D extends DataStructureFactory> LearnedConstraintsDeletionStrategy newSlack(
Solver<D> solver, ConflictTimer timer) {
return new PBGlucoseLCDS<D>(solver, timer,
new SlackLBDComputerStrategy());
}
@Override
public void init() {
super.init();
......
package org.sat4j.pb.lcds;
import java.math.BigInteger;
import org.sat4j.minisat.core.ILits;
import org.sat4j.pb.constraints.pb.PBConstr;
public class SlackLBDComputerStrategy implements ILBDComputerStrategy {
@Override
public void init(int howmany) {
// TODO Auto-generated method stub
}
@Override
public int computeLBD(ILits voc, PBConstr constr, int propagated) {
BigInteger slack = constr.getSumCoefs().subtract(constr.getDegree());
if (slack.bitLength() < Integer.SIZE) {
return slack.intValue();
}
return Integer.MAX_VALUE;
}
}
......@@ -502,6 +502,11 @@ public class KTHLauncher {
.newRatio(cpsolver, timer);
cpsolver.setLearnedConstraintsDeletionStrategy(lcds);
} else if ("slack".equals(value)) {
LearnedConstraintsDeletionStrategy lcds = PBGlucoseLCDS
.newSlack(cpsolver, timer);
cpsolver.setLearnedConstraintsDeletionStrategy(lcds);
} else {
log(value
+ " is not a supported value for option deletion-strategy");
......
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