|Performance comparison between (an initial version of) COMiniSatPS and SWDiA5BY
SAT Competition 2013 Benchmarks (150 SAT/150 UNSAT)
Timeout of 4,200 seconds on Intel Core i5-4460S @ 2.90GHz / 12GB RAM
|The official winner in the industrial SAT track in SAT Competition 2013 is Lingeling (solving 119), but in reality, two other solvers, SINNminisat (solving 120) and minisat_bit (118) should have been the first- and third-place winners, making Lingeling 2nd and ZENN (113) 4th. Surprisingly, the two others were the MiniSat Hack Track solvers, and it is very unfortunate that their authors missed the prizes and thus failed to attract well-deserved attention only because they did not indicate participation in the main track. ... Similarly and interestingly, in 2014 Competition, the winner of the industrial SAT track was again a MiniSat hack solver minisat_blbd. Ironically, however, minisat_blbd performed worse in overall than the MiniSat Hack Track winner MiniSat_HACK_999ED (5th in the SAT track, which is still remarkable), ... Then, organizers of 2011 Competition already reported that there were many good MiniSat hack solvers (including the top two Contrasat and CIR_minisat) for application SAT, and especially, the authors of Glucose noted their use of Luby-series restarts. ... Obviously, very simple solvers with tiny but critical changes can indeed be impressively competitive or even outperform complex state-of-the-art sovers (e.g., in-processing, multi-engine solvers, or machine-learning solvers trained over hundreds of competition instances from past years), the fact that researchers not directly working in practical SAT may find it surprising. However, this is indeed the nature of practical SAT. This unsettling truth has been proven more explicitly in 2014 Competition, e.g., by the great success of SWDiA5BY and our MiniSat_HACK_xxxED hack solvers. However, it should not be assumed hastily that original MiniSat itself is still competitive, which is not at all the case (e.g., look at the result of the Application Certified UNSAT Track of SAT Competition 2013). As such, we felt that now is the time the SAT community needs the next new "MiniSat" whose performance matches that of recent state-of-the-art solvers by and while only minimally adopting simple but truly effective ideas. This would then immensely help the SAT community create new innovations for the coming years, similar to what the past MiniSat derivatives, including Glucose, have contributed. COMiniSatPS thrives to be the next "MiniSat", preferring simplicity over complexity to reach out to wide audience. As such, it is provided as a series of incremental patches to original MiniSat where each small patch adds one feature or enhances implementation, one at a time, to produce a fully functional solver, often changing solver characteristics fundamentally. Researchers, particularly young and new to SAT, would benefit tremendously as it is easy to isolate, study, implement, and adopt the ideas behind each incremental change. The goal is to lower the entering bar so that anyone interested can implement and test their new ideas on a simple solver guaranteed with exceptional performance.|
$ tar zxvf minisat-2.2.0.tar.gz $ cd minisat $ patch -p1 < 01_minisat2glucoseSC13.patch (No error or warning should print for each patch application.) $ patch -p1 < 02_SWDiA5BY_SC14.patch $ patch -p1 < 03_tiny_fixes.patch ... (and so on)Patches will properly modify license information, when necessary. To compile,
$ cd minisat-2.2.0/simp $ MROOT=.. make rs (for static linking) or $ MROOT=.. make rErrors in compiling? If MiniSat does not compile on your platform, neither will COMiniSatPS. The goal of COMiniSatPS is to maintain absolute simplicity for the purpose of effective dissemination of core knowledge (please refer to the Preface section above); I do not attempt to fix it to compile on every platform. However, if you think that something must be fixed, please contact the author.
|01_minisat2glucoseSC13.patch||Turns MiniSat 2.2.0 into Glucose 2.3 that participated in SAT Competitions 2013 and 2014.1 The resulting solver precisely simulates Glucose 2.3, including bugs, to produce the perfectly same execution results of the competitions.2 Does not, however, conform to the output requirements of the competition.|
|02_SWDiA5BY_SC14.patch||Turns it into SWDiA5BY A26 that participated in SAT Competition 2014. The resulting solver precisely simulates SWDiA5BY, including bugs, to produce the perfectly same execution results of the competition.2 Does not, however, conform to the output requirements of the competition.|
|Below are the actual source code of the four versions that entered SAT-Race 2015. The solvers will precisely replicate the competition results. The system description for these solvers can be found on the competition webpage. Apologies for not providing the solvers by patches at the moment.|
|COMiniSatPS_Main_Sequence.zip (2015)||System description on the SAT-Race 2015 webpage.|
|COMiniSatPS_Subdwarf.zip (2015)||Proof-of-concept solver. Parameters are intentionally configured with extreme values. Proves the surprisingly insignificant role of learnt clauses. Should be of theoretical interest only. Don't use it in practice. The solver could have been made better.|
|COMiniSatPS_1Earth.zip (2015)||A version that participated in the Incremental Track. Built to provide a reference implementation of incremental variable elimination . Modified to conform to the format required by the Incremental Track. Requires the environment provided by the competition to compile.|
|COMiniSatPS_1Sun.zip (2015)||Another version that participated in the Incremental Track.|
1 For the 2014 entry, the authors of Glucose specified the version as 3.0, but the code is precisely the same code of Glucose 2.3 that entered the 2013 competition. After all, for sequential SAT solving, there is no real difference between Glucose 2.3, Glucose 3.0, and Glucose 4.0.
2 Logical equivalence in execution, modulo physical properties; e.g., memory consumption, garbage collection frequency, and output messages will differ. However, it is not impossible that the logical equivalence may become broken in certain extremely unlikely cases of, e.g., arithmetic overflow. Please contact the author if you found any instance that results in a different behavior.
MIT - the same license as MiniSat's.
|minisat-2.2.0-to-glucose.patch||Makes MiniSat use LBD and employ Glucose's restart strategy; essentially, it is now Glucose.|
|binary-watches.patch||Implements dedicated watchers for binary clauses as well as simple learnt clause minimization using them.|
 Chanseok Oh. Improving SAT Solvers by Exploiting Empirical Characteristics of CDCL, PhD thesis, New York University
 Chanseok Oh. Patching MiniSat to Deliver Performance of Modern SAT Solvers, SAT-Race'15
 Chanseok Oh. Between SAT and UNSAT: The Fundamental Difference in CDCL SAT, SAT'15
 James Ezick, Jonathan Springer, Tom Henretty, and Chanseok Oh. Extreme SAT-based Constraint Solving with R-Solve, HPEC'14
 Chanseok Oh. COMiniSatPS: A SAT Solver with New Insights, unpublished manuscript--