Commit 1e4465b2 authored by Anne Parrain's avatar Anne Parrain

Allow divide-v1 option : always round coefficient of the propagating

literal to 1 (during conflict anaysis)
parent 3728be40
......@@ -35,15 +35,12 @@ import org.sat4j.pb.core.PBSolverStats;
public class ConflictMapRounding extends ConflictMap {
private final PBSolverStats stats;
/**
* @param cpb
* @param level
*/
public ConflictMapRounding(PBConstr cpb, int level, PBSolverStats stats) {
super(cpb, level);
this.stats = stats;
}
/**
......@@ -54,17 +51,37 @@ public class ConflictMapRounding extends ConflictMap {
public ConflictMapRounding(PBConstr cpb, int level, boolean noRemove,
PBSolverStats stats) {
super(cpb, level, noRemove);
this.stats = stats;
}
public static IConflict createConflict(PBConstr cpb, int level,
PBSolverStats stats) {
return new ConflictMapRounding(cpb, level, stats);
public ConflictMapRounding(PBConstr cpb, int level, boolean noRemove,
boolean skip, IPostProcess postProcessing,
IWeakeningStrategy weakeningStrategy, PBSolverStats stats) {
super(cpb, level, noRemove, skip, postProcessing, weakeningStrategy,
stats);
}
public static IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, PBSolverStats stats) {
return new ConflictMapRounding(cpb, level, noRemove, stats);
boolean noRemove, boolean skip, IPostProcess postProcessing,
IWeakeningStrategy weakeningStrategy, PBSolverStats stats) {
return new ConflictMapRounding(cpb, level, noRemove, skip,
postProcessing, weakeningStrategy, stats);
}
public static IConflictFactory factory() {
return new IConflictFactory() {
@Override
public IConflict createConflict(PBConstr cpb, int level,
boolean noRemove, boolean skip, IPostProcess postprocess,
IWeakeningStrategy weakeningStrategy, PBSolverStats stats) {
return ConflictMapRounding.createConflict(cpb, level, noRemove,
skip, postprocess, weakeningStrategy, stats);
}
@Override
public String toString() {
return "Always round the coefficient of the propagating literal to 1 during conflict analysis.";
}
};
}
static BigInteger ceildiv(BigInteger p, BigInteger q) {
......
......@@ -24,6 +24,7 @@ import org.sat4j.pb.constraints.pb.ConflictMapReduceByGCD;
import org.sat4j.pb.constraints.pb.ConflictMapReduceByPowersOf2;
import org.sat4j.pb.constraints.pb.ConflictMapReduceToCard;
import org.sat4j.pb.constraints.pb.ConflictMapReduceToClause;
import org.sat4j.pb.constraints.pb.ConflictMapRounding;
import org.sat4j.pb.constraints.pb.IWeakeningStrategy;
import org.sat4j.pb.constraints.pb.PostProcessToCard;
import org.sat4j.pb.constraints.pb.PostProcessToClause;
......@@ -231,6 +232,9 @@ public class KTHLauncher {
ConflictMapReduceToCard.factory());
break;
case "divide-v1":
cpsolver.setConflictFactory(
ConflictMapRounding.factory());
break;
case "divide-unless-equal":
case "divide-unless-divisor":
case "round-to-gcd":
......
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