Commit 6bac6d28 authored by Romain WALLON's avatar Romain WALLON
Browse files

Fixes the lost conflict due to irrelevant literal removal.

parent 3cbd2c53
Pipeline #9195 failed with stages
in 20 minutes and 30 seconds
......@@ -382,6 +382,8 @@ public class ConflictMap extends MapPb implements IConflict {
degreeCons, wpb);
if (degreeCons == null) {
// Aborting the resolution step.
// TODO Remove if irrelevant literal are removed before
// aborting.
int litLevel = ConflictMap
.levelToIndex(voc.getLevel(litImplied));
byLevel[litLevel].remove(nLitImplied);
......@@ -389,6 +391,7 @@ public class ConflictMap extends MapPb implements IConflict {
byLevel[0] = new VecInt();
}
byLevel[0].push(nLitImplied);
// TODO ---------
stats.abortedCancellations++;
return degree;
}
......@@ -515,6 +518,22 @@ public class ConflictMap extends MapPb implements IConflict {
ppcm = ppcm(reducedCoefs[ind], coefLitImplied);
this.coefMult = ppcm.divide(coefLitImplied);
this.coefMultCons = ppcm.divide(reducedCoefs[ind]);
slackThis = possConstraint(wpb, reducedCoefs).subtract(reducedDegree)
.multiply(this.coefMultCons);
assert slackThis.equals(wpb.slackConstraint(reducedCoefs, reducedDegree)
.multiply(this.coefMultCons)) : slackThis + " != "
+ wpb.slackConstraint(reducedCoefs, reducedDegree)
.multiply(this.coefMultCons);
assert slackConflict.equals(slackConflict());
slackIndex = slackConflict.multiply(this.coefMult);
assert slackIndex.signum() <= 0;
// estimate of the slack after the cutting plane
slackResolve = slackThis.add(slackIndex);
if (slackResolve.signum() >= 0) {
stats.numberOfReReducing++;
return reduceUntilConflict(litImplied, ind, reducedCoefs,
reducedDegree, wpb);
}
// TODO ----------------------------
assert this.coefMult.multiply(this.weightedLits.get(litImplied ^ 1))
......
......@@ -106,6 +106,8 @@ public class PBSolverStats extends SolverStats {
public long abortedCancellations;
public long numberOfReReducing;
private long falsifiedLiteralsRemovedFromConflict;
private long falsifiedLiteralsRemovedFromReason;
......@@ -145,6 +147,7 @@ public class PBSolverStats extends SolverStats {
this.numberOfConstraintsWhichAreClauses = 0;
this.numberOfConstraintsWhichAreCard = 0;
this.abortedCancellations = 0;
this.numberOfReReducing = 0;
this.numberOfTriggeredSaturations = 0;
this.timeSpentDetectingIrrelevant = 0;
......@@ -201,6 +204,8 @@ public class PBSolverStats extends SolverStats {
out.println(prefix
+ "number of irrelevant literals after cancellation \t: "
+ this.numberOfRemovedIrrelevantLiteralsAfterCancellation);
out.println(prefix + "number of re-reducing \t: "
+ this.numberOfReReducing);
out.println(
prefix + "max degree for Chow \t: " + this.maxDegreeForChow);
out.println(prefix + "max size for Chow \t: " + this.maxSizeForChow);
......
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