Skip to content

Commit

Permalink
Removing dependency on non-standard MersenneTwister
Browse files Browse the repository at this point in the history
  • Loading branch information
@msoos
msoos committed Oct 21, 2023
1 parent 8d09e7a commit b883c33
Show file tree
Hide file tree
Showing 19 changed files with 47 additions and 503 deletions.
423 changes: 0 additions & 423 deletions src/MersenneTwister.h
View file

This file was deleted.

4 changes: 4 additions & 0 deletions src/cnf.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ THE SOFTWARE.

#include <atomic>
#include <limits>
#include <random>

#include "constants.h"
#include "vardata.h"
Expand All @@ -45,6 +46,7 @@ THE SOFTWARE.
#include <boost/serialization/vector.hpp>
#endif


namespace CMSat {

class ClauseAllocator;
Expand Down Expand Up @@ -105,6 +107,7 @@ class CNF
if (_conf != NULL) {
conf = *_conf;
}
mtrand.seed(conf.origSeed);
frat = new Drat;
assert(_must_interrupt_inter != NULL);
must_interrupt_inter = _must_interrupt_inter;
Expand All @@ -119,6 +122,7 @@ class CNF

ClauseAllocator cl_alloc;
SolverConf conf;
std::mt19937_64 mtrand;

bool ok = true; //If FALSE, state of CNF is UNSAT

Expand Down
7 changes: 7 additions & 0 deletions src/constants.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,13 @@ THE SOFTWARE.
#include <cstdlib>
#include <stdio.h>
#include <limits>
#include <random>

#define unif_uint_dist(x,y) std::uniform_int_distribution<> x(0, y)
inline uint32_t rnd_uint(std::mt19937_64& mtrand, const uint32_t maximum) {
unif_uint_dist(u, maximum);
return u(mtrand);
}

This comment has been minimized.

Sign in to view

Copy link
@horenmar

horenmar Dec 21, 2023

Contributor

Two quick notes on this

  1. there is a type mismatch between the defaulted std::uniform_int_distribution<> and the return type -> the default is to return ints, not uint32_t. This mismatch can carry performance penalty, depending on how the distribution internally converts between types.

