Commit 3fc24511 authored by Romain WALLON's avatar Romain WALLON

More statistics for the different strategies

parent e19a5e18
......@@ -51,7 +51,7 @@ class GlucoseLCDS<D extends DataStructureFactory>
/**
*
*/
private final Solver<D> solver;
protected final Solver<D> solver;
private static final long serialVersionUID = 1L;
private int[] flags = new int[0];
private int flag = 0;
......@@ -75,6 +75,7 @@ class GlucoseLCDS<D extends DataStructureFactory>
} else {
c.remove(solver);
solver.slistener.delete(c);
onRemove(c);
}
}
if (solver.isVerbose()) {
......@@ -88,6 +89,10 @@ class GlucoseLCDS<D extends DataStructureFactory>
}
protected void onRemove(Constr c) {
// Nothing to do by default.
}
public ConflictTimer getTimer() {
return this.timer;
}
......
......@@ -386,12 +386,15 @@ public class ConflictMap extends MapPb implements IConflict {
}
// coefficients of the conflict must be multiplied by coefMult
long before = System.nanoTime();
if (!this.coefMult.equals(BigInteger.ONE)) {
for (int i = 0; i < size(); i++) {
changeCoef(i, this.weightedLits.getCoef(i)
.multiply(this.coefMult));
}
}
long after = System.nanoTime();
stats.incTimeForArithmeticOperations(after - before);
}
assert slackConflict().signum() < 0;
......@@ -674,8 +677,13 @@ public class ConflictMap extends MapPb implements IConflict {
* second integer
* @return the least common factor
*/
protected static BigInteger ppcm(BigInteger a, BigInteger b) {
return a.divide(a.gcd(b)).multiply(b);
protected BigInteger ppcm(BigInteger a, BigInteger b) {
long before = System.nanoTime();
BigInteger lcm = a.divide(a.gcd(b)).multiply(b);
long after = System.nanoTime();
stats.incTimeForArithmeticOperations(after - before);
return lcm;
}
/**
......
......@@ -30,6 +30,7 @@
package org.sat4j.pb.core;
import java.io.PrintWriter;
import java.math.BigInteger;
import org.sat4j.minisat.core.SolverStats;
......@@ -72,6 +73,14 @@ public class PBSolverStats extends SolverStats {
private long falsifiedLiteralsRemovedFromReason;
private long timeForArtithmeticOperations;
private BigInteger minRemoved;
private BigInteger maxRemoved;
private int nbRemoved;
@Override
public void reset() {
super.reset();
......@@ -136,6 +145,14 @@ public class PBSolverStats extends SolverStats {
out.println(prefix
+ "number of falsified literals weakened from conflict\t: "
+ this.falsifiedLiteralsRemovedFromConflict);
out.println(prefix + "time for arithmetic operations\t: "
+ this.timeForArtithmeticOperations);
out.println(prefix + "minimum degree of deleted constraints\t: "
+ this.minRemoved);
out.println(prefix + "maximum degree of deleted constraints\t: "
+ this.maxRemoved);
out.println(
prefix + "number of deleted constraints\t: " + this.nbRemoved);
}
public long getNumberOfReductions() {
......@@ -260,4 +277,28 @@ public class PBSolverStats extends SolverStats {
}
public void incTimeForArithmeticOperations(long time) {
this.timeForArtithmeticOperations += time;
}
public void setMinRemoved(BigInteger minRemoved) {
if (minRemoved == null) {
this.minRemoved = minRemoved;
} else {
this.minRemoved = this.minRemoved.min(minRemoved);
}
}
public void setMaxRemoved(BigInteger maxRemoved) {
if (maxRemoved == null) {
this.maxRemoved = maxRemoved;
} else {
this.maxRemoved = this.maxRemoved.max(maxRemoved);
}
}
public void incNbRemoved() {
this.nbRemoved++;
}
}
......@@ -9,6 +9,7 @@ import org.sat4j.minisat.core.Glucose2LCDS;
import org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy;
import org.sat4j.minisat.core.Solver;
import org.sat4j.pb.constraints.pb.PBConstr;
import org.sat4j.pb.core.PBSolverStats;
import org.sat4j.specs.Constr;
/**
......@@ -81,4 +82,12 @@ public class PBGlucoseLCDS<D extends DataStructureFactory>
+ lbdStrategy;
}
@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());
}
}
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