Shuffle minisat

Lib/Random.hpp

@@ -32,12 +32,12 @@ namespace Lib
  * A fully static class for random number generation. Optimized to generate
  * random bits.
  */
-class Random 
+class Random
 {
-  /* 
-   * An entertaining talk on why using the c++11 approach is an improvement 
+  /*
+   * An entertaining talk on why using the c++11 approach is an improvement
    * over the old C style via rand():
-   * 
+   *
    * https://channel9.msdn.com/Events/GoingNative/2013/rand-Considered-Harmful
    *
    * Still, this is not reproducible across platforms
@@ -56,7 +56,7 @@ class Random
   static double getDouble(double min, double max) {
     return std::uniform_real_distribution<double>(min,max)(_eng);
   }
-  
+
   /**
    * Return a random bit.
    */

Minisat/core/Solver.cc

@@ -66,6 +66,8 @@ Solver::Solver() :
   , random_var_freq  (opt_random_var_freq)
   , random_seed      (opt_random_seed)
   , luby_restart     (opt_luby_restart)
+  , shuffle_watches  (false)
+  , shuffle_clauses  (false)
   , ccmin_mode       (opt_ccmin_mode)
   , phase_saving     (opt_phase_saving)
   , rnd_pol          (false)
@@ -155,7 +157,6 @@ void Solver::releaseVar(Lit l)
     }
 }
 
-
 bool Solver::addClause_(vec<Lit>& ps)
 {
     assert(decisionLevel() == 0);
@@ -171,6 +172,9 @@ bool Solver::addClause_(vec<Lit>& ps)
             ps[j++] = p = ps[i];
     ps.shrink(i - j);
 
+    if (shuffle_clauses)
+        shuffle(ps);
+
     if (ps.size() == 0)
         return ok = false;
     else if (ps.size() == 1){
@@ -327,7 +331,7 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
                     out_learnt.push(q);
             }
         }
-        
+
         // Select next clause to look at:
         while (!seen[var(trail[index--])]);
         p     = trail[index+1];
@@ -500,11 +504,11 @@ void Solver::uncheckedEnqueue(Lit p, CRef from)
 /*_________________________________________________________________________________________________
 |
 |  propagate : [void]  ->  [Clause*]
-|  
+|
 |  Description:
 |    Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
 |    otherwise CRef_Undef.
-|  
+|
 |    Post-conditions:
 |      * the propagation queue is empty, even if there was a conflict.
 |________________________________________________________________________________________________@*/
@@ -519,6 +523,9 @@ CRef Solver::propagate()
         Watcher        *i, *j, *end;
         num_props++;
 
