Commit f4f0ab96 authored by Romain WALLON's avatar Romain WALLON
Browse files

Some changes to take both removal and weakening into account.

parent 68f45ed9
Pipeline #7736 failed with stages
in 61 minutes and 15 seconds
......@@ -30,6 +30,7 @@
package org.sat4j;
import java.io.BufferedReader;
import java.io.FileNotFoundException;
import java.io.IOException;
import java.io.InputStreamReader;
import java.io.ObjectInputStream;
......
......@@ -7,7 +7,7 @@ public final class IrrelevantLiteralDetectionStrategyFactory {
}
public static IrrelevantLiteralDetectionStrategy defaultStrategy() {
return new KnapsackApproximationIrrelevantLiteralDetectionStrategy();
return new SubsetSumApproximationIrrelevantLiteralDetectionStrategy();
}
}
......@@ -72,7 +72,8 @@ public class RemoveIrrelevantPostProcess implements IPostProcess {
conflictMap.stats.numberOfNonPbConstraints++;
return;
}
BigInteger slack = conflictMap.computeSlack(lvl);
BigInteger slack = conflictMap.computeSlack(lvl + 1)
.subtract(conflictMap.degree);
Set<BigInteger> irrelevant = new HashSet<>();
BigInteger smallestRelevant = BigInteger.ZERO;
for (Entry<BigInteger, List<Integer>> e : coefs.entrySet()) {
......@@ -111,7 +112,22 @@ public class RemoveIrrelevantPostProcess implements IPostProcess {
for (int i = 0; i < toRemove.size(); i++)
conflictMap.removeCoef(toRemove.get(i));
conflictMap.degree = conflictMap.degree.subtract(newDegree);
BigInteger reducedDegree = conflictMap.degree.subtract(newDegree);
BigInteger sumAllCoef = BigInteger.ZERO;
BigInteger sumAllCoefSaturated = BigInteger.ZERO;
for (int i = 0; i < conflictMap.size(); i++) {
sumAllCoef = sumAllCoef.add(conflictMap.weightedLits.getCoef(i)
.min(conflictMap.degree));
sumAllCoefSaturated = sumAllCoefSaturated.add(
conflictMap.weightedLits.getCoef(i).min(reducedDegree));
}
if (sumAllCoef.subtract(conflictMap.degree).compareTo(
sumAllCoefSaturated.subtract(reducedDegree)) > 0) {
conflictMap.degree = reducedDegree;
conflictMap.stats.numberOfTriggeredSaturations++;
System.out.println("saturation");
}
if (smallestRelevant.compareTo(conflictMap.degree) >= 0) {
conflictMap.stats.numberOfConstraintsWhichAreClauses++;
......@@ -121,11 +137,6 @@ public class RemoveIrrelevantPostProcess implements IPostProcess {
}
conflictMap.saturation();
if (maxCoeff.compareTo(conflictMap.degree) > 0) {
conflictMap.stats.numberOfTriggeredSaturations++;
}
if (alit >= 0) {
conflictMap.assertiveLiteral = conflictMap.weightedLits
.getFromAllLits(alit);
......
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