Commit 3c078bdd authored by Romain Wallon's avatar Romain Wallon

Adds the LBD-effective measure

parent 297871ae
Pipeline #9130 passed with stages
in 103 minutes and 28 seconds
......@@ -95,7 +95,7 @@ public class ActivityLCDS implements LearnedConstraintsDeletionStrategy {
}
}
public void onPropagation(Constr from) {
public void onPropagation(Constr from, int propagated) {
// do nothing
}
......
......@@ -68,7 +68,8 @@ final class AgeLCDS implements LearnedConstraintsDeletionStrategy {
}
if (solver.isVerbose()) {
solver.out.log(solver.getLogPrefix() + "cleaning " //$NON-NLS-1$
+ (solver.learnts.size() - j) + " clauses out of " + solver.learnts.size()); //$NON-NLS-1$
+ (solver.learnts.size() - j) + " clauses out of " //$NON-NLS-1$
+ solver.learnts.size());
// out.flush();
}
solver.learnts.shrinkTo(j);
......@@ -97,7 +98,7 @@ final class AgeLCDS implements LearnedConstraintsDeletionStrategy {
// do nothing
}
public void onPropagation(Constr from) {
public void onPropagation(Constr from, int propagated) {
// do nothing
}
}
\ No newline at end of file
......@@ -49,9 +49,9 @@ public class Glucose2LCDS<D extends DataStructureFactory>
}
@Override
public void onPropagation(Constr from) {
public void onPropagation(Constr from, int propagated) {
if (from.getActivity() > 2.0) {
int nblevel = computeLBD(from);
int nblevel = computeLBD(from, propagated);
if (nblevel < from.getActivity()) {
getSolver().stats.incUpdateLBD();
from.setActivity(nblevel);
......
......@@ -114,11 +114,11 @@ class GlucoseLCDS<D extends DataStructureFactory>
}
public void onClauseLearning(Constr constr) {
int nblevel = computeLBD(constr);
int nblevel = computeLBD(constr, -1);
constr.setActivity(nblevel);
}
protected int computeLBD(Constr constr) {
protected int computeLBD(Constr constr, int propagated) {
int nblevel = 1;
this.flag++;
int currentLevel;
......@@ -136,7 +136,7 @@ class GlucoseLCDS<D extends DataStructureFactory>
}
public void onPropagation(Constr from) {
public void onPropagation(Constr from, int propagated) {
}
......
......@@ -79,5 +79,5 @@ public interface LearnedConstraintsDeletionStrategy extends Serializable {
*
* @param from
*/
void onPropagation(Constr from);
void onPropagation(Constr from, int propagated);
}
\ No newline at end of file
......@@ -96,7 +96,7 @@ final class SizeLCDS implements LearnedConstraintsDeletionStrategy {
}
}
public void onPropagation(Constr from) {
public void onPropagation(Constr from, int propagated) {
// do nothing
}
}
\ No newline at end of file
......@@ -575,7 +575,7 @@ public class Solver<D extends DataStructureFactory>
this.voc.setReason(p, from);
this.trail.push(p);
if (from != null && from.learnt()) {
this.learnedConstraintsDeletionStrategy.onPropagation(from);
this.learnedConstraintsDeletionStrategy.onPropagation(from, p);
}
return true;
}
......@@ -1698,7 +1698,7 @@ public class Solver<D extends DataStructureFactory>
return this.aTimer;
}
public void onPropagation(Constr from) {
public void onPropagation(Constr from, int propagated) {
// TODO Auto-generated method stub
}
......
......@@ -321,7 +321,7 @@ public abstract class PBSolver extends Solver<PBDataStructureFactory>
// do nothing
}
public void onPropagation(Constr from) {
public void onPropagation(Constr from, int propagated) {
// do nothing
}
};
......
......@@ -3,7 +3,8 @@ package org.sat4j.pb.lcds;
import org.sat4j.minisat.core.ILits;
import org.sat4j.pb.constraints.pb.PBConstr;
public abstract class AbstractLBDComputerStrategy implements ILBDComputerStrategy {
public abstract class AbstractLBDComputerStrategy
implements ILBDComputerStrategy {
protected int[] flags = new int[0];
......@@ -18,10 +19,10 @@ public abstract class AbstractLBDComputerStrategy implements ILBDComputerStrateg
}
@Override
public int computeLBD(ILits voc, PBConstr constr) {
public int computeLBD(ILits voc, PBConstr constr, int propagated) {
int nblevel = 1;
this.flag++;
startComputeLBD();
startComputeLBD(constr, propagated);
for (int i = 0; i < constr.size(); i++) {
int currentLevel = voc.getLevel(constr.get(i));
if (currentLevel < 0) {
......@@ -36,7 +37,7 @@ public abstract class AbstractLBDComputerStrategy implements ILBDComputerStrateg
return nblevel;
}
protected void startComputeLBD() {
protected void startComputeLBD(PBConstr constr, int propagated) {
}
......@@ -44,4 +45,8 @@ public abstract class AbstractLBDComputerStrategy implements ILBDComputerStrateg
protected abstract int assignedLiteral(ILits voc, PBConstr constr, int i);
protected int fixLbd(PBConstr constr, int lbd) {
return lbd;
}
}
......@@ -21,7 +21,7 @@ public class DegreeLBDComputerStrategy implements ILBDComputerStrategy {
}
@Override
public int computeLBD(ILits voc, PBConstr constr) {
public int computeLBD(ILits voc, PBConstr constr, int propagated) {
BigInteger degree = constr.getDegree();
if (degree.bitLength() < Integer.SIZE) {
return degree.intValue();
......
......@@ -3,8 +3,13 @@
*/
package org.sat4j.pb.lcds;
import java.math.BigInteger;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.core.ILits;
import org.sat4j.pb.constraints.pb.PBConstr;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.IteratorInt;
/**
* @author wallon
......@@ -13,16 +18,51 @@ import org.sat4j.pb.constraints.pb.PBConstr;
public class EffectiveLiteralsOnlyLBDComputerStrategy
extends AbstractLBDComputerStrategy {
private int currentPropagated;
private BigInteger degree;
private final IVecInt lbdCandidates = new VecInt();
@Override
protected void startComputeLBD(PBConstr constr, int propagated) {
this.degree = constr.getDegree();
this.currentPropagated = propagated;
lbdCandidates.clear();
}
@Override
protected int unassignedLiteral(ILits voc, PBConstr constr, int i) {
degree = degree.subtract(constr.getCoef(i));
return 0;
}
@Override
protected int assignedLiteral(ILits voc, PBConstr constr, int i) {
if (constr.get(i) == currentPropagated) {
return 0;
}
if (voc.isSatisfied(constr.get(i))) {
degree = degree.subtract(constr.getCoef(i));
return 0;
}
lbdCandidates.push(i);
return 1;
}
@Override
protected int fixLbd(PBConstr constr, int lbd) {
int newLbd = 0;
for (IteratorInt it = lbdCandidates.iterator(); it.hasNext();) {
int v = it.next();
if (constr.getCoef(v).compareTo(degree) >= 0) {
newLbd++;
} else {
break;
}
}
return newLbd;
}
}
/**
*
*/
package org.sat4j.pb.lcds;
import org.sat4j.minisat.core.ILits;
import org.sat4j.pb.constraints.pb.PBConstr;
/**
* @author wallon
*
*/
public class FalsifiedLiteralsOnlyLBDComputerStrategy
extends AbstractLBDComputerStrategy {
@Override
protected int unassignedLiteral(ILits voc, PBConstr constr, int i) {
return 0;
}
@Override
protected int assignedLiteral(ILits voc, PBConstr constr, int i) {
if (voc.isSatisfied(constr.get(i))) {
return 0;
}
return 1;
}
}
......@@ -7,6 +7,6 @@ public interface ILBDComputerStrategy {
void init(int howmany);
int computeLBD(ILits voc, PBConstr constr);
int computeLBD(ILits voc, PBConstr constr, int propagated);
}
\ No newline at end of file
......@@ -24,8 +24,8 @@ public class LBDComputerStrategyDecorator implements ILBDComputerStrategy {
}
@Override
public int computeLBD(ILits voc, PBConstr constr) {
return decorated.computeLBD(voc, constr);
public int computeLBD(ILits voc, PBConstr constr, int propagated) {
return decorated.computeLBD(voc, constr, propagated);
}
}
......@@ -48,8 +48,8 @@ public class NullLCDS implements LearnedConstraintsDeletionStrategy {
}
@Override
public void onPropagation(Constr from) {
decorated.onPropagation(from);
public void onPropagation(Constr from, int propagated) {
decorated.onPropagation(from, propagated);
}
}
......@@ -37,6 +37,12 @@ public class PBGlucoseLCDS<D extends DataStructureFactory>
new IgnoreUnassignedLiteralsLBDComputerStrategy());
}
public static <D extends DataStructureFactory> LearnedConstraintsDeletionStrategy newFalsifiedOnly(
Solver<D> solver, ConflictTimer timer) {
return new PBGlucoseLCDS<D>(solver, timer,
new FalsifiedLiteralsOnlyLBDComputerStrategy());
}
public static <D extends DataStructureFactory> LearnedConstraintsDeletionStrategy newEffectiveOnly(
Solver<D> solver, ConflictTimer timer) {
return new PBGlucoseLCDS<D>(solver, timer,
......@@ -68,12 +74,13 @@ public class PBGlucoseLCDS<D extends DataStructureFactory>
}
@Override
protected int computeLBD(Constr constr) {
protected int computeLBD(Constr constr, int propagated) {
if (constr instanceof PBConstr) {
return lbdStrategy.computeLBD(getSolver().getVocabulary(),
(PBConstr) constr);
PBConstr pbconstr = (PBConstr) constr;
return lbdStrategy.computeLBD(getSolver().getVocabulary(), pbconstr,
propagated);
}
return super.computeLBD(constr);
return super.computeLBD(constr, propagated);
}
@Override
......
......@@ -16,7 +16,7 @@ public class UnassignedLiteralsHaveSameLevelLBDComputerStrategy
private boolean unassignedFound;
@Override
protected void startComputeLBD() {
protected void startComputeLBD(PBConstr constr, int propagated) {
this.unassignedFound = false;
}
......
......@@ -19,8 +19,9 @@ public class WeightedLBDComputerStrategy extends LBDComputerStrategyDecorator {
}
@Override
public int computeLBD(ILits voc, PBConstr constr) {
BigInteger lbd = BigInteger.valueOf(super.computeLBD(voc, constr));
public int computeLBD(ILits voc, PBConstr constr, int propagated) {
BigInteger lbd = BigInteger
.valueOf(super.computeLBD(voc, constr, propagated));
BigInteger weighted = lbd.multiply(constr.getDegree().multiply(lbd));
if (weighted.bitLength() < Integer.SIZE) {
return weighted.intValue();
......
......@@ -39,7 +39,7 @@ public class BumperEffective implements IBumper {
} else if (!voc.isFalsified(constr.get(lit))) {
// Weakening on this literal preserves the propagation.
constrDegree = constrDegree.subtract(constr.getCoefs()[lit]);
constrDegree = constrDegree.subtract(constr.getCoef(lit));
} else {
// The literal may be effective.
......@@ -51,8 +51,10 @@ public class BumperEffective implements IBumper {
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) {
if (constr.getCoef(v).compareTo(constrDegree) >= 0) {
bumpStrategy.varBumpActivity(order, constr, v);
} else {
break;
}
}
}
......
......@@ -42,6 +42,7 @@ 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;
......@@ -429,27 +430,31 @@ public class KTHLauncher {
ConflictTimer timer = cpsolver.lbd_based.getTimer();
if ("activity".equals(value)) {
LearnedConstraintsDeletionStrategy lcds = new PBActivityLCDS(cpsolver, timer);
cpsolver.setLearnedConstraintsDeletionStrategy(lcds);
cpsolver.setLearnedConstraintsDeletionStrategy(new NullLCDS(lcds));
} else if ("assigned".equals(value)) {
LearnedConstraintsDeletionStrategy lcds = PBGlucoseLCDS.newIgnoreUnassigned(cpsolver, timer);
cpsolver.setLearnedConstraintsDeletionStrategy(lcds);
cpsolver.setLearnedConstraintsDeletionStrategy(new NullLCDS(lcds));
} else if ("unassigned-same".equals(value)) {
LearnedConstraintsDeletionStrategy lcds = PBGlucoseLCDS.newUnassignedSame(cpsolver, timer);
cpsolver.setLearnedConstraintsDeletionStrategy(lcds);
cpsolver.setLearnedConstraintsDeletionStrategy(new NullLCDS(lcds));
} else if ("unassigned-different".equals(value)) {
LearnedConstraintsDeletionStrategy lcds = PBGlucoseLCDS.newUnassignedDifferent(cpsolver, timer);
cpsolver.setLearnedConstraintsDeletionStrategy(lcds);
cpsolver.setLearnedConstraintsDeletionStrategy(new NullLCDS(lcds));
} else if ("falsified".equals(value)) {
LearnedConstraintsDeletionStrategy lcds = PBGlucoseLCDS.newFalsifiedOnly(cpsolver, timer);
cpsolver.setLearnedConstraintsDeletionStrategy(new NullLCDS(lcds));
} else if ("effective".equals(value)) {
LearnedConstraintsDeletionStrategy lcds = PBGlucoseLCDS.newEffectiveOnly(cpsolver, timer);
cpsolver.setLearnedConstraintsDeletionStrategy(lcds);
cpsolver.setLearnedConstraintsDeletionStrategy(new NullLCDS(lcds));
} else if ("degree".equals(value)) {
LearnedConstraintsDeletionStrategy lcds = PBGlucoseLCDS.newDegree(cpsolver, timer);
cpsolver.setLearnedConstraintsDeletionStrategy(lcds);
cpsolver.setLearnedConstraintsDeletionStrategy(new NullLCDS(lcds));
} else {
log(value
......
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