Commit 6d880cc4 authored by Romain Wallon's avatar Romain Wallon

Adds more statistics to the different LCDSs.

parent 408542ef
......@@ -34,12 +34,12 @@ import org.sat4j.specs.Constr;
import org.sat4j.specs.IVec;
@Feature(value = "deletion", parent = "expert")
final class ActivityLCDS implements LearnedConstraintsDeletionStrategy {
public class ActivityLCDS implements LearnedConstraintsDeletionStrategy {
private static final long serialVersionUID = 1L;
private final ConflictTimer timer;
private final Solver<? extends DataStructureFactory> solver;
protected final Solver<? extends DataStructureFactory> solver;
ActivityLCDS(Solver<? extends DataStructureFactory> solver,
public ActivityLCDS(Solver<? extends DataStructureFactory> solver,
ConflictTimer timer) {
this.timer = timer;
this.solver = solver;
......@@ -53,6 +53,7 @@ final class ActivityLCDS implements LearnedConstraintsDeletionStrategy {
if (c.locked() || c.size() == 2) {
learnedConstrs.set(j++, learnedConstrs.get(i));
} else {
onRemove(c);
c.remove(solver);
solver.slistener.delete(c);
}
......@@ -97,4 +98,8 @@ final class ActivityLCDS implements LearnedConstraintsDeletionStrategy {
public void onPropagation(Constr from) {
// do nothing
}
protected void onRemove(Constr c) {
// Nothing to do by default.
}
}
\ No newline at end of file
......@@ -282,7 +282,7 @@ public class PBSolverStats extends SolverStats {
}
public void setMinRemoved(BigInteger minRemoved) {
if (minRemoved == null) {
if (this.minRemoved == null) {
this.minRemoved = minRemoved;
} else {
this.minRemoved = this.minRemoved.min(minRemoved);
......@@ -290,7 +290,7 @@ public class PBSolverStats extends SolverStats {
}
public void setMaxRemoved(BigInteger maxRemoved) {
if (maxRemoved == null) {
if (this.maxRemoved == null) {
this.maxRemoved = maxRemoved;
} else {
this.maxRemoved = this.maxRemoved.max(maxRemoved);
......
/**
*
*/
package org.sat4j.pb.lcds;
import org.sat4j.minisat.core.ActivityLCDS;
import org.sat4j.minisat.core.ConflictTimer;
import org.sat4j.minisat.core.DataStructureFactory;
import org.sat4j.minisat.core.Solver;
import org.sat4j.pb.constraints.pb.PBConstr;
import org.sat4j.pb.core.PBSolverStats;
import org.sat4j.specs.Constr;
/**
* @author romain
*
*/
public class PBActivityLCDS extends ActivityLCDS {
/**
*
*/
private static final long serialVersionUID = 1L;
public PBActivityLCDS(Solver<? extends DataStructureFactory> solver,
ConflictTimer timer) {
super(solver, timer);
}
@Override
protected void onRemove(Constr c) {
PBConstr constr = (PBConstr) c;
PBSolverStats stats = (PBSolverStats) solver.getStats();
stats.incNbRemoved();
stats.setMinRemoved(constr.getDegree());
stats.setMaxRemoved(constr.getDegree());
}
}
......@@ -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.PBActivityLCDS;
import org.sat4j.pb.lcds.PBGlucoseLCDS;
import org.sat4j.pb.orders.BumpStrategy;
import org.sat4j.pb.orders.Bumper;
......@@ -424,6 +425,8 @@ public class KTHLauncher {
String value = line.getOptionValue("deletion-strategy");
ConflictTimer timer = cpsolver.lbd_based.getTimer();
if ("activity".equals(value)) {
LearnedConstraintsDeletionStrategy lcds = new PBActivityLCDS(cpsolver, timer);
cpsolver.setLearnedConstraintsDeletionStrategy(lcds);
} else if ("assigned".equals(value)) {
LearnedConstraintsDeletionStrategy lcds = PBGlucoseLCDS.newIgnoreUnassigned(cpsolver, timer);
......@@ -445,12 +448,6 @@ public class KTHLauncher {
LearnedConstraintsDeletionStrategy lcds = PBGlucoseLCDS.newDegree(cpsolver, timer);
cpsolver.setLearnedConstraintsDeletionStrategy(lcds);
} else if ("size".equals(value)) {
cpsolver.setLearnedConstraintsDeletionStrategy(cpsolver.size_based);
} else if ("age".equals(value)) {
cpsolver.setLearnedConstraintsDeletionStrategy(cpsolver.age_based);
} 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