Fix 1233

solver/src/main/java/org/chocosolver/sat/ArrayClause.java

@@ -41,6 +41,11 @@ public final class ArrayClause extends Clause {
      */
     private final int id;
 
+    /**
+     * Position of the last scanned literal
+     */
+    private int lastScannedLit = 1;
+
     /**
      * Create a clause with a set of literals
      *
@@ -166,4 +171,19 @@ public int _g(int i) {
     public void _s(int pos, int l) {
         literals_[pos] = l;
     }
+
+    /**
+     * @return the position of the last scanned literal
+     */
+    public int getLastScannedLit() {
+        return lastScannedLit;
+    }
+
+    /**
+     * Set the position of the last scanned literal to <i>lastScannedLit</i>.
+     * @param lastScannedLit position to store
+     */
+    public void setLastScannedLit(int lastScannedLit) {
+        this.lastScannedLit = lastScannedLit;
+    }
 }

solver/src/main/java/org/chocosolver/sat/MiniSat.java

@@ -99,7 +99,7 @@ public void resize(int j) {
     static final VarData VD_Undef = new VarData(R_Undef, -1, -1);
     public Clause confl = C_Undef;
 
-    public static final Clause C_Fail = new ArrayClause(new int[]{0, 0});
+    public static final ArrayClause C_Fail = new ArrayClause(new int[]{0, 0});
     static final ChannelInfo CI_Null = new ChannelInfo(null, 0, 0, 0);
 
     // If false, the constraints are already unsatisfiable. No part of
@@ -254,7 +254,7 @@ public boolean addClause(TIntList ps) {
                 propagate();
                 return (ok_ = (confl == C_Undef));
             default:
-                Clause cr = new ArrayClause(ps);
+                ArrayClause cr = new ArrayClause(ps);
                 clauses.add(cr);
                 attachClause(cr);
                 break;
@@ -305,6 +305,47 @@ public boolean addClause(int p, int q, int r) {
         return addClause(temporary_add_vector_);
     }
 
+    /**
+     * Moves the literal with the highest decision level to position 1 in the clause.
+     * This ensures that the second watched literal (at position 1) is the one with the highest
+     * decision level, which can improve propagation efficiency.
+     * The literal at position 0 (the asserting literal) is left unchanged.
+     * 
+     * The method performs an early exit if a literal at the current decision level is found,
+     * as no literal can have a higher level than the current one.
+     *
+     * @param cr the clause to reorganize
+     */
+    private void moveHighestDecisionLitToPos1(ArrayClause cr) {
+        if (cr.size() <= 2) {
+            return; // Nothing to do for binary clauses
+        }
+
+        int currentLevel = trailMarker();
+        int highestPos = 1;
+        int highestLevel = level(var(cr._g(1)));
+
+        // Find the literal with the highest decision level (excluding position 0)
+        for (int i = 2; i < cr.size(); i++) {
+            int litLevel = level(var(cr._g(i)));
+            if (litLevel > highestLevel) {
+                highestLevel = litLevel;
+                highestPos = i;
+                // Early exit: if we found a literal at the current level, no need to continue
+                if (highestLevel == currentLevel) {
+                    break;
+                }
+            }
+        }
+
+        // If a literal with higher level was found, swap it with position 1
+        if (highestPos != 1) {
+            int temp = cr._g(1);
+            cr._s(1, cr._g(highestPos));
+            cr._s(highestPos, temp);
+        }
+    }
+
     /**
      * Add a learnt clause to the solver.
      * If the param unforgettable is true, the clause will not be removed during {@link #doReduceDB()}.
@@ -317,7 +358,8 @@ public void addLearnt(TIntList learnt_clause, boolean unforgettable) {
         if (learnt_clause.size() == 1) {
             uncheckedEnqueue(learnt_clause.get(0));
         } else {
-            Clause cr = new ArrayClause(learnt_clause, true);
+            ArrayClause cr = new ArrayClause(learnt_clause, true);
+            moveHighestDecisionLitToPos1(cr);
             learnts.add(cr);
             if (unforgettable) { // in the case of a solution, for instance.
                 if (learnts.size() > 1) {
@@ -490,7 +532,7 @@ private static boolean isAssertingClause(MiniSat sat, Clause c) {
     // Enqueue a literal. Assumes value of literal is undefined.
     public void uncheckedEnqueue(int l, Clause from) {
         assert valueLit(l) == lUndef : "l: " + printLit(l) + " from: " + from;
-        assert isAssertingClause(this, from.getConflict()) : "the reason " + showReason(from) + " is not valid because it is not unit";
+        assert isAssertingClause(this, from.getConflict()) : "the reason " + showReason(from) + " is not asserting under propagation";
         int v = var(l);
         if (assignment_.getQuick(v) == lUndef) {
             onLiteralPushed(l);
@@ -527,9 +569,9 @@ public void uncheckedEnqueue(int l) {
     }
 
     public void cEnqueue(int l, Reason r) {
-        assert valueLit(l) != lTrue;
+        assert valueLit(l) != lTrue : l + " not true, reason is " + r;
         assert r != null : "reason is null for " + printLit(l);
-        assert isAssertingClause(this, r.getConflict()) : "the reason " + showReason(r) + " is not valid because it is not unit";
+        assert isAssertingClause(this, r.getConflict()) : "the reason " + showReason(r) + " is not asserting under propagation";
         int v = var(l);
         if (valueLit(l) == lFalse) {
             if (r == R_Undef) {
@@ -560,7 +602,7 @@ public void cEnqueue(int l, Reason r) {
     }
 
     // Attach a clause to watcher lists.
-    void attachClause(Clause cr) {
+    void attachClause(ArrayClause cr) {
         assert cr.size() > 1;
         MinimaList<Watcher> l0 = watches_.get(neg(cr._g(0)));
         if (l0 == null) {
@@ -625,7 +667,7 @@ private void propagateLit(int p) {
             }
 
             // Make sure the false literal is data[1]:
-            Clause cr = w.clause;
+            ArrayClause cr = w.clause;
             final int false_lit = neg(p);
             if (cr._g(0) == false_lit) {
                 cr._s(0, cr._g(1));
@@ -645,7 +687,7 @@ private void propagateLit(int p) {
                 continue;
             }
 
-            boolean cont = newWatch(cr, false_lit, w);
+            boolean cont = newWatchCircular(cr, false_lit, w);
 
             // Did not find watch -- clause is unit under assignment:
             if (!cont) {
@@ -672,21 +714,73 @@ private void propagateLit(int p) {
         }
     }
 
-    private boolean newWatch(Clause cr, int false_lit, Watcher w) {
+    private void changeWatchedLiteral(ArrayClause cr, int false_lit, Watcher w, int k) {
+        // Swap: place the new literal in position 1
+        cr._s(1, cr._g(k));
+        cr._s(k, false_lit);
+        // Attach the watcher to the new position
+        MinimaList<Watcher> lw = watches_.get(neg(cr._g(1)));
+        if (lw == null) {
+            lw = new MinimaList<>();
+            watches_.put(neg(cr._g(1)), lw);
+        }
+        lw.add(w);
+    }
+
+    /**
+     * Implements the circular approach for finding a new watched literal in a clause.
+     * This method is based on the optimal implementation of watched literals as described in:
+     * <p>
+     * <i>Optimal Implementation of Watched Literals and More General Techniques</i>
+     * by Ian P. Gent, Journal of Artificial Intelligence Research (JAIR), Volume 48, 2013.
+     * </p>
+     * <p>
+     * The circular approach maintains a pointer ({@code lastScannedLit}) to the last scanned position
+     * in the clause. When searching for a new acceptable literal (one that is not false), it starts
+     * from the position after the last scanned one, and wraps around to the beginning (position 2)
+     * when reaching the end of the clause. The search stops when it returns to the starting position,
+     * ensuring that each literal is checked at most twice per node in the search tree.
+     * </p>
+     * <p>
+     * This approach is proven to be big-O optimal when amortized across the entire search tree,
+     * with a worst-case constant factor of only 2. In contrast to the state restoration method,
+     * this approach is backtrack-stable: it does not require restoring the search position during
+     * backtracking, relying instead on the monotonicity property of acceptability (if a literal
+     * is unacceptable at a node, it remains unacceptable at all descendant nodes).
+     * </p>
+     * <p>
+     * Empirical results from the paper show a 29% speedup in unit propagation when using this
+     * circular approach in MiniSat, though this does not translate to a statistically significant
+     * improvement in overall solver runtime.
+     * </p>
+     *
+     * @param cr the clause in which to find a new watched literal
+     * @param false_lit the literal that has become false (the negated watched literal)
+     * @param w the watcher associated with this clause
+     * @return {@code true} if a new acceptable literal was found and set as the new watched literal,
+     *         {@code false} if no acceptable literal exists in the clause
+     * @see <a href="https://doi.org/10.1613/jair.10772">JAIR Paper DOI</a>
+     */
+    private boolean newWatchCircular(ArrayClause cr, int false_lit, Watcher w) {
+        int last = cr.getLastScannedLit();
+        int lastCache = last;
+        int n = cr.size();
         // Look for new watch:
-        for (int k = 2; k < cr.size(); k++) {
-            if (valueLit(cr._g(k)) != lFalse) {
-                cr._s(1, cr._g(k));
-                cr._s(k, false_lit);
-                MinimaList<Watcher> lw = watches_.get(neg(cr._g(1)));
-                if (lw == null) {
-                    lw = new MinimaList<>();
-                    watches_.put(neg(cr._g(1)), lw);
-                }
-                lw.add(w);
+        do {
+            last++;
+            // If we return to the starting position, there are no valid literals
+            if (last == n) {
+                // By convention, the false literal is at 1 before calling this method
+                last = 1;
+            }
+            // Checks whether the literal at position k is valid
+            if (valueLit(cr._g(last)) != lFalse) {
+                changeWatchedLiteral(cr, false_lit, w, last);
+                // Updates the latest search position
+                cr.setLastScannedLit(last);
                 return true;
             }
-        }
+        } while (lastCache != last);
         return false;
     }
 
@@ -1084,8 +1178,6 @@ public void deleteAllLearnedClauses() {
 
     public void doReduceDB() {
         int i, j;
-        double extra_lim = cla_inc / learnts.size();    // Remove any clause below this activity
-
         learnts.subList(learnt_first_removable, learnts.size())  // only removable clauses
                 .sort(comp);
         // Don't delete binary or locked clauses or unforgettable clauses.
@@ -1268,10 +1360,10 @@ private String showReason(Reason r) {
      */
     private static final class Watcher {
 
-        final Clause clause;
-        int blocker;
+        private final ArrayClause clause;
+        private int blocker;
 
-        Watcher(final Clause cr, int l) {
+        Watcher(final ArrayClause cr, int l) {
             this.clause = cr;
             this.blocker = l;
         }

solver/src/main/java/org/chocosolver/sat/SatDecorator.java

@@ -82,7 +82,7 @@ public void learnClause(int... ps) {
                 ok_ = (confl == C_Undef);
                 return;
             default:
-                Clause cr = new ArrayClause(ps);
+                ArrayClause cr = new ArrayClause(ps);
                 //removeDominated(cr);
                 learnts.add(cr);
                 attachClause(cr);