Commit a05fdec0 authored by Daniel Le Berre's avatar Daniel Le Berre

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

parents a75cfaa7 eb123484
Pipeline #336 passed with stage
in 31 seconds
......@@ -554,6 +554,7 @@ public class Solver<D extends DataStructureFactory>
// literal is already satisfied. Skipping.
return true;
}
System.out.println("enqueue " + org.sat4j.core.LiteralsUtils.toDimacs(p));
if (this.voc.isFalsified(p)) {
// conflicting enqueued assignment
return false;
......@@ -1300,6 +1301,7 @@ public class Solver<D extends DataStructureFactory>
}
}
if (confl != null) {
System.out.println("conflict");
// conflict found
this.stats.conflicts++;
this.slistener.conflictFound(confl, decisionLevel(),
......
......@@ -114,6 +114,7 @@ public class VarOrderHeap implements IOrder, Serializable {
if (this.activity[var] < 0.0001) {
this.nullchoice++;
}
System.out.println("select(): " + org.sat4j.core.LiteralsUtils.toDimacs(next));
return next;
}
}
......
......@@ -294,6 +294,7 @@ public class ConflictMap extends MapPb implements IConflict {
*/
public BigInteger resolve(PBConstr cpb, int litImplied,
VarActivityListener val) {
System.out.println("resolve(cpb="+cpb+", litImplied="+litImplied+")");
assert litImplied > 1;
int nLitImplied = litImplied ^ 1;
if (cpb == null || !this.weightedLits.containsKey(nLitImplied)) {
......@@ -320,10 +321,12 @@ public class ConflictMap extends MapPb implements IConflict {
}
return this.degree;
}
System.out.println("resolve? " + org.sat4j.core.LiteralsUtils.toDimacs(litImplied));
if (this.allowSkipping) {
System.out.println("skip");
System.out.println("coef: " + this.weightedLits.get(nLitImplied) + ", slack: " + slackConflict());
if (this.weightedLits.get(nLitImplied).negate()
.compareTo(currentSlack.subtract(degree)) > 0) {
.compareTo(slackConflict() /*currentSlack.subtract(degree) */) > 0) {
if (this.endingSkipping)
stats.numberOfEndingSkipping++;
else
......@@ -341,10 +344,10 @@ public class ConflictMap extends MapPb implements IConflict {
return this.degree;
} else
this.endingSkipping = false;
}
stats.numberOfDerivationSteps++;
System.out.println("resolve " + org.sat4j.core.LiteralsUtils.toDimacs(litImplied));
assert slackConflict().signum() < 0;
assert this.degree.signum() >= 0;
......@@ -413,6 +416,7 @@ public class ConflictMap extends MapPb implements IConflict {
}
assert slackConflict().signum() < 0;
//assert slackConflict().equals(currentSlack.subtract(degree));
// cutting plane
this.degree = cuttingPlane(cpb, degreeCons, coefsCons,
......@@ -425,11 +429,13 @@ public class ConflictMap extends MapPb implements IConflict {
assert getLevelByLevel(nLitImplied) == -1;
assert this.degree.signum() > 0;
assert slackConflict().signum() < 0;
//assert slackConflict().equals(currentSlack.subtract(degree));
// saturation
this.degree = saturation();
assert slackConflict().signum() < 0;
divideCoefs();
System.out.println("after resolve step: " + this);
return this.degree;
}
......
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