From 9148a7ebaa48f8c36e8a1ab041020ab9eb114ad5 Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Mon, 26 Jan 2026 17:58:54 +0100 Subject: [PATCH 1/6] try shuffling clauses in minisat (input clauses and learnt clauses at discovery time) --- Minisat/core/Solver.cc | 15 +++++++++++++++ Minisat/core/Solver.h | 2 ++ 2 files changed, 17 insertions(+) diff --git a/Minisat/core/Solver.cc b/Minisat/core/Solver.cc index 581dc301b..1ed14c870 100644 --- a/Minisat/core/Solver.cc +++ b/Minisat/core/Solver.cc @@ -155,6 +155,18 @@ void Solver::releaseVar(Lit l) } } +void Solver::shuffle(vec& v, int from) +{ + static double shuffling_seed = 91648253; + int len = v.size(); + for(unsigned i=from;i& ps) { @@ -171,6 +183,8 @@ bool Solver::addClause_(vec& ps) ps[j++] = p = ps[i]; ps.shrink(i - j); + shuffle(ps); + if (ps.size() == 0) return ok = false; else if (ps.size() == 1){ @@ -726,6 +740,7 @@ lbool Solver::search(int nof_conflicts) if (learnt_clause.size() == 1){ uncheckedEnqueue(learnt_clause[0]); }else{ + 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..1a6e98068 100644 --- a/Minisat/core/Solver.h +++ b/Minisat/core/Solver.h @@ -302,6 +302,8 @@ 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); } + + void shuffle(vec& v, int from = 0); }; From 1f192089aa144665a38b9fc8db532eb7dc011a92 Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Mon, 26 Jan 2026 18:28:24 +0100 Subject: [PATCH 2/6] set minisat seed and set its new shuffle_clauses on randomTraversals() --- Lib/Random.hpp | 10 +++++----- Minisat/core/Solver.cc | 7 +++++-- Minisat/core/Solver.h | 2 ++ SAT/MinisatInterfacing.hpp | 25 +++++++++++++++++-------- Saturation/Splitter.cpp | 10 +++++++--- 5 files changed, 36 insertions(+), 18 deletions(-) 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 1ed14c870..73e7b4ada 100644 --- a/Minisat/core/Solver.cc +++ b/Minisat/core/Solver.cc @@ -66,6 +66,7 @@ Solver::Solver() : , random_var_freq (opt_random_var_freq) , random_seed (opt_random_seed) , luby_restart (opt_luby_restart) + , shuffle_clauses (false) , ccmin_mode (opt_ccmin_mode) , phase_saving (opt_phase_saving) , rnd_pol (false) @@ -183,7 +184,8 @@ bool Solver::addClause_(vec& ps) ps[j++] = p = ps[i]; ps.shrink(i - j); - shuffle(ps); + if (shuffle_clauses) + shuffle(ps); if (ps.size() == 0) return ok = false; @@ -740,7 +742,8 @@ lbool Solver::search(int nof_conflicts) if (learnt_clause.size() == 1){ uncheckedEnqueue(learnt_clause[0]); }else{ - shuffle(learnt_clause,1); + 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 1a6e98068..7c4ea7a59 100644 --- a/Minisat/core/Solver.h +++ b/Minisat/core/Solver.h @@ -139,6 +139,8 @@ class Solver { double random_var_freq; double random_seed; bool luby_restart; + 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. diff --git a/SAT/MinisatInterfacing.hpp b/SAT/MinisatInterfacing.hpp index ac9e44014..5e71eee58 100644 --- a/SAT/MinisatInterfacing.hpp +++ b/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,36 @@ 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; + } + +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..b3511551c 100644 --- a/Saturation/Splitter.cpp +++ b/Saturation/Splitter.cpp @@ -76,11 +76,15 @@ 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()); + inner = minisat; break; + } case Options::SatSolver::CADICAL: - inner = new CadicalInterfacing; + inner = new CadicalInterfacing(); break; #if VZ3 case Options::SatSolver::Z3: From b39412431447f1b545613d2675ee943d29bfd8f0 Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Mon, 26 Jan 2026 18:31:14 +0100 Subject: [PATCH 3/6] warning (stay signed everywhere) --- Minisat/core/Solver.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Minisat/core/Solver.cc b/Minisat/core/Solver.cc index 73e7b4ada..ed60c7ae0 100644 --- a/Minisat/core/Solver.cc +++ b/Minisat/core/Solver.cc @@ -160,7 +160,7 @@ void Solver::shuffle(vec& v, int from) { static double shuffling_seed = 91648253; int len = v.size(); - for(unsigned i=from;i Date: Tue, 27 Jan 2026 10:14:36 +0100 Subject: [PATCH 4/6] move to header, tap to minisat's seed --- Minisat/core/Solver.cc | 19 +++---------------- Minisat/core/Solver.h | 14 ++++++++++++-- 2 files changed, 15 insertions(+), 18 deletions(-) diff --git a/Minisat/core/Solver.cc b/Minisat/core/Solver.cc index ed60c7ae0..d122893b1 100644 --- a/Minisat/core/Solver.cc +++ b/Minisat/core/Solver.cc @@ -156,19 +156,6 @@ void Solver::releaseVar(Lit l) } } -void Solver::shuffle(vec& v, int from) -{ - static double shuffling_seed = 91648253; - int len = v.size(); - for(int i=from;i& ps) { assert(decisionLevel() == 0); @@ -343,7 +330,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]; @@ -516,11 +503,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. |________________________________________________________________________________________________@*/ diff --git a/Minisat/core/Solver.h b/Minisat/core/Solver.h index 7c4ea7a59..1c8a21a0c 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); @@ -305,7 +305,17 @@ class Solver { static inline int irand(double& seed, int size) { return (int)(drand(seed) * size); } - void shuffle(vec& v, int from = 0); + template + void shuffle(vec& v, int from = 0) + { + int len = v.size(); + for(int i=from;i Date: Tue, 27 Jan 2026 10:19:43 +0100 Subject: [PATCH 5/6] implement watches shuffling in Minisat --- Minisat/core/Solver.cc | 4 ++++ Minisat/core/Solver.h | 1 + SAT/MinisatInterfacing.hpp | 4 ++++ Saturation/Splitter.cpp | 1 + 4 files changed, 10 insertions(+) diff --git a/Minisat/core/Solver.cc b/Minisat/core/Solver.cc index d122893b1..efe3bfcbc 100644 --- a/Minisat/core/Solver.cc +++ b/Minisat/core/Solver.cc @@ -66,6 +66,7 @@ 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) @@ -522,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; diff --git a/Minisat/core/Solver.h b/Minisat/core/Solver.h index 1c8a21a0c..4aef99906 100644 --- a/Minisat/core/Solver.h +++ b/Minisat/core/Solver.h @@ -139,6 +139,7 @@ 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). diff --git a/SAT/MinisatInterfacing.hpp b/SAT/MinisatInterfacing.hpp index 5e71eee58..20f29b4b4 100644 --- a/SAT/MinisatInterfacing.hpp +++ b/SAT/MinisatInterfacing.hpp @@ -92,6 +92,10 @@ class MinisatInterfacing : public SATSolver _solver.shuffle_clauses = newVal; } + void setWatchesShuffling(bool newVal) { + _solver.shuffle_watches = newVal; + } + protected: void solveModuloAssumptionsAndSetStatus(unsigned conflictCountLimit = UINT_MAX); diff --git a/Saturation/Splitter.cpp b/Saturation/Splitter.cpp index b3511551c..cb5ec18d9 100644 --- a/Saturation/Splitter.cpp +++ b/Saturation/Splitter.cpp @@ -80,6 +80,7 @@ void SplittingBranchSelector::init() auto minisat = new MinisatInterfacing(); minisat->setSeed(Random::seed()); minisat->setClauseShuffling(_parent.getOptions().randomTraversals()); + minisat->setWatchesShuffling(_parent.getOptions().randomTraversals()); inner = minisat; break; } From dce0ebb84f638be36a05fef98eb69397d470b474 Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Tue, 27 Jan 2026 12:12:02 +0100 Subject: [PATCH 6/6] use std::swap --- Minisat/core/Solver.h | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Minisat/core/Solver.h b/Minisat/core/Solver.h index 4aef99906..906afa46b 100644 --- a/Minisat/core/Solver.h +++ b/Minisat/core/Solver.h @@ -312,9 +312,7 @@ class Solver { int len = v.size(); for(int i=from;i