Modifying the method extendGivenModel in SatSolver.cc to accept multiple witnesses from WitnessIterator (CaDiCaL)

Author: marekpiotrow

CadicalWrap.h

@@ -99,34 +99,12 @@ class SimpSolver {
     class ExtendIterator : public CaDiCaL::WitnessIterator {
     public:
         vec<uint32_t> elimCls;
-    private:
-        static void mkElimClause(vec<uint32_t>& elimclauses, Var v, const std::vector<int> &cl)
-        {
-            size_t first = elimclauses.size();      
-            int v_pos = -1;
-
-            // Copy clause to elimclauses-vector. Remember position where the
-            // variable 'v' occurs:
-            for (size_t i = 0; i < cl.size(); i++) {
-                Lit lit = mkLit(abs(cl[i]) - 1, cl[i] < 0);
-                elimclauses.push(toInt(lit));
-                if (var(lit) == v) v_pos = int(i + first);
-            }
-            assert(v_pos != -1);
-
-            // Swap the first literal with the 'v' literal, so that the literal
-            // containing 'v' will occur first in the clause:
-            uint32_t tmp = elimclauses[v_pos];
-            elimclauses[v_pos] = elimclauses[first];
-            elimclauses[first] = tmp;
-
-            // Store the length of the clause last:
-            elimclauses.push(cl.size());
-        }
     public:
         bool witness (const std::vector<int> &cl, const std::vector<int> &witness, uint64_t ) {
-            Lit l = mkLit(abs(witness[0]) - 1, witness[0] < 0);
-            mkElimClause(elimCls,var(l), cl);
+            for (const int w : witness) elimCls.push(toInt(mkLit(abs(w) - 1, w < 0)));
+            elimCls.push(witness.size());
+            for (const int c : cl) elimCls.push(toInt(mkLit(abs(c) - 1, c < 0)));
+            elimCls.push(cl.size());
             return true;
         }
     } extendIt;

SatSolver.cc

@@ -57,23 +57,41 @@ bool ExtSimpSolver::reduceProblem()
     return res;
 }
 
-#if !defined(CRYPTOMS)
 void ExtSimpSolver::extendGivenModel(vec<lbool> &model)
 {
+#if defined(CADICAL)
+    for (int i = model.size() - 1; i >= 0; i--)
+        if (model[i] == l_Undef) model[i] = l_False;
+    for (int j, i = elimClauses.size()-1; i > 0; i -= j) {
+        Lit x;
+        for (j = elimClauses[i--]; j > 0; j--, i--) { // clause processing
+            x = Minisat::toLit(elimClauses[i]);
+            if ((model[var(x)] ^ sign(x)) == l_True) { // the clause is satisfied
+                i -= elimClauses[i-j] + 1; // skip witnesses
+                goto next;             }
+        }
+        for (j = elimClauses[i--]; j > 0; j--, i--) { // witnesses processing
+            x = Minisat::toLit(elimClauses[i]);
+            if ((model[var(x)] ^ sign(x)) != l_True) //  x is not satisfied
+                model[var(x)] = (model[var(x)] == l_True ? l_False : l_True); // x is flipped
+        }
+next:;
+    }
+#elif !defined(CRYPTOMS)
     for (int j, i = elimClauses.size()-1; i > 0; i -= j) {
         Lit x;
         for (j = elimClauses[i--]; j > 1; j--, i--) {
             x = Minisat::toLit(elimClauses[i]);
-            if ((model[var(x)] ^ sign(x)) != l_False) goto next; // x is no false in the model
+            if ((model[var(x)] ^ sign(x)) != l_False) goto next; // x is not false in the model
         }
         x = Minisat::toLit(elimClauses[i]);
         model[var(x)] = lbool(!sign(x));
 next:;
     }
-}
 #else
-void ExtSimpSolver::extendGivenModel(vec<lbool> &) {}
+    (void)model;
 #endif
+}
 
 void ExtSimpSolver::printVarsCls(bool encoding, const vec<Pair<weight_t, Minisat::vec<Lit>* > > *soft_cls, int soft_cnt)
 {