CryptoMiniSat 4.2 has been released. This release brings multi-threading, some bug fixes, and a lot of code cleanup.

Multi-threading

Multi-threading has been implemented using the std::thread class of C++11. This makes it very portable and at the same time easy to use. Multi-threading is very simple and only shares unitary and binary learnt clauses. This is in comparison to other approaches that have some form of complex clause-sharing algorithms, sometimes even sharing clause databases. However, this system works when it’s used as a library, even with assumptions. Simply call set_num_threads(N) before calling any other functions.

The method used to speed up the system is the portfolio method, i.e. there are many threads started with different parameters and they share some information among them. The threads are configured as:

switch(thread_num) {
case 1: {
    conf.restartType = restart_type_geom;
    conf.polarity_mode = CMSat::polarmode_neg;
    conf.varElimRatioPerIter = 1;
    break;
}
case 2: {
    conf.shortTermHistorySize = 80;
    conf.clauseCleaningType = CMSat::clean_glue_based;
    conf.restartType = CMSat::restart_type_glue;
    conf.increaseClean = 1.08;
    conf.ratioRemoveClauses = 0.55;
    break;
}
case 3: {
    conf.doVarElim = 0;
    conf.doGateFind = 0;
    conf.more_red_minim_limit_cache = 400;
    conf.more_red_minim_limit_binary = 200;
    conf.probe_bogoprops_timeoutM = 3500;
    conf.restartType = CMSat::restart_type_agility;
    conf.ratioRemoveClauses = 0.6;
    break;
}
case 4: {
    conf.simplify_at_startup = 1;
    conf.regularly_simplify_problem = 0;
    conf.varElimRatioPerIter = 1;
    conf.restartType = restart_type_geom;
    conf.clauseCleaningType = CMSat::clean_sum_activity_based;
    conf.polarity_mode = CMSat::polarmode_neg;
    conf.ratioRemoveClauses = 0.65;
    break;
}
case 5: {
    conf.doGateFind = 0;
    conf.more_red_minim_limit_cache = 100;
    conf.more_red_minim_limit_binary = 100;
    conf.probe_bogoprops_timeoutM = 4000;
    conf.ratioRemoveClauses = 0.6;
    break;
}
case 6: {
    conf.numCleanBetweenSimplify = 1;
    conf.skip_some_bve_resolvents = 1;
    conf.ratioRemoveClauses = 0.7;
    break;
}
case 7: {
    conf.clauseCleaningType = CMSat::clean_sum_confl_depth_based;
    conf.ratioRemoveClauses = 0.55;
    break;
}
case 8: {
    conf.polarity_mode = CMSat::polarmode_pos;
    conf.ratioRemoveClauses = 0.6;
    break;
}
case 9: {
    conf.do_bva = 0;
    conf.doGateFind = 0;
    conf.more_red_minim_limit_cache = 800;
    conf.more_red_minim_limit_binary = 400;
    conf.polarity_mode = CMSat::polarmode_neg;
    conf.ratioRemoveClauses = 0.6;
    break;
}
case 10: {
    conf.do_bva = 0;
    conf.doGateFind = 0;
    conf.restartType = CMSat::restart_type_agility;
    conf.clauseCleaningType = CMSat::clean_glue_based;
    conf.ratioRemoveClauses = 0.6;
    break;
}
case 11: {
    conf.simplify_at_startup = 1;
    conf.propBinFirst = 1;
    conf.doLHBR = 1;
    conf.increaseClean = 1.12;
    conf.ratioRemoveClauses = 0.7;
    break;
}
default: {
    conf.clauseCleaningType = CMSat::clean_glue_based;
    conf.ratioRemoveClauses = 0.7;
    break;
}
}

These configurations have been chosen because they seemed to have quite orthogonal parameters. Only 12 threads are properly configured, the rest are not really configured and are only cleaning a lot more clauses than normal (so as not to run out of memory). In a certain sense, the above is the “secret sauce” that makes the parallel system work.

Code cleanup

The code has been greatly refactored. This is an ongoing effort, but its fruits are already quite visible. In general, variable and function names are more meaningful, function sizes have been drastically cut and the expressiveness of the code has been improved.

Unfortunately, C++ (and C) are quite limiting in a number of ways, and so CryptoMiniSat might move to other languages such as Go. Go for example provides reflection and significantly improved compile times. These two are very useful for development: the former greatly simplifies testing while the latter allows for quicker build (and thus debug) cycles.

[paypal-donation]