  2. This change means that the randomness in CMSat is no longer reproducible across different platforms (stdlibs) or their versions. Just on Windows, CMSat compiled with VS 2019 and VS 2022 will give different results for the same seed. The issue is that while the generators from <random> are specified to be reproducible, the distributions are not, and in fact various platforms have changed the underlying algorithms for uniform int distribution recently.

This comment has been minimized.

Sign in to view

Copy link
@msoos

msoos Dec 21, 2023

Author Owner

Wow, thank you so much for this comment! This is SUPER helpful.

Thankfully, I can use std::uniform_int_distribution<uint32_t> to fix the uint32_t problem. I'll fix that in a sec.

But the non-reproducibility really bugs me. I don't really know what to do. I MUST have a portable system. And MTRand was super-cool but NOT portable. So CMS didn't even compile properly for ARM. That was unacceptable, given how popular ARM is. Do you have a suggestion how to fix?

This comment has been minimized.

Sign in to view

Copy link
@horenmar

horenmar Dec 21, 2023

Contributor

Either bring in distributions from a library, or write your own. I picked the latter for Catch2, because I don't want to add more dependencies and it is not particularly hard even if you go more generic than the standard. (commit1, commit2)

The reason just bringing in a library works is that there isn't anything nonportable about uniform integer distributions -> as long as the code remains the same, there is no reason to get different results on different platforms.

I would also recommend bringing in (again either via a library dependency or a rewrite) a better PRNG (e.g. xoshiro or PCG). While MT is the best one from <random>, it is still pretty bad due to being comparatively slow and extremely large.

This comment has been minimized.

Sign in to view

Copy link
@msoos

msoos Dec 21, 2023

Author Owner

Ah, thanks for the pro tips! I'll fix that tomorrow :)

This comment has been minimized.

Sign in to view

Copy link
@horenmar

horenmar Dec 21, 2023 •
edited
Loading

Contributor

Also please note that std::shuffle is not reproducible across platforms, for exactly the same reason that the distributions are not.

This comment has been minimized.

Sign in to view

Copy link
@msoos

msoos Jan 13, 2024

Author Owner

First of all, thank you for the detailed feedback! It really helped me.

I decided that having my own algorithm for everything is kinda unmanageable for me, personally. I also use std::sort, and that does the same, too. std::multimap's iterator will likely also be the same (same key, multiple elements -> different order). I can't write a multimap, I can't write a sort, and I don't think I want to use "bare minimum C++" without all the help that I can get. I could import a library for everything, and hope that the library implementation doesn't change and is correct, but I find that very tedious. Is there some very good reason why I would need to have this reproducible across all platforms? I am afraid that it's just too much work 😢 Let me know what you think. In the meanwhile, I think I'll leave it as-is.

Regarding performance -- MTRand is good enough for me. It's probably running less than 0.1% of the time. If it runs more than 1% of the time on any serious problem (takes > 10s to solve), I owe you a beer. I don't want to spend my time to squeeze 1%. If I implemented important optimizations, I could easily get 10-20% (e.g. via SBVA).

I value your feedback, and it made me think about things, honestly. But I think that my time is likely best spent elsewhere -- users are more interested in other things, e.g. performance and ease-of-compile (currently, I lack a Windows binary, which I'll add by moving away from boost, for example).

Thanks again for all the detailed info! I fixed the uint vs int thing, I'll release it soon, it's on an unreleased branch, but it's coming :)

// #define VERBOSE_DEBUG
// #define VERBOSE_DEBUG_FULLPROP
Expand Down
6 changes: 2 additions & 4 deletions src/distillerbin.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -109,7 +109,7 @@ bool DistillerBin::distill_bin_cls_all(
const Lit lit = Lit::toLit(i);
todo.push_back(lit);
}
std::shuffle(todo.begin(), todo.end(), std::default_random_engine(solver->mtrand.randInt()));
std::shuffle(todo.begin(), todo.end(), solver->mtrand);
for(const auto& lit: todo) {
time_out = go_through_bins(lit);
if (time_out || !solver->okay()) {
Expand Down Expand Up @@ -208,9 +208,7 @@ bool DistillerBin::try_distill_bin(
#endif

//Try different ordering
if (solver->mtrand.randInt(1) == 1) {
std::swap(lit1, lit2);
}
if (rnd_uint(solver->mtrand, 1) == 1) std::swap(lit1, lit2);

//Disable this clause
findWatchedOfBin(solver->watches, lit1, lit2, false, w.get_ID()).mark_bin_cl();
Expand Down
6 changes: 3 additions & 3 deletions src/distillerlong.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ THE SOFTWARE.

#include "distillerlong.h"
#include "clausecleaner.h"
#include "constants.h"
#include "time_mem.h"
#include "solver.h"
#include "watchalgos.h"
Expand Down Expand Up @@ -282,10 +283,9 @@ bool DistillerLong::distill_long_cls_all(
exit(-1);
#endif
} else if (solver->conf.distill_sort == 4) {
bool randomly_sort = solver->mtrand.randInt(solver->conf.distill_rand_shuffle_order_every_n) == 0;
bool randomly_sort = rnd_uint(solver->mtrand, solver->conf.distill_rand_shuffle_order_every_n) == 0;
if (randomly_sort) {
std::mt19937 gen(solver->mtrand.randInt());
std::shuffle(offs.begin(), offs.end(), gen);
std::shuffle(offs.begin(), offs.end(), solver->mtrand);
} else {
std::sort(offs.begin(),
offs.end(),
Expand Down
15 changes: 3 additions & 12 deletions src/distillerlongwithimpl.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@ THE SOFTWARE.
#include "clauseallocator.h"
#include "sqlstats.h"

#include <algorithm>
#include <iomanip>
using namespace CMSat;
using std::cout;
Expand Down Expand Up @@ -267,19 +268,9 @@ bool DistillerLongWithImpl::remove_or_shrink_clause(Clause& cl, ClOffset& offset
return true;
}

void DistillerLongWithImpl::randomise_order_of_clauses(
vector<ClOffset>& clauses
) {
if (clauses.empty())
return;

void DistillerLongWithImpl::randomise_order_of_clauses(vector<ClOffset>& clauses) {
timeAvailable -= (long)clauses.size()*2;
for(size_t i = 0; i < clauses.size()-1; i++) {
std::swap(
clauses[i]
, clauses[i + solver->mtrand.randInt(clauses.size()-i-1)]
);
}
std::shuffle(clauses.begin(), clauses.end(), solver->mtrand);
}

uint64_t DistillerLongWithImpl::calc_time_available(
Expand Down
2 changes: 1 addition & 1 deletion src/gatefinder.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,7 @@ void GateFinder::find_or_gates()
if (solver->nVars() < 1)
return;

const size_t offs = solver->mtrand.randInt(solver->nVars()*2-1);
const size_t offs = rnd_uint(solver->mtrand, solver->nVars()*2-1);
for(size_t i = 0
; i < solver->nVars()*2
&& *simplifier->limit_to_decrease > 0
Expand Down
8 changes: 1 addition & 7 deletions src/heap.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#ifndef Glucose_Heap_h
#define Glucose_Heap_h

#include <iostream>
#include "Vec.h"
#include "MersenneTwister.h"

namespace CMSat {

Expand Down Expand Up @@ -118,12 +118,6 @@ class Heap {
assert(index < (int)heap.size());
return heap[index];
}
int random_element(MTRand& rnd)
{
assert(!heap.empty());
return heap[rnd.randInt(heap.size()-1)];
}


void decrease (int n)
{
Expand Down
17 changes: 3 additions & 14 deletions src/intree.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ THE SOFTWARE.
#include "sqlstats.h"
#include "watchalgos.h"

#include <algorithm>
#include <cmath>
#include <cassert>

Expand Down Expand Up @@ -166,7 +167,8 @@ bool InTree::intree_probe()
start_bogoprops = solver->propStats.bogoProps;

fill_roots();
randomize_roots();
//randomize_roots
std::shuffle(roots.begin(), roots.end(), solver->mtrand);

//Let's enqueue all ~root -s.
for(Lit lit: roots) enqueue(~lit, lit_Undef, false, 0);
Expand Down Expand Up @@ -223,19 +225,6 @@ void InTree::unmark_all_bins()
}
}

void InTree::randomize_roots()
{
for (size_t i = 0
; i + 1< roots.size()
; i++
) {
std::swap(
roots[i]
, roots[i+solver->mtrand.randInt(roots.size()-1-i)]
);
}
}

void InTree::tree_look()
{
assert(failed.empty());
Expand Down
1 change: 0 additions & 1 deletion src/intree.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,6 @@ class InTree

bool check_timeout_due_to_hyperbin();
void unmark_all_bins();
void randomize_roots();
bool handle_lit_popped_from_queue(
const Lit lit, const Lit propagating, const bool red, const int32_t ID);
bool empty_failed_list();
Expand Down
4 changes: 2 additions & 2 deletions src/occsimplifier.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -738,7 +738,7 @@ void OccSimplifier::eliminate_empty_resolvent_vars()
assert(solver->watches.get_smudged_list().empty());
if (solver->nVars() == 0) goto end;

for(size_t var = solver->mtrand.randInt(solver->nVars()-1), num = 0
for(size_t var = rnd_uint(solver->mtrand,solver->nVars()-1), num = 0
; num < solver->nVars() && *limit_to_decrease > 0
; var = (var + 1) % solver->nVars(), num++
) {
Expand Down Expand Up @@ -2464,7 +2464,7 @@ bool OccSimplifier::ternary_res()
Sub1Ret sub1_ret;

//NOTE: the "clauses" here will change in size as we add resolvents
size_t at = solver->mtrand.randInt(clauses.size()-1);
size_t at = rnd_uint(solver->mtrand, clauses.size()-1);
for(size_t i = 0; i < clauses.size(); i++) {
ClOffset offs = clauses[(at+i) % clauses.size()];
Clause * cl = solver->cl_alloc.ptr(offs);
Expand Down
7 changes: 5 additions & 2 deletions src/propengine.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,9 @@ THE SOFTWARE.
#include "cnf.h"
#include "watchalgos.h"
#include "gqueuedata.h"
#include <random>

using std::mt19937_64;

namespace CMSat {

Expand Down Expand Up @@ -158,13 +161,13 @@ struct RandHeap
return true;
}

uint32_t get_random_element(MTRand& mtrand)
uint32_t get_random_element(mt19937_64& mtrand)
{
if (vars.empty()) {
return var_Undef;
}

uint32_t which = mtrand.randInt(vars.size()-1);
uint32_t which = rnd_uint(mtrand, vars.size()-1);
uint32_t picked = vars[which];
std::swap(vars[which], vars[vars.size()-1]);
vars.pop_back();
Expand Down
8 changes: 4 additions & 4 deletions src/searcher.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,6 @@ Searcher::Searcher(const SolverConf *_conf, Solver* _solver, std::atomic<bool>*
, _solver
, _must_interrupt_inter
)
, mtrand(conf.origSeed)
, solver(_solver)
, cla_inc(1)
{
Expand Down Expand Up @@ -2407,9 +2406,10 @@ void Searcher::setup_polarity_strategy()

if ((polarity_strategy_at % 8) == 0) {
for(auto& v: varData) {
v.best_polarity = mtrand.randInt(1);
v.stable_polarity = mtrand.randInt(1);
v.saved_polarity = mtrand.randInt(1);
unif_uint_dist(u, 1);
v.best_polarity = u(mtrand);
v.stable_polarity = u(mtrand);
v.saved_polarity = u(mtrand);
}
}

Expand Down
8 changes: 4 additions & 4 deletions src/searcher.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,11 +25,11 @@ THE SOFTWARE.

#include <array>

#include "constants.h"
#include "propengine.h"
#include "solvertypes.h"
#include "time_mem.h"
#include "hyperengine.h"
#include "MersenneTwister.h"
#include "simplefile.h"
#include "searchstats.h"
#include "searchhist.h"
Expand Down Expand Up @@ -83,7 +83,6 @@ class Searcher : public HyperEngine
bool must_abort(lbool status);
PropBy insert_gpu_clause(Lit* lits, uint32_t count);
uint64_t luby_loop_num = 0;
MTRand mtrand; ///< random number generator
void set_seed(const uint32_t seed);


Expand Down Expand Up @@ -588,8 +587,9 @@ inline bool Searcher::pick_polarity(const uint32_t var)
case PolarityMode::polarmode_pos:
return true;

case PolarityMode::polarmode_rnd:
return mtrand.randInt(1);
case PolarityMode::polarmode_rnd: {
return rnd_uint(mtrand, 1);
}

case PolarityMode::polarmode_automatic:
assert(false);
Expand Down
7 changes: 2 additions & 5 deletions src/solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3140,8 +3140,7 @@ bool Solver::full_probe(const bool bin_only)
if (value(l) == l_Undef && varData[i].removed == Removed::none)
vars.push_back(i);
}
std::mt19937 g(mtrand.randInt());
std::shuffle(vars.begin(), vars.end(), g);
std::shuffle(vars.begin(), vars.end(), mtrand);

for(auto const& v: vars) {
if ((int64_t)solver->propStats.bogoProps > start_bogoprops + bogoprops_to_use)
Expand Down Expand Up @@ -5502,9 +5501,7 @@ bool Solver::backbone_simpl(int64_t orig_max_confl, bool cmsgen, bool& finished)
if (varData[var].removed != Removed::none) continue;
var_order.push_back(var);
}
std::mt19937 g;
g.seed(mtrand.randInt());
std::shuffle(var_order.begin(), var_order.end(), g);
std::shuffle(var_order.begin(), var_order.end(), mtrand);

int64_t orig_max_props = orig_max_confl*1000LL;
if (orig_max_props < orig_max_confl) orig_max_props = orig_max_confl;
Expand Down
2 changes: 1 addition & 1 deletion src/str_impl_w_impl.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ bool StrImplWImpl::str_impl_w_impl()
return solver->okay();

//Randomize starting point
size_t upI = solver->mtrand.randInt(solver->watches.size()-1);
size_t upI = rnd_uint(solver->mtrand, solver->watches.size()-1);
size_t numDone = 0;
for (; numDone < solver->watches.size() && timeAvailable > 0
; upI = (upI +1) % solver->watches.size(), numDone++
Expand Down
2 changes: 1 addition & 1 deletion src/subsumeimplicit.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -137,7 +137,7 @@ void SubsumeImplicit::subsume_implicit(const bool check_stats, std::string calle
}

//Randomize starting point
const size_t rnd_start = solver->mtrand.randInt(solver->watches.size()-1);
const size_t rnd_start = rnd_uint(solver->mtrand, solver->watches.size()-1);
size_t numDone = 0;
for (;numDone < solver->watches.size() && timeAvailable > 0 && !solver->must_interrupt_asap()
;numDone++
Expand Down
21 changes: 4 additions & 17 deletions src/subsumestrengthen.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ THE SOFTWARE.
#include "solver.h"
#include "solvertypes.h"
#include "subsumeimplicit.h"
#include <algorithm>
#include <array>

//#define VERBOSE_DEBUG
Expand Down Expand Up @@ -226,20 +227,6 @@ bool SubsumeStrengthen::backw_sub_str_with_long(
return solver->okay();
}

void SubsumeStrengthen::randomise_clauses_order()
{
const size_t sz = simplifier->clauses.size();
for (size_t i = 0
; i + 1 < sz
; i++
) {
std::swap(
simplifier->clauses[i]
, simplifier->clauses[i+solver->mtrand.randInt(simplifier->clauses.size()-1-i)]
);
}
}

void SubsumeStrengthen::backw_sub_long_with_long()
{
//If clauses are empty, the system below segfaults
Expand All @@ -250,7 +237,7 @@ void SubsumeStrengthen::backw_sub_long_with_long()
size_t wenThrough = 0;
Sub0Ret sub0ret;
const int64_t orig_limit = simplifier->subsumption_time_limit;
randomise_clauses_order();
std::shuffle(simplifier->clauses.begin(), simplifier->clauses.end(), solver->mtrand);
const size_t max_go_through =
solver->conf.subsume_gothrough_multip*(double)simplifier->clauses.size();

Expand Down Expand Up @@ -317,7 +304,7 @@ bool SubsumeStrengthen::backw_str_long_with_long()
const int64_t orig_limit = *simplifier->limit_to_decrease;
Sub1Ret ret;

randomise_clauses_order();
std::shuffle(simplifier->clauses.begin(), simplifier->clauses.end(), solver->mtrand);
while(*simplifier->limit_to_decrease > 0
&& wenThrough < 1.5*(double)2*simplifier->clauses.size()
&& solver->okay()
Expand Down Expand Up @@ -1009,7 +996,7 @@ bool SubsumeStrengthen::backw_sub_str_long_with_bins()

//Randomize start in the watchlist
size_t upI;
upI = solver->mtrand.randInt(solver->watches.size()-1);
upI = rnd_uint(solver->mtrand, solver->watches.size()-1);

size_t numDone = 0;
for (; numDone < solver->watches.size() && *simplifier->limit_to_decrease > 0
Expand Down
2 changes: 0 additions & 2 deletions src/subsumestrengthen.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -105,8 +105,6 @@ class SubsumeStrengthen
, const cl_abst_type abs
);

void randomise_clauses_order();

template<class T>
uint32_t find_smallest_watchlist_for_clause(const T& ps) const;

Expand Down

0 comments on commit b883c33

Please sign in to comment.