Commit 7ce27840 authored by Romain Wallon's avatar Romain Wallon

Ads some more bumping and LCD strategies

parent 3c078bdd
Pipeline #9137 passed with stages
in 102 minutes and 27 seconds
......@@ -149,4 +149,9 @@ public final class AtLeastPB extends AtLeast implements PBConstr {
return stb.toString();
}
@Override
public BigInteger getSumCoefs() {
return BigInteger.valueOf(size());
}
}
......@@ -78,4 +78,9 @@ public final class LearntBinaryClausePB extends LearntBinaryClause
stb.append(" >= 1");
return stb.toString();
}
@Override
public BigInteger getSumCoefs() {
return BigInteger.valueOf(size());
}
}
......@@ -99,4 +99,9 @@ public final class LearntHTClausePB extends LearntHTClause implements PBConstr {
return stb.toString();
}
@Override
public BigInteger getSumCoefs() {
return BigInteger.valueOf(size());
}
}
......@@ -605,5 +605,9 @@ public final class MaxWatchPbLong extends WatchPbLong {
return cstr.dump();
}
@Override
public BigInteger getSumCoefs() {
return cstr.getSumCoefs();
}
}
}
......@@ -217,4 +217,9 @@ public final class MinWatchCardPB extends MinWatchCard implements PBConstr {
return stb.toString();
}
@Override
public BigInteger getSumCoefs() {
return BigInteger.valueOf(size());
}
}
......@@ -100,4 +100,9 @@ public final class OriginalBinaryClausePB extends OriginalBinaryClause
return stb.toString();
}
@Override
public BigInteger getSumCoefs() {
return BigInteger.valueOf(size());
}
}
......@@ -103,4 +103,9 @@ public final class OriginalHTClausePB extends OriginalHTClause
stb.append(" >= 1");
return stb.toString();
}
@Override
public BigInteger getSumCoefs() {
return BigInteger.valueOf(size());
}
}
......@@ -41,15 +41,17 @@ import org.sat4j.specs.IVecInt;
*/
public interface PBConstr extends Constr {
BigInteger getCoef(int literal);
BigInteger getCoef(int literal);
BigInteger getDegree();
BigInteger getDegree();
ILits getVocabulary();
ILits getVocabulary();
int[] getLits();
int[] getLits();
BigInteger[] getCoefs();
BigInteger[] getCoefs();
IVecInt computeAnImpliedClause();
IVecInt computeAnImpliedClause();
BigInteger getSumCoefs();
}
......@@ -82,4 +82,9 @@ public final class UnitClausePB extends UnitClause implements PBConstr {
stb.append(" >= 1");
return stb.toString();
}
@Override
public BigInteger getSumCoefs() {
return BigInteger.valueOf(size());
}
}
......@@ -64,4 +64,9 @@ public class UnitClausesPB extends UnitClauses implements PBConstr {
public IVecInt computeAnImpliedClause() {
throw new UnsupportedOperationException();
}
@Override
public BigInteger getSumCoefs() {
return BigInteger.ONE;
}
}
......@@ -722,4 +722,9 @@ public abstract class WatchPb
}
return stb.toString();
}
@Override
public BigInteger getSumCoefs() {
return sumcoefs;
}
}
......@@ -729,4 +729,8 @@ public abstract class WatchPbLong
}
return stb.toString();
}
public BigInteger getSumCoefs() {
return BigInteger.valueOf(sumcoefs);
}
}
......@@ -759,4 +759,9 @@ public abstract class WatchPbLongCP
}
return stb.toString();
}
@Override
public BigInteger getSumCoefs() {
return BigInteger.valueOf(sumcoefs);
}
}
/**
*
*/
package org.sat4j.pb.lcds;
import org.sat4j.minisat.core.ILits;
import org.sat4j.pb.constraints.pb.PBConstr;
/**
* @author wallon
*
*/
public class DegreeSizeLBDComputerStrategy implements ILBDComputerStrategy {
@Override
public void init(int howmany) {
// TODO Auto-generated method stub
}
@Override
public int computeLBD(ILits voc, PBConstr constr, int propagated) {
return constr.getDegree().bitLength();
}
}
......@@ -67,6 +67,18 @@ public class PBGlucoseLCDS<D extends DataStructureFactory>
new DegreeLBDComputerStrategy());
}
public static <D extends DataStructureFactory> LearnedConstraintsDeletionStrategy newDegreeSize(
Solver<D> solver, ConflictTimer timer) {
return new PBGlucoseLCDS<D>(solver, timer,
new DegreeSizeLBDComputerStrategy());
}
public static <D extends DataStructureFactory> LearnedConstraintsDeletionStrategy newRatio(
Solver<D> solver, ConflictTimer timer) {
return new PBGlucoseLCDS<D>(solver, timer,
new RatioCoefficientsDegreeLBDComputerStrategy());
}
@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;
/**
* @author wallon
*
*/
public class RatioCoefficientsDegreeLBDComputerStrategy
implements ILBDComputerStrategy {
@Override
public void init(int howmany) {
// TODO Auto-generated method stub
}
@Override
public int computeLBD(ILits voc, PBConstr constr, int propagated) {
BigInteger sum = constr.getSumCoefs();
BigInteger degree = constr.getDegree();
BigInteger ratio = sum.divide(degree);
if (ratio.bitLength() < Integer.SIZE) {
return ratio.intValue();
}
return Integer.MAX_VALUE;
}
}
......@@ -8,28 +8,35 @@ public enum Bumper implements IBumper {
ANY {
@Override
boolean isBumpable(ILits voc, int i) {
boolean isBumpable(ILits voc, int i, int p) {
return true;
}
},
ASSIGNED {
@Override
boolean isBumpable(ILits voc, int i) {
boolean isBumpable(ILits voc, int i, int p) {
return !voc.isUnassigned(i);
}
},
FALSIFIED {
@Override
boolean isBumpable(ILits voc, int i) {
boolean isBumpable(ILits voc, int i, int p) {
return voc.isFalsified(i);
}
},
FALSIFIED_AND_PROPAGATED {
@Override
boolean isBumpable(ILits voc, int i, int p) {
return voc.isFalsified(i) || (voc.getLevel(i) == voc.getLevel(p));
}
};
public void varBumpActivity(ILits voc, BumpStrategy bumpStrategy,
IOrder order, PBConstr constr, int i, int propagated) {
if (isBumpable(voc, constr.get(i))) {
if (isBumpable(voc, constr.get(i), constr.get(propagated))) {
bumpStrategy.varBumpActivity(order, constr, i);
}
}
......@@ -39,6 +46,6 @@ public enum Bumper implements IBumper {
// Everything has already been done.
}
abstract boolean isBumpable(ILits voc, int i);
abstract boolean isBumpable(ILits voc, int i, int p);
}
/**
*
*/
package org.sat4j.pb.orders;
import java.math.BigInteger;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.IOrder;
import org.sat4j.pb.constraints.pb.PBConstr;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.IteratorInt;
/**
*
*/
public class BumperEffectiveAndPropagated implements IBumper {
private int propagatedLit;
private BigInteger constrDegree;
private final IVecInt bumpableCandidates = new VecInt();
private BumpStrategy bumpStrategy;
@Override
public void varBumpActivity(ILits voc, BumpStrategy bStrategy, IOrder order,
PBConstr constr, int lit, int propagated) {
if (lit == 0) {
// A new constraint is being bumped.
constrDegree = constr.getDegree();
bumpableCandidates.clear();
bumpStrategy = bStrategy;
propagatedLit = constr.get(propagated);
}
int currentLit = constr.get(lit);
if ((lit == propagated) || (voc.isSatisfied(currentLit)
&& voc.getLevel(currentLit) == voc.getLevel(propagated))) {
// The implied literals are always bumped.
bStrategy.varBumpActivity(order, constr, lit);
} else if (!voc.isFalsified(currentLit)) {
// Weakening on this literal preserves the propagation.
constrDegree = constrDegree.subtract(constr.getCoef(lit));
} else {
// The literal may be effective.
bumpableCandidates.push(lit);
}
}
@Override
public void postBumpActivity(IOrder order, PBConstr constr) {
for (IteratorInt it = bumpableCandidates.iterator(); it.hasNext();) {
int v = it.next();
if (constr.getCoef(v).compareTo(constrDegree) >= 0) {
bumpStrategy.varBumpActivity(order, constr, v);
} else {
break;
}
}
}
@Override
public String toString() {
return "EFFECTIVE AND PROPAGATED";
}
}
package org.sat4j.pb.orders;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.IOrder;
import org.sat4j.pb.constraints.pb.PBConstr;
public class DoubleBumpClashingLiteralsDecorator implements IBumper {
private final IBumper decorated;
public DoubleBumpClashingLiteralsDecorator(IBumper decorated) {
this.decorated = decorated;
}
@Override
public void varBumpActivity(ILits voc, BumpStrategy bumpStrategy,
IOrder order, PBConstr constr, int i, int propagated) {
decorated.varBumpActivity(voc, bumpStrategy, order, constr, i,
propagated);
bumpStrategy.varBumpActivity(order, constr, i);
}
@Override
public void postBumpActivity(IOrder order, PBConstr constr) {
decorated.postBumpActivity(order, constr);
}
}
......@@ -42,12 +42,14 @@ import org.sat4j.pb.constraints.pb.PreProcessReduceConflict;
import org.sat4j.pb.constraints.pb.SkipStrategy;
import org.sat4j.pb.core.PBDataStructureFactory;
import org.sat4j.pb.core.PBSolverCP;
import org.sat4j.pb.lcds.NullLCDS;
import org.sat4j.pb.lcds.PBActivityLCDS;
import org.sat4j.pb.lcds.PBGlucoseLCDS;
import org.sat4j.pb.orders.BumpStrategy;
import org.sat4j.pb.orders.Bumper;
import org.sat4j.pb.orders.BumperEffective;
import org.sat4j.pb.orders.BumperEffectiveAndPropagated;
import org.sat4j.pb.orders.DoubleBumpClashingLiteralsDecorator;
import org.sat4j.pb.orders.IBumper;
import org.sat4j.pb.reader.OPBReader2012;
import org.sat4j.pb.restarts.GrowingCoefficientRestarts;
import org.sat4j.pb.tools.InprocCardConstrLearningSolver;
......@@ -101,8 +103,10 @@ public class KTHLauncher {
"Bumping strategy to apply, among one, degree, coefficient, ratio");
options.addOption("br", "bumper", true,
"Literal bumper, among any, assigned and falsified");
options.addOption("lcds", "deletion-strategy", true,
"Learned constraint deletion strategy, among lbd, assigned, unassigned-same, unassigned-different, effective,, degree");
options.addOption("br", "bumper", true,
"Literal bumper, among any, assigned and falsified");
options.addOption("db", "double-bump-clashing", false,
"Whether clashing literal should be doubly bumped");
Option op = options.getOption("coeflim");
op.setArgName("limit");
op = options.getOption("coeflim-small");
......@@ -244,11 +248,14 @@ public class KTHLauncher {
if ("none".equals(value)) {
// default case, do nothing
} else if ("reduce".equals(value)) {
cpsolver.setPreprocess(PreProcessReduceConflict.instanceWithFalsified());
cpsolver.setPreprocess(
PreProcessReduceConflict.instanceWithFalsified());
} else if ("reduce-not-falsified".equals(value)) {
cpsolver.setPreprocess(PreProcessReduceConflict.instanceWithoutFalsified());
cpsolver.setPreprocess(PreProcessReduceConflict
.instanceWithoutFalsified());
} else {
log(value + " is not a supported value for option preprocess-conflict");
log(value
+ " is not a supported value for option preprocess-conflict");
return;
}
}
......@@ -279,21 +286,29 @@ public class KTHLauncher {
} else if ("divide-v1".equals(value)) {
cpsolver.setConflictFactory(ConflictMapRounding.factory());
} else if ("weaken".equals(value)) {
cpsolver.setConflictFactory(ConflictMapWeakenReason.factory());
cpsolver.setConflictFactory(
ConflictMapWeakenReason.factory());
} else if ("weaken-to-clash".equals(value)) {
cpsolver.setConflictFactory(ConflictMapWeakenToClash.factory());
cpsolver.setConflictFactory(
ConflictMapWeakenToClash.factory());
} else if ("weaken-and-divide".equals(value)) {
cpsolver.setConflictFactory(ConflictMapDivideByPivot.fullWeakeningOnReasonFactory());
cpsolver.setConflictFactory(ConflictMapDivideByPivot
.fullWeakeningOnReasonFactory());
} else if ("partial-weaken-and-divide".equals(value)) {
cpsolver.setConflictFactory(ConflictMapDivideByPivot.partialWeakeningOnReasonFactory());
cpsolver.setConflictFactory(ConflictMapDivideByPivot
.partialWeakeningOnReasonFactory());
} else if ("weaken-and-divide-both".equals(value)) {
cpsolver.setConflictFactory(ConflictMapDivideByPivot.fullWeakeningOnBothFactory());
cpsolver.setConflictFactory(ConflictMapDivideByPivot
.fullWeakeningOnBothFactory());
} else if ("partial-weaken-and-divide-both".equals(value)) {
cpsolver.setConflictFactory(ConflictMapDivideByPivot.partialWeakeningOnBothFactory());
cpsolver.setConflictFactory(ConflictMapDivideByPivot
.partialWeakeningOnBothFactory());
} else if ("weaken-and-divide-conflict".equals(value)) {
cpsolver.setConflictFactory(ConflictMapDivideByPivot.fullWeakeningOnConflictFactory());
cpsolver.setConflictFactory(ConflictMapDivideByPivot
.fullWeakeningOnConflictFactory());
} else if ("partial-weaken-and-divide-conflict".equals(value)) {
cpsolver.setConflictFactory(ConflictMapDivideByPivot.partialWeakeningOnConflictFactory());
cpsolver.setConflictFactory(ConflictMapDivideByPivot
.partialWeakeningOnConflictFactory());
} else {
// "divide-unless-equal":
// "divide-unless-divisor":
......@@ -352,110 +367,141 @@ public class KTHLauncher {
if (line.hasOption("autodiv")) {
cpsolver.setAutoDivisionStrategy(AutoDivisionStrategy.ENABLED);
}
if (line.hasOption("restart-strategy")) {
String value = line.getOptionValue("restart-strategy");
if ("picosat".equals(value)) {
// This is the default.
// This is the default.
} else if ("luby".equals(value)) {
cpsolver.setRestartStrategy(new LubyRestarts());
} else if ("lbd".equals(value)) {
cpsolver.setRestartStrategy(new Glucose21Restarts());
} else if ("size".equals(value)) {
cpsolver.setRestartStrategy(new GrowingCoefficientRestarts());
cpsolver.setRestartStrategy(
new GrowingCoefficientRestarts());
} else if ("none".equals(value)) {
cpsolver.setRestartStrategy(new NoRestarts());
} else {
log(value
+ " is not a supported value for option restart-strategy");
return;
}
}
if (line.hasOption("bump-strategy")) {
String value = line.getOptionValue("bump-strategy");
if ("one".equals(value)) {
cpsolver.setBumpStrategy(BumpStrategy.ALWAYS_ONE);
} else if ("degree".equals(value)) {
cpsolver.setBumpStrategy(BumpStrategy.DEGREE);
} else if ("coefficient".equals(value)) {
cpsolver.setBumpStrategy(BumpStrategy.COEFFICIENT);
} else if ("ratio-cd".equals(value)) {
cpsolver.setBumpStrategy(BumpStrategy.RATIO_CD);
} else if ("ratio-dc".equals(value)) {
cpsolver.setBumpStrategy(BumpStrategy.RATIO_DC);
} else {
log(value
+ " is not a supported value for option bump-strategy");
return;
}
}
if (line.hasOption("bumper")) {
String value = line.getOptionValue("bumper");
IBumper bumper = null;
if ("any".equals(value)) {
cpsolver.setBumper(Bumper.ANY);
bumper = Bumper.ANY;
} else if ("assigned".equals(value)) {
cpsolver.setBumper(Bumper.ASSIGNED);
bumper = Bumper.ASSIGNED;
} else if ("falsified".equals(value)) {
cpsolver.setBumper(Bumper.FALSIFIED);
bumper = Bumper.FALSIFIED;
} else if ("falsified-and-propagated".equals(value)) {
bumper = Bumper.FALSIFIED_AND_PROPAGATED;
} else if ("effective".equals(value)) {
cpsolver.setBumper(new BumperEffective());
bumper = new BumperEffective();
} else if ("effective-and-propagated".equals(value)) {
bumper = new BumperEffectiveAndPropagated();
} else {
log(value
+ " is not a supported value for option bump-strategy");
return;
}
if (line.hasOption("double-bump-clashing")) {