Commit 309f26f0 authored by Daniel Le Berre's avatar Daniel Le Berre

Merge branch 'master' of https://gitlab.ow2.org/sat4j/sat4j

parents 2afe466e bbcddd9a
Pipeline #372 failed with stages
in 11 minutes and 12 seconds
......@@ -395,6 +395,17 @@ public class ConflictMap extends MapPb implements IConflict {
// updating of the degree of the conflict
degreeCons = degreeCons.multiply(this.coefMultCons);
this.degree = this.degree.multiply(this.coefMult);
// Updating the stats about the reduction.
for (int i = 0; i < cpb.size(); i++) {
if (coefsCons[i].signum() != 0) {
if (this.voc.isUnassigned(cpb.get(i))) {
this.stats.numberOfRemainingUnassigned++;
} else {
this.stats.numberOfRemainingAssigned++;
}
}
}
}
// coefficients of the conflict must be multiplied by coefMult
......@@ -404,9 +415,7 @@ public class ConflictMap extends MapPb implements IConflict {
.multiply(this.coefMult));
}
}
}
assert slackConflict().signum() < 0;
// cutting plane
......
......@@ -64,6 +64,10 @@ public class PBSolverStats extends SolverStats {
public long numberOfDerivationSteps;
public long numberOfRemainingUnassigned;
public long numberOfRemainingAssigned;
@Override
public void reset() {
super.reset();
......@@ -78,6 +82,8 @@ public class PBSolverStats extends SolverStats {
this.numberOfEndingSkipping = 0;
this.numberOfInternalSkipping = 0;
this.numberOfDerivationSteps = 0;
this.numberOfRemainingUnassigned = 0;
this.numberOfRemainingAssigned = 0;
}
@Override
......@@ -116,6 +122,10 @@ public class PBSolverStats extends SolverStats {
out.println(prefix + "number of skipped derivation steps \t: "
+ (this.numberOfInternalSkipping
+ this.numberOfEndingSkipping));
out.println(prefix + "number of remaining unassigned \t: "
+ this.numberOfRemainingUnassigned);
out.println(prefix + "number of remaining assigned \t: "
+ this.numberOfRemainingAssigned);
}
}
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