Commit 0e8589ac authored by Daniel Le Berre's avatar Daniel Le Berre
Browse files

Detect when no decision are taken after the first conflict.

parent ca754f5a
Pipeline #15603 passed with stages
in 48 minutes and 18 seconds
......@@ -1285,6 +1285,9 @@ public class Solver<D extends DataStructureFactory>
if (this.sharedConflict == null) {
// New variable decision
this.stats.incDecisions();
if (this.stats.getConflicts() > 0L) {
this.stats.setNoDecisionAfterFirstConflict(false);
}
int p = this.order.select();
if (p == ILits.UNDEFINED) {
// check (expensive) if all the constraints are not
......
......@@ -78,6 +78,8 @@ public class SolverStats implements Serializable {
private int importedUnits;
private boolean noDecisionAfterFirstConflict;
public void reset() {
this.starts = 0;
this.decisions = 0;
......@@ -96,6 +98,7 @@ public class SolverStats implements Serializable {
this.reduceddb = 0;
this.updateLBD = 0;
this.importedUnits = 0;
this.noDecisionAfterFirstConflict = true;
}
public void printStat(PrintWriter out, String prefix) {
......@@ -122,6 +125,8 @@ public class SolverStats implements Serializable {
out.println(prefix + "Number of update (reduction) of LBD\t: "
+ this.updateLBD);
out.println(prefix + "Imported unit clauses\t: " + this.importedUnits);
out.println(prefix + "No decision after first conflict\t: "
+ this.noDecisionAfterFirstConflict);
}
public Map<String, Number> toMap() {
......@@ -282,4 +287,13 @@ public class SolverStats implements Serializable {
public void incImportedUnits(int increment) {
this.importedUnits += increment;
}
public boolean hasNoDecisionAfterFirstConflict() {
return noDecisionAfterFirstConflict;
}
public void setNoDecisionAfterFirstConflict(
boolean noDecisionAfterFirstConflict) {
this.noDecisionAfterFirstConflict = noDecisionAfterFirstConflict;
}
}
Supports Markdown
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