[To Author's Home] [MapleCOMSPS]


COMiniSatPS (a.k.a. COMSPS)

COMiniSatPS is a new and innovative CDCL SAT solver incarnated from the family of our initial prototypes (SWDiA5BY and MiniSat_HACK_xxxED) that were highly successful to have collectively won six medals in SAT Competition 2014 and Configurable SAT Solver Challenge 2014. Thriving to become the next "MiniSat", COMiniSatPS is provided as a series of small diff patches to MiniSat, for the purpose of rapid and wide dissemination of minimally essential knowledge to compose a highly competitive solvers of these days. Compared to award-winning SWDiA5BY (which would also have won the application track with smaller timeouts around 1,000 seconds), the performance of COMiniSatPS has been significantly improved with new innovations.

 SWDiA5BYCOMiniSatPS
SAT109133
UNSAT123132
Total Solved232265
Timeouts6835
  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

If you have a cool idea about SAT and if you think you can implement it on MiniSat, you can do it easily right on top of COMiniSatPS. No matter what the idea is, I encourge you to enter each year's SAT-related competitions; winning competitions is very possible. Moreover, you are contributing to the SAT community way more than you think; every year, I learn new things from the results of many different solvers participating in the competitions.

If you want to cite COMiniSatPS or SWDiA5BY, please site [1]. (See the papers section at the bottom of this page.)

______
This work was supported in part by NSF grant CCS-1350574.


Preface

The following paragraphs are (slightly modified) excerpts from [5]:

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.

SWDiA5BY Principle

Do you think learnt clauses are important? Yes, you do. Really? You may be interested in reading [1] and [2]. Especially, the Subdwarf version of COMiniSatPS described in [2] may surprise you once you look at the SAT-Race 2015 competition result. (However, Subdwarf should be of theoretical interest only as it is strictly a proof-of-concept solver that could have been made better. Don't use it in practice.)


COMiniSatPS Principle

In short, employ different strategies when searching for a satisfying assignment (for targeting satisfiable instances) and when trying to derive an empty clause (for targeting unsatisfiable instances); you should be able to do much better [1]. Particularly, it is relatively easy to make a solver much stronger on satisfiable (or unsatisfiable) instances by scarificing performance on unsatisfiable (or satisfiable, respectively) instances, and there exist many ways of achieving that. Unfortunately, there exist adverse forces between proving satisfiability and proving unsatisfiability in this regard. It is not easy to have great performance improvement in both cases at the same time. However, it is definitely possible.


Building COMiniSatPS

Each diff patch will yield a fully functional SAT solver. To start, download MiniSat 2.2.0 from the official web page: http://minisat.se/MiniSat.html. (Don't use the GitHub version.) This is the version that organizers of SAT Competitions 2013 and 2014 used as a base solver. Next, download and apply the patches provided in the download section, in order (you don't have to apply all of them though), e.g.,

   $ 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 r
Errors 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.


Patch Downloads

[Sep 1, 2017] The source of the solvers that actually participated in SAT Competitions after 2015 is not available here. (Sorry.) Please download the solvers at the respective competition webpage.

[Sep 27, 2015] The source of the solvers that actually participated in SAT-Race 2015 is now available but not in the format of patches for the moment.

Patch FileDescription
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 [2]. 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.


License

MIT - the same license as MiniSat's.


Bonus - MiniSat to Glucose

Glucose itself is, in general, a huge leap forward from MiniSat in terms of performance. (For example, Glucose 2.3 was ranked 2nd in the Application UNSAT Track at SAT-COMP 2014.)

I emphasize that turning MiniSat into Glucose requires only small changes in code; small enough to consider it a hack. In fact, many researchers have been doing it for the MiniSat Hack Track in the past SAT Competitions. By just doing it, you are already starting far ahead of others, so please do it! If you don't and instead use original MiniSat, you basically cannot compete with others. However, never forget the possibility that there may be hidden virtues of MiniSat (or any techniques that we now consider obsolete) that we may be blindly discarding, judging only from the general fact that Glucose is superior than MiniSat. One such example is the Luby-series restarts [1].

The first main patch "01_minisat2glucoseSC13.patch" is small enough to understand what are the essence of Glucose, but to further facilitate knowledge dissemination, I broke it down into the following two patches. The patches have been over-simplified for the said purpose (e.g., not safe to parallelize), and the resulting solver after applying the two patches will closely, but not precisely, simulate Glucose 2.3 (hence 3.0 and 4.0). Therefore, it cannot be used to continue to apply the rest of the main patches. Use them for research purposes only.

Patch FileDescription
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.

Papers

[1] Chanseok Oh. Improving SAT Solvers by Exploiting Empirical Characteristics of CDCL, PhD thesis, New York University

[2] Chanseok Oh. Patching MiniSat to Deliver Performance of Modern SAT Solvers, SAT-Race'15

[3] Chanseok Oh. Between SAT and UNSAT: The Fundamental Difference in CDCL SAT, SAT'15

[4] James Ezick, Jonathan Springer, Tom Henretty, and Chanseok Oh. Extreme SAT-based Constraint Solving with R-Solve, HPEC'14

[5] Chanseok Oh. COMiniSatPS: A SAT Solver with New Insights, unpublished manuscript

--
오찬석