diff --git a/Lib/Random.hpp b/Lib/Random.hpp index 8c00e9403..167219e91 100644 --- a/Lib/Random.hpp +++ b/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(min,max)(_eng); } - + /** * Return a random bit. */ diff --git a/Minisat/core/Solver.cc b/Minisat/core/Solver.cc index 581dc301b..efe3bfcbc 100644 --- a/Minisat/core/Solver.cc +++ b/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& ps) { assert(decisionLevel() == 0); @@ -171,6 +172,9 @@ bool Solver::addClause_(vec& 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& 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); diff --git a/Minisat/core/Solver.h b/Minisat/core/Solver.h index 2b3c86172..906afa46b 100644 --- a/Minisat/core/Solver.h +++ b/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 + void shuffle(vec& v, int from = 0) + { + int len = v.size(); + for(int i=from;i 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 _assumptions; diff --git a/Saturation/Splitter.cpp b/Saturation/Splitter.cpp index debe2c4fb..cb5ec18d9 100644 --- a/Saturation/Splitter.cpp +++ b/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: