improved selection order index after conflict

logic-ng · Sep 14, 2019 · 1483906 · 1483906
1 parent 6d7d344
commit 1483906
Show file tree

Hide file tree

Showing 4 changed files with 44 additions and 5 deletions.
diff --git a/src/main/java/org/logicng/solvers/sat/GlucoseSyrup.java b/src/main/java/org/logicng/solvers/sat/GlucoseSyrup.java
@@ -828,7 +828,14 @@ private Tristate search() {
         this.lbdQueue.push(this.analyzeLBD);
         this.sumLBD += this.analyzeLBD;
         cancelUntil(this.analyzeBtLevel);
-        selectionOrderIdx = 0;
+        if(this.analyzeBtLevel < this.selectionOrder.size()) {
+          // this.selectionOrderIdx = this.analyzeBtLevel;
+          Integer orderIdx = this.decisionLvl2OrderIdx.get(this.analyzeBtLevel);
+          if(orderIdx != null) {
+            this.selectionOrderIdx = orderIdx;
+          }
+        }
+//        this.selectionOrderIdx = 0;
 
         if (this.config.proofGeneration) {
           final LNGIntVector vec = new LNGIntVector(learntClause.size());

diff --git a/src/main/java/org/logicng/solvers/sat/MiniCard.java b/src/main/java/org/logicng/solvers/sat/MiniCard.java
@@ -653,7 +653,14 @@ private Tristate search(final int nofConflicts) {
         final LNGIntVector learntClause = new LNGIntVector();
         analyze(confl, learntClause);
         cancelUntil(this.analyzeBtLevel);
-        selectionOrderIdx = 0;
+        if(this.analyzeBtLevel < this.selectionOrder.size()) {
+          // this.selectionOrderIdx = this.analyzeBtLevel;
+          Integer orderIdx = this.decisionLvl2OrderIdx.get(this.analyzeBtLevel);
+          if(orderIdx != null) {
+            this.selectionOrderIdx = orderIdx;
+          }
+        }
+//         this.selectionOrderIdx = 0;
         if (learntClause.size() == 1) {
           uncheckedEnqueue(learntClause.get(0), null);
           this.unitClauses.push(learntClause.get(0));

diff --git a/src/main/java/org/logicng/solvers/sat/MiniSat2Solver.java b/src/main/java/org/logicng/solvers/sat/MiniSat2Solver.java
@@ -573,7 +573,14 @@ private Tristate search(final int nofConflicts) {
         final LNGIntVector learntClause = new LNGIntVector();
         analyze(confl, learntClause);
         cancelUntil(this.analyzeBtLevel);
-        selectionOrderIdx = 0;
+        if(this.analyzeBtLevel < this.selectionOrder.size()) {
+          // this.selectionOrderIdx = this.analyzeBtLevel;
+          Integer orderIdx = this.decisionLvl2OrderIdx.get(this.analyzeBtLevel);
+          if(orderIdx != null) {
+            this.selectionOrderIdx = orderIdx;
+          }
+        }
+//         this.selectionOrderIdx = 0;
 
         if (this.config.proofGeneration) {
           final LNGIntVector vec = new LNGIntVector(learntClause.size());

diff --git a/src/main/java/org/logicng/solvers/sat/MiniSatStyleSolver.java b/src/main/java/org/logicng/solvers/sat/MiniSatStyleSolver.java
@@ -141,7 +141,10 @@ public abstract class MiniSatStyleSolver {
 
   // Selection order
   protected LNGIntVector selectionOrder;
+  //protected Map<Integer, Integer> orderLit2Idx;
+  protected Map<Integer, Integer> decisionLvl2OrderIdx;
   protected int selectionOrderIdx;
+  private int missCounter;
 
   /**
    * Constructs a new MiniSAT-style solver with a given configuration.
@@ -250,6 +253,8 @@ protected void initialize() {
     }
     this.computingBackbone = false;
     this.selectionOrder = new LNGIntVector();
+    // this.orderLit2Idx = new HashMap<>();
+    this.decisionLvl2OrderIdx = new HashMap<>();
     this.selectionOrderIdx = 0;
   }
 
@@ -487,7 +492,10 @@ protected int pickBranchLit() {
         final int var = var(lit);
         final MSVariable msVariable = this.vars.get(var);
         if (msVariable.assignment() == UNDEF) {
+          decisionLvl2OrderIdx.put(decisionLevel(), selectionOrderIdx);
           return lit;
+        } else {
+          missCounter++;
         }
       }
     }
@@ -1021,15 +1029,25 @@ public LNGVector<MSVariable> variables() {
 
   public void setSelectionOrder(final List<? extends Literal> selectionOrder) {
     this.selectionOrder.clear();
-    for (final Literal literal : selectionOrder) {
+    // this.orderLit2Idx.clear();
+    this.decisionLvl2OrderIdx.clear();
+    missCounter = 0;
+    for(int idx = 0; idx < selectionOrder.size(); ++idx) {
+      Literal literal = selectionOrder.get(idx);
       final Integer var = this.name2idx.get(literal.name());
       if (var != null) {
-        this.selectionOrder.push(mkLit(var, !literal.phase()));
+        int lit = mkLit(var, !literal.phase());
+        this.selectionOrder.push(lit);
+        // this.orderLit2Idx.put(lit, idx);
       }
     }
   }
 
   public void resetSelectionOrder() {
+    System.out.println(missCounter);
     this.selectionOrder.clear();
+    // this.orderLit2Idx.clear();
+    this.decisionLvl2OrderIdx.clear();
+    missCounter = 0;
   }
 }