Commit b695c886 authored by Romain WALLON's avatar Romain WALLON

A first attempt to measure time needed to detect irrelevant literals

parent 0a3207ec
Pipeline #4741 failed with stages
in 4 minutes and 53 seconds
......@@ -47,87 +47,97 @@ public class RemoveIrrelevantPostProcess implements IPostProcess {
conflictMap.stats.numberOfConstraintsIgnoredByChow++;
return;
}
int alit = conflictMap.weightedLits
.getLit(conflictMap.assertiveLiteral);
conflictMap.stats.maxDegreeForChow = Math.max(
conflictMap.stats.maxDegreeForChow,
conflictMap.degree.longValue());
conflictMap.stats.maxSizeForChow = Math
.max(conflictMap.stats.maxSizeForChow, conflictMap.size());
NavigableMap<BigInteger, List<Integer>> coefs = new TreeMap<>();
BigInteger maxCoeff = BigInteger.ZERO;
for (int i = 0; i < conflictMap.size(); i++) {
BigInteger c = conflictMap.weightedLits.getCoef(i)
.min(conflictMap.degree);
coefs.computeIfAbsent(c, k -> new LinkedList<Integer>()).add(i);
maxCoeff = maxCoeff.max(c);
}
if (coefs.size() == 1) {
conflictMap.stats.numberOfNonPbConstraints++;
return;
}
long timeBefore = System.nanoTime();
try {
int alit = conflictMap.weightedLits
.getLit(conflictMap.assertiveLiteral);
conflictMap.stats.maxDegreeForChow = Math.max(
conflictMap.stats.maxDegreeForChow,
conflictMap.degree.longValue());
conflictMap.stats.maxSizeForChow = Math
.max(conflictMap.stats.maxSizeForChow, conflictMap.size());
NavigableMap<BigInteger, List<Integer>> coefs = new TreeMap<>();
BigInteger maxCoeff = BigInteger.ZERO;
for (int i = 0; i < conflictMap.size(); i++) {
BigInteger c = conflictMap.weightedLits.getCoef(i)
.min(conflictMap.degree);
coefs.computeIfAbsent(c, k -> new LinkedList<Integer>()).add(i);
maxCoeff = maxCoeff.max(c);
}
Set<BigInteger> irrelevant = new HashSet<>();
BigInteger smallestRelevant = BigInteger.ZERO;
for (Entry<BigInteger, List<Integer>> e : coefs.entrySet()) {
if (dependsOn(conflictMap, e.getKey(), e.getValue().get(0))) {
smallestRelevant = e.getKey();
break;
if (coefs.size() == 1) {
conflictMap.stats.numberOfNonPbConstraints++;
return;
}
irrelevant.add(e.getKey());
}
if (irrelevant.isEmpty()) {
conflictMap.stats.numberOfConstraintsNotChangedByChow++;
return;
}
Set<BigInteger> irrelevant = new HashSet<>();
BigInteger smallestRelevant = BigInteger.ZERO;
for (Entry<BigInteger, List<Integer>> e : coefs.entrySet()) {
if (dependsOn(conflictMap, e.getKey(), e.getValue().get(0))) {
smallestRelevant = e.getKey();
break;
}
irrelevant.add(e.getKey());
}
IVecInt toRemove = new VecInt();
BigInteger newDegree = BigInteger.ZERO;
for (BigInteger c : irrelevant) {
for (int i : coefs.get(c)) {
int lit = conflictMap.weightedLits.getLit(i);
toRemove.push(lit);
newDegree = newDegree.add(c);
if (irrelevant.isEmpty()) {
conflictMap.stats.numberOfConstraintsNotChangedByChow++;
return;
}
IVecInt toRemove = new VecInt();
BigInteger newDegree = BigInteger.ZERO;
for (BigInteger c : irrelevant) {
for (int i : coefs.get(c)) {
int lit = conflictMap.weightedLits.getLit(i);
toRemove.push(lit);
newDegree = newDegree.add(c);
}
}
}
for (int i = 0; i < toRemove.size(); i++)
conflictMap.removeCoef(toRemove.get(i));
for (int i = 0; i < toRemove.size(); i++)
conflictMap.removeCoef(toRemove.get(i));
conflictMap.degree = conflictMap.degree.subtract(newDegree);
conflictMap.degree = conflictMap.degree.subtract(newDegree);
if (smallestRelevant.compareTo(conflictMap.degree) >= 0) {
conflictMap.stats.numberOfConstraintsWhichAreClauses++;
if (smallestRelevant.compareTo(conflictMap.degree) >= 0) {
conflictMap.stats.numberOfConstraintsWhichAreClauses++;
} else if (smallestRelevant.equals(maxCoeff)) {
conflictMap.stats.numberOfConstraintsWhichAreCard++;
} else if (smallestRelevant.equals(maxCoeff)) {
conflictMap.stats.numberOfConstraintsWhichAreCard++;
}
}
conflictMap.saturation();
conflictMap.saturation();
if (maxCoeff.compareTo(conflictMap.degree) > 0) {
conflictMap.stats.numberOfTriggeredSaturations++;
}
if (maxCoeff.compareTo(conflictMap.degree) > 0) {
conflictMap.stats.numberOfTriggeredSaturations++;
}
conflictMap.assertiveLiteral = conflictMap.weightedLits
.getFromAllLits(alit);
conflictMap.stats.numberOfConstraintsChangedByChow++;
conflictMap.stats.numberOfRemovedIrrelevantLiterals += toRemove.size();
conflictMap.stats.maxDegreeModifiedByChow = Math.max(
conflictMap.stats.maxDegreeModifiedByChow,
conflictMap.degree.longValue());
conflictMap.stats.maxSizeModifiedByChow = Math.max(
conflictMap.stats.maxSizeModifiedByChow, conflictMap.size());
conflictMap.stats.maxDegreeDiff = Math
.max(conflictMap.stats.maxDegreeDiff, newDegree.longValue());
conflictMap.stats.maxRemovedChow = Math
.max(conflictMap.stats.maxRemovedChow, toRemove.size());
conflictMap.assertiveLiteral = conflictMap.weightedLits
.getFromAllLits(alit);
conflictMap.stats.numberOfConstraintsChangedByChow++;
conflictMap.stats.numberOfRemovedIrrelevantLiterals += toRemove
.size();
conflictMap.stats.maxDegreeModifiedByChow = Math.max(
conflictMap.stats.maxDegreeModifiedByChow,
conflictMap.degree.longValue());
conflictMap.stats.maxSizeModifiedByChow = Math.max(
conflictMap.stats.maxSizeModifiedByChow,
conflictMap.size());
conflictMap.stats.maxDegreeDiff = Math.max(
conflictMap.stats.maxDegreeDiff, newDegree.longValue());
conflictMap.stats.maxRemovedChow = Math
.max(conflictMap.stats.maxRemovedChow, toRemove.size());
} finally {
conflictMap.stats.timeSpentDetectingIrrelevant += System.nanoTime()
- timeBefore;
}
}
......
......@@ -96,6 +96,8 @@ public class PBSolverStats extends SolverStats {
public int numberOfTriggeredSaturations;
public long timeSpentDetectingIrrelevant;
@Override
public void reset() {
super.reset();
......@@ -128,6 +130,7 @@ public class PBSolverStats extends SolverStats {
this.numberOfConstraintsWhichAreCard = 0;
this.numberOfTriggeredSaturations = 0;
this.timeSpentDetectingIrrelevant = 0;
}
@Override
......@@ -198,6 +201,8 @@ public class PBSolverStats extends SolverStats {
+ this.numberOfConstraintsWhichAreCard);
out.println(prefix + "number of saturation after Chow \t: "
+ this.numberOfTriggeredSaturations);
out.println(prefix + "time spent detecting irrelevant literals \t: "
+ (this.timeSpentDetectingIrrelevant * 1E-9));
}
public long getNumberOfReductions() {
......
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