Tag Archives: Release

ApproxMCv3, a modern approximate model counter

This blogpost and its underlying work has been brewing for many years, and I’m extremely happy to be able to share it with you now. Kuldeep Meel and myself have been working very hard on speeding up approximate model counting for SAT and I think we have made real progress. The research paper, accepted at AAAI-19 is available here. The code is available here (release with static binary here). The main result is that we can solve a lot more problems than before. The speed of solving is orders(!) of magnitude faster than the previous best system:

Background

The idea of approximate model counting, originally by Chakraborty, Meel and Vardi was a huge hit back in 2013, and many papers have followed it, trying to improve its results. All of them were basically tied to CryptoMiniSat, the SAT solver that I maintain, as all of them relied on XOR constraints being added to the regular CNF of a typical SAT problem.

So it made sense to examine what CryptoMiniSat could do to improve the speed of approximate counting. This time interestingly coincided with me giving up on XORs in CryptoMiniSat. The problem was the following. A lot of new in- and preprocessing systems were being invented, mostly by Armin Biere et al, and I quickly realised that I simply couldn’t keep adding them, because they didn’t take into account XOR constraints. They handled CNF just fine, but not XORs. So XORs became a burden, and I removed them in versions 3 and 4 of CryptoMiniSat. But there was need, and Kuldeep made it very clear to me that this is an exciting area. So, they had to come back.

Blast-Inprocess-Recover-Destroy

But how to both have and not have XOR constraints? Re-inventing all the algorithms for XORs was not a viable option. The solution I came up with was a rather trivial one: forget the XORs during inprocessing and recover them after. The CNF would always remain the source of truth. Extracting all the XORs after in- and preprocessing would allow me to run the Gauss-Jordan elimination on the XORs post-recovery. So I can have the cake and eat it too.

The process is conceptually quite easy:

  1. Blast all XORs into clauses that are in the input using intermediate variables. I had all the setup for this, as I was doing Bounded Variable Addition  (also by Biere et al.) so I didn’t have to write code to “hide” these additional variables.
  2. Perform pre- or inprocessing. I actually only do inprocessing nowadays (as it has faster startup time). But preprocessing is just inprocessing at the start ;)
  3. Recover the XORs from the CNF. There were some trivial methods around. They didn’t work as well as one would have hoped, but more on that later
  4. Run the CDCL and Gauss-Jordan code at the same time.
  5. Destroy the XORs and goto 2.

This system allows for everything to be in CNF form, lifting the XORs out when necessary and then forgetting them when it’s convenient. All of these steps are rather trivial, except, as I later found out, recovery.

XOR recovery

Recovering XORs sounds like a trivial task. Let’s say we have the following clauses

This is conceptually equivalent to the XOR v1+v2+v3=1. So recovering this is trivial, and has been done before, by Heule in particular, in his PhD thesis. The issue with the above is the following: a stronger system than the above still implies the XOR, but doesn’t look the same. Let me give an example:

This is almost equivalent to the previous set of clauses, but misses a literal from one of the clauses. It still implies the XOR of course. Now what? And what to do when missing literals mean that an entire clause can be missing? The algorithm to recover XORs in such cases is non-trivial. It’s non-trivial not only because of the complexity of how many combinations of missing literals and clauses there can be (it’s exponential) but because one must do this work extremely fast because SAT solvers are sensitive to time.

The algorithm that is in the paper explains all the bit-fiddling and cache-friendly data layout used along with some fun algorithms that I’m sure some people will like. We even managed to use compiler intrinsics to use target-specific assembly instructions for hamming weight calculation. It’s a blast. Take a look.

The results

The results, as shown above, speak for themselves. Problems that took thousands of seconds to solve can now be solved under 20. The reason for such incredible speedup is basically the following. CryptoMiniSatv2 was way too clunky and didn’t have all the fun stuff that CryptoMiniSatv5 has, plus the XOR handling was incorrect, loosing XORs and the like. The published algorithm solves the underlying issue and allows CNF pre- and inprocessing to happen independent of XORs, thus enabling CryptoMiniSatv5 to be used in all its glory. And CryptoMiniSatv5 is fast, as per the this year’s SAT Competition results.

Some closing words

Finally, I want to say thank you to Kuldeep Meel who got me into the National University of Singapore to do the work above and lots of other cool work, that we will hopefully publish soon. I would also like to thank the National Supercomputing Center Singapore  that allowed us to run a ton of benchmarks on their machines, using at least 200 thousand CPU hours to make this paper. This gave us the chance to debug all the weird edge-cases and get this system up to speed where it beats the best exact counters by a wide margin. Finally, thanks to all the great people I had the chance to meet and sometimes work with at NUS, it was a really nice time.

 

CryptoMiniSat 5.6.3 Released

The latest CryptoMiniSat, version 5.6.3 has been released. This release marks the 12’000th commit to this solver that has weathered more than I originally intended it to weather. It’s been an interesting ride, and I have a lot to thank Kuldeep and NSCC‘s ASPIRE-1 cluster for this release. I have burned over 200k CPU hours to make this release, so it’s a pretty well-performing release (out-performing anything out there, by a wide margin), though I’m working very hard to make sure that neither I nor anyone else will have to burn anything close to that to make a well-performing SAT solver.

The solver has some interesting new algorithms inside, the most interesting of which is Gauss-Jordan elimination using a Simplex-like method, generously contributed by Jie-Hong Roland Jiang and Cheng-Shen Han from the National Taiwan University. This addition should finally settle the issues regarding Gaussian vs Gauss-Jordan elimination in SAT solvers. Note that to use this novel system, you must configure with “cmake -DUSE_GAUSS=ON ..” and then re-compile.