+        if (shuffle_watches)
+            shuffle(ws);
+
         for (i = j = (Watcher*)ws, end = i + ws.size();  i != end;){
             // Try to avoid inspecting the clause:
             Lit blocker = i->blocker;
@@ -726,6 +733,8 @@ lbool Solver::search(int nof_conflicts)
             if (learnt_clause.size() == 1){
                 uncheckedEnqueue(learnt_clause[0]);
             }else{
+                if (shuffle_clauses)
+                    shuffle(learnt_clause,1);
                 CRef cr = ca.alloc(learnt_clause, true);
                 learnts.push(cr);
                 attachClause(cr);

Minisat/core/Solver.h

@@ -91,7 +91,7 @@ class Solver {
     void    toDimacs     (const char* file, Lit p);
     void    toDimacs     (const char* file, Lit p, Lit q);
     void    toDimacs     (const char* file, Lit p, Lit q, Lit r);
-    
+
     // Variable mode:
     // 
     void    suggestPolarity(Var v, bool b);
@@ -139,6 +139,9 @@ class Solver {
     double    random_var_freq;
     double    random_seed;
     bool      luby_restart;
+    bool      shuffle_watches;    // MS: randomize traversal of the watched literals
+    bool      shuffle_clauses;    // MS: add clause shuffling, for both intput clauses and learnt ones
+                                  // (NB: shuffling input clauses on client size does not work, as internal processing sorts first)
     int       ccmin_mode;         // Controls conflict clause minimization (0=none, 1=basic, 2=deep).
     int       phase_saving;       // Controls the level of phase saving (0=none, 1=limited, 2=full).
     bool      rnd_pol;            // Use random polarities for branching heuristics.
@@ -302,6 +305,16 @@ class Solver {
     // Returns a random integer 0 <= x < size. Seed must never be 0.
     static inline int irand(double& seed, int size) {
         return (int)(drand(seed) * size); }
+
+    template <typename T>
+    void shuffle(vec<T>& v, int from = 0)
+    {
+        int len = v.size();
+        for(int i=from;i<len;i++){
+            int j = irand(random_seed,len-i)+i;
+            std::swap(v[i],v[j]);
+        }
+    }
 };
 
 

SAT/MinisatInterfacing.hpp

@@ -53,7 +53,7 @@ class MinisatInterfacing : public SATSolver
 
   void suggestPolarity(unsigned var, unsigned pol) override {
     // 0 -> true which means negated, e.g. false in the model
-    bool mpol = pol ? false : true; 
+    bool mpol = pol ? false : true;
     _solver.suggestPolarity(vampireVar2Minisat(var),mpol);
   }
 
@@ -83,27 +83,40 @@ class MinisatInterfacing : public SATSolver
     return minimizePremiseList(premises, assumps);
   }
 
-protected:    
+  void setSeed(unsigned seed) {
+    ASS_NEQ(seed,0)
+    _solver.random_seed = seed;
+  }
+
+  void setClauseShuffling(bool newVal) {
+    _solver.shuffle_clauses = newVal;
+  }
+
+  void setWatchesShuffling(bool newVal) {
+    _solver.shuffle_watches = newVal;
+  }
+
+protected:
   void solveModuloAssumptionsAndSetStatus(unsigned conflictCountLimit = UINT_MAX);
-  
+
   Minisat::Var vampireVar2Minisat(unsigned vvar) {
     ASS_G(vvar,0); ASS_LE(vvar,(unsigned)_solver.nVars());
     return (vvar-1);
   }
-  
+
   unsigned minisatVar2Vampire(Minisat::Var mvar) {
     return (unsigned)(mvar+1);
   }
-  
+
   const Minisat::Lit vampireLit2Minisat(SATLiteral vlit) {
-    return Minisat::mkLit(vampireVar2Minisat(vlit.var()),!vlit.positive()); 
+    return Minisat::mkLit(vampireVar2Minisat(vlit.var()),!vlit.positive());
   }
-  
+
   /* sign=true in minisat means "negated" in vampire */
   const SATLiteral minisatLit2Vampire(Minisat::Lit mlit) {
     return SATLiteral(minisatVar2Vampire(Minisat::var(mlit)),Minisat::sign(mlit) ? 0 : 1);
   }
-  
+
 private:
   Status _status = Status::SATISFIABLE;
   Minisat::vec<Minisat::Lit> _assumptions;

Saturation/Splitter.cpp

@@ -76,11 +76,16 @@ void SplittingBranchSelector::init()
 
   SATSolver *inner;
   switch(_parent.getOptions().satSolver()){
-    case Options::SatSolver::MINISAT:
-      inner = new MinisatInterfacing;
+    case Options::SatSolver::MINISAT: {
+      auto minisat = new MinisatInterfacing();
+      minisat->setSeed(Random::seed());
+      minisat->setClauseShuffling(_parent.getOptions().randomTraversals());
+      minisat->setWatchesShuffling(_parent.getOptions().randomTraversals());
+      inner = minisat;
       break;
+    }
     case Options::SatSolver::CADICAL:
-      inner = new CadicalInterfacing;
+      inner = new CadicalInterfacing();
       break;
 #if VZ3
     case Options::SatSolver::Z3: