Commit 408542ef authored by Romain WALLON's avatar Romain WALLON

Adds the bumper for effective literals only.

parent 3fc24511
Pipeline #9077 passed with stages
in 104 minutes and 37 seconds
......@@ -1074,7 +1074,7 @@ public class Solver<D extends DataStructureFactory>
this.order.updateVar(p);
}
public void varBumpActivity(Constr constr, int i) {
public void varBumpActivity(Constr constr, int i, int p) {
this.order.updateVar(constr.get(i));
}
......@@ -2599,4 +2599,9 @@ public class Solver<D extends DataStructureFactory>
public void setUnitClauseConsumer(UnitClauseConsumer ucc) {
this.unitClauseConsumer = ucc;
}
@Override
public void postBumpActivity(Constr constr) {
// Nothing to do by default.
}
}
......@@ -53,6 +53,8 @@ public interface VarActivityListener extends Serializable {
/**
* Update the activity of a variable v.
*/
void varBumpActivity(Constr constr, int i);
void varBumpActivity(Constr constr, int i, int p);
void postBumpActivity(Constr constr);
}
......@@ -400,7 +400,7 @@ public class ConflictMap extends MapPb implements IConflict {
// cutting plane
this.degree = cuttingPlane(cpb, degreeCons, coefsCons,
this.coefMultCons, val);
this.coefMultCons, val, ind);
// neither litImplied nor nLitImplied is present in coefs structure
assert !this.weightedLits.containsKey(litImplied);
assert !this.weightedLits.containsKey(nLitImplied);
......
......@@ -95,13 +95,13 @@ public interface IDataStructurePB {
@Override
public BigInteger cuttingPlane(PBConstr cpb, BigInteger degreeCons,
BigInteger[] reducedCoefs, BigInteger coefMult,
VarActivityListener val) {
VarActivityListener val, int p) {
throw new UnsupportedOperationException();
}
@Override
public BigInteger cuttingPlane(PBConstr cpb, BigInteger deg,
BigInteger[] reducedCoefs, VarActivityListener val) {
BigInteger[] reducedCoefs, VarActivityListener val, int p) {
throw new UnsupportedOperationException();
}
......@@ -119,11 +119,11 @@ public interface IDataStructurePB {
BigInteger saturation();
BigInteger cuttingPlane(PBConstr cpb, BigInteger deg,
BigInteger[] reducedCoefs, VarActivityListener val);
BigInteger[] reducedCoefs, VarActivityListener val, int p);
BigInteger cuttingPlane(PBConstr cpb, BigInteger degreeCons,
BigInteger[] reducedCoefs, BigInteger coefMult,
VarActivityListener val);
VarActivityListener val, int p);
BigInteger cuttingPlane(int[] lits, BigInteger[] reducedCoefs,
BigInteger deg);
......
......@@ -197,29 +197,29 @@ public class MapPb implements IDataStructurePB {
}
public BigInteger cuttingPlane(PBConstr cpb, BigInteger deg,
BigInteger[] reducedCoefs, VarActivityListener val) {
return cuttingPlane(cpb, deg, reducedCoefs, BigInteger.ONE, val);
BigInteger[] reducedCoefs, VarActivityListener val, int p) {
return cuttingPlane(cpb, deg, reducedCoefs, BigInteger.ONE, val, p);
}
public BigInteger cuttingPlane(PBConstr cpb, BigInteger degreeCons,
BigInteger[] reducedCoefs, BigInteger coefMult,
VarActivityListener val) {
VarActivityListener val, int p) {
this.degree = this.degree.add(degreeCons);
assert this.degree.signum() > 0;
if (reducedCoefs == null) {
for (int i = 0; i < cpb.size(); i++) {
val.varBumpActivity(cpb, i);
val.varBumpActivity(cpb, i, p);
cuttingPlaneStep(cpb.get(i),
multiplyCoefficient(cpb.getCoef(i), coefMult));
}
} else {
for (int i = 0; i < cpb.size(); i++) {
val.varBumpActivity(cpb, i);
val.varBumpActivity(cpb, i, p);
cuttingPlaneStep(cpb.get(i),
multiplyCoefficient(reducedCoefs[i], coefMult));
}
}
val.postBumpActivity(cpb);
return this.degree;
}
......
......@@ -51,6 +51,7 @@ import org.sat4j.pb.constraints.pb.PBConstr;
import org.sat4j.pb.constraints.pb.SkipStrategy;
import org.sat4j.pb.orders.BumpStrategy;
import org.sat4j.pb.orders.Bumper;
import org.sat4j.pb.orders.IBumper;
import org.sat4j.specs.Constr;
import org.sat4j.specs.IVec;
import org.sat4j.specs.TimeoutException;
......@@ -86,7 +87,7 @@ public class PBSolverCP extends PBSolver {
private BumpStrategy bumpStrategy = BumpStrategy.ALWAYS_ONE;
private Bumper bumper = Bumper.ANY;
private IBumper bumper = Bumper.ANY;
/**
* @param acg
......@@ -262,8 +263,8 @@ public class PBSolverCP extends PBSolver {
this.bumpStrategy = bumpStrategy;
}
public void setBumper(Bumper bumper) {
this.bumper = bumper;
public void setBumper(IBumper bumperEffective) {
this.bumper = bumperEffective;
}
public SkipStrategy isSkipAllow() {
......@@ -316,9 +317,14 @@ public class PBSolverCP extends PBSolver {
}
@Override
public void varBumpActivity(Constr constr, int i) {
public void varBumpActivity(Constr constr, int i, int p) {
bumper.varBumpActivity(voc, bumpStrategy, getOrder(), (PBConstr) constr,
i);
i, p);
}
@Override
public void postBumpActivity(Constr constr) {
bumper.postBumpActivity(getOrder(), (PBConstr) constr);
}
}
......@@ -4,7 +4,7 @@ import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.IOrder;
import org.sat4j.pb.constraints.pb.PBConstr;
public enum Bumper {
public enum Bumper implements IBumper {
ANY {
@Override
......@@ -28,12 +28,17 @@ public enum Bumper {
};
public void varBumpActivity(ILits voc, BumpStrategy bumpStrategy,
IOrder order, PBConstr constr, int i) {
IOrder order, PBConstr constr, int i, int propagated) {
if (isBumpable(voc, constr.get(i))) {
bumpStrategy.varBumpActivity(order, constr, i);
}
}
@Override
public void postBumpActivity(IOrder order, PBConstr constr) {
// Everything has already been done.
}
abstract boolean isBumpable(ILits voc, int i);
}
/**
*
*/
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 BumperEffective implements IBumper {
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;
}
if (lit == propagated) {
// The implied literal is always bumped.
bStrategy.varBumpActivity(order, constr, lit);
} else if (!voc.isFalsified(constr.get(lit))) {
// Weakening on this literal preserves the propagation.
constrDegree = constrDegree.subtract(constr.getCoefs()[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.getCoefs()[v].compareTo(constrDegree) >= 0) {
bumpStrategy.varBumpActivity(order, constr, v);
}
}
}
@Override
public String toString() {
return "EFFECTIVE";
}
}
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 interface IBumper {
void varBumpActivity(ILits voc, BumpStrategy bumpStrategy, IOrder order,
PBConstr constr, int i, int propagated);
void postBumpActivity(IOrder order, PBConstr constr);
}
......@@ -14,7 +14,6 @@ import org.apache.commons.cli.ParseException;
import org.apache.commons.cli.PosixParser;
import org.sat4j.minisat.core.ConflictTimer;
import org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy;
import org.sat4j.minisat.core.LearnedConstraintsEvaluationType;
import org.sat4j.minisat.learning.MiniSATLearning;
import org.sat4j.minisat.orders.NaturalStaticOrder;
import org.sat4j.minisat.orders.VarOrderHeap;
......@@ -46,6 +45,7 @@ import org.sat4j.pb.core.PBSolverCP;
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.reader.OPBReader2012;
import org.sat4j.pb.restarts.GrowingCoefficientRestarts;
import org.sat4j.pb.tools.InprocCardConstrLearningSolver;
......@@ -410,6 +410,9 @@ public class KTHLauncher {
} else if ("falsified".equals(value)) {
cpsolver.setBumper(Bumper.FALSIFIED);
} else if ("effective".equals(value)) {
cpsolver.setBumper(new BumperEffective());
} else {
log(value
+ " is not a supported value for option bump-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