What’s also interesting is what’s not inside, though. I have been reading (maybe too much) Nassim Taleb and he is very much into via negativa. So I tried removing algorithms that have been in the solver for a while and mostly nobody would question if they are useful. In the end I removed the following algorithms from running by default, each removal leading to better solving time:

  • Regular probing. Intree probing is significantly better, so regular probing is not needed. Thanks Matti/Marijn/Armin!
  • Stamping. This was a big surprise, especially because I also had to remove caching, which is my own, crappy (“different”) version of stamping. I knew that it wasn’t always so good to have, but damn. It was a hard call, but if it’s just slowing it down, what can I do. It’s weird.
  • Burst searching. This is when I search for a short period with high randomness all over the search space. I thought it would allow me to explore the search space in places where VSIDS/Maple doesn’t. Why this is slowing the solver down so much may say more about search heuristics/variable bumping/clause bumping than anything.
  • Note that I never had blocked clause elimination. It doesn’t work well for incremental solving. In fact, it doesn’t work at all, though apparently the authors have some new work that allows it to work, super-interesting!

I’m nowadays committed to understanding this damned thing rather than adding another impossible-to-explain magic constant  to make the solving 10% faster. I think there is interesting stuff out there that could be done to make SAT solvers 10x, not 10%, faster.

CryptoMiniSat 4.2 released

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:

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]

CryptoMiniSat 4 released

[wpdm_file id=1]
CryptoMiniSat 4 is now available for download. This version brings a number of substantial improvements and picks up speed to be as good as the best solvers out there. It now has a much improved library interface as well as a simple but powerful python interface.

SAT Competition 2014

This release is made ahead of the SAT competition 2014 deadlines so anybody can compete and actually have a chance to win. Unfortunately, the way I see it, it’s not possible to use newer versions of lingeling or riss (see license for for details), MiniSat is rather old and glucose doesn’t have new simplification techniques. If you feel the same way, and you rather not write 30K LoC of code, you might enjoy playing with CryptoMiniSat v4 and submitting it to the competition. You can change as much as you like, it’s LGPLv2 — just don’t call it CryptoMiniSat.

Improvements and techniques

Here is a non-exhaustive list of techniques used in CryptoMiniSat v4:

  • Variable elimination and replacement, strengthening, subsumption, vivification
  • On-the-fly stamping, literal caching, hyper-binary resolution and transitive reduction during failed literal probing
  • Bounded variable addition with hack to allow 2-literal diff
  • DRUP-based unsatisfiable proof logging
  • Gate-based clause shortening and removal
  • XOR recovery and manipulation (NOTE: uses the M4RI library that is GPL, if you want LGPL, compile without it)
  • Precise time- and memory tracking. No time or memory-outs on weird CNFs
  • Precise usefulness tracking of all clauses
  • Clause usefulness-based redundant clause removal. Glues are not used by default, but glues are tracked and can be used (command line option)
  • Variable renumbering and variable number hiding. Thanks to this, XOR clauses are cut and the added variables are transparent to the user.
  • SQL-based data logging and AJAX-based powerful data display
  • And of course many-many more

All of the above are implemented as inprocessing techniques. I do not believe in preprocessing and the solver does not in fact use preprocessing at all — it immediately starts to solve instead. This, as everything else, is configurable and you can change it by passing '--presimp 1' as a command-line option. There are a total of 120 command-line options so you can tune the solver as you like.

Python interface

It’s intuitive and fun to use:

You can even have assumptions:

All the power of the SAT solver in a very accessible manner. XOR clauses are trivial, too:

Where the second argument is the right hand side (RHS) of the equation v1 XOR v2 = False.

C++ interface

Usage is pretty simple, and the header files have been significantly cleaned up:

Some suggestions where you can improve the solver to compete

Here is a non-exhaustive list of things that you can improve to win at the competition:

  • Add your own weird idea. You can add new variables if you like, use the occurrence lists already built, and take advantage of all the datastructures (such as stamps, literal cache) already present.
  • Tune the parameters. I only have exactly one i7-4770 to tune the parameters. You might have more. All parameters are accessible from command line, so tuning should be trivial.
  • Use glues to clean clauses. Or use a combination of glues and usefulness metrics. All the metrics are at your fingertips.
  • Make bounded variable addition work for learnt clauses. I could never figure this one out.
  • Improve the ordering of variable elimination. Makes a huge difference.
  • Try a different approach: I use the ‘heavy’ approach where I don’t remove all clauses that I can as I like strong propagation properties. You might try the ‘light’ approach where everything is removed if possible. Just set variable elimination to 100% and add blocked clause elimination. It might work.

For example, below is the code that calculates which clause should be cleaned or kept. You can clearly see how easily this can be changed using the data elements below:

If you were thinking about submitting your weird hack to the MiniSat hacktrack, think about doing the same to CrytoMiniSat v4. You might actually win the real competition. You can change as much as you like.

I will submit a description of CryptoMiniSat v4, your description can simply say that it’s the same except for xyz that you changed. The point of the descriptions is so that people can read what you did and why and then comprehend the results in that light. Just explain carefully what you did and why, and you should be fine.

Thanks

Many-many thanks to Martin Maurer who has submitted over 100 bug reports through the GitHub issue system. Kudos to all who have helped me use, debug and improve the solver. To name just a few: Vegard Nossum, Martin Albrecht, Karsten Nohl, Luca Melette, Vijay Ganesh and Robert Aston.