Tag Archives: SAT Race

Final polish of my SAT competition entry

[wpdm_file id=2] UPDATE: Fixed crash, UPDATE2: fixed looking for Gaussian elimination library

In the last days of the competition deadline, I have improved the following on the SAT solver:

  • Adding N new variables is now possible in one go. This reduces variable addition overhead, especially when having many threads.
  • Memory allocation overhead per new clause addition is now much smaller thanks to judicious use of globally allocated temporaries. Using such temporaries is very dangerous as CryptoMiniSat uses addClause() from multiple places in the code in a recursive manner. However, I only use the temporaries for add_clause_outer(), so things should be fine.
  • If more than 0.5M variables or 1.5M binary clauses are in the problem, on-the-fly hyper-binary resolution and transitive reduction is turned off during 1st-decision-level search. This is kind of like probing, but during search. However, unlike probing, it cannot time-out and switch off these systems in case they takes too much time.
  • Diversified the threads’ parameters. Also, I reduced the number of threads to 8. I wanted to run with 12, but it’s a bit dangerous from a memory-usage perspective: there is only 24GB available for 12 cores, which means 2GB/core. Some problems take more than 2GB just to parse into the watchlists.
  • Check total memory usage at startup of threads and if too much, halve the total number of threads. This is an emergency measure in case things go wild due to very weird CNF.

Overall these are small changes but allow for a much faster startup. For example a notorious problem, AProVE07-11.cnf, now starts in 2.5s instead of 4.5s. As far as I can tell, this is very similar to the startup time of lingeling on this instance. However, lingeling only uses 1/3rd the memory (~250MB) thanks to a more tight memory manager plus I suspect it doesn’t have a couple of datastructs that I keep around.

The other difference, about OTF hyper-binary resolution, allows for large problems to actually get to the point of solving instead of getting stuck at adding and removing useless binary clauses. Let’s hope all goes well for the competition :)

My SAT Competition 2014 entry

[wpdm_file id=2]

In case you want to download my SAT competition 2014 zipfile, you can do it now. You can port the changes that you added to CryptoMiniSatv4 — it should work out of the box. Nothing really important changed except some timeout fixes, bug fixes, threading, and fixing DRAT.

Unfortunately the SAT Competition’14 setup doesn’t have Boost’s program options, so I had to create a main_simple.cpp that compiles without Boost. It only supports options “–drat=1”, “–threads=N”, “–verbosity=N” and reading plain CNF files (not gzipped). This means you will have to edit SolverConf.cpp in case your changeset involves command line options. The command line options and their corresponding class variables are easy to look up in main.cpp, so changing SolverConf.cpp appropriately should not be difficult.

Good luck with the competition!

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.

15 minutes of SAT Comp’09, 11, and 13

I’m finally moving over to looking at visual logs rather than console logs. They actually take up less space since the solution to some problems is in the MB range due the number of variables. They also take almost no time at all to dump, I couldn’t observe any significant difference in solving times with SQL dumping turned on or off. So, I ran a full set of SAT Competition 09,11 and 13 instances on current CryptoMiniSat git (dc657…). Below are the results for a 15min timeout on an i7-4770. I get these graphs as on-the-fly updated AJAX pull (i.e. I can see the solving as it’s progressing), but I didn’t want to make my puny little VM die, so these are pulled form pre-generated static files. Just select a file and it loads automatically. The version cannot be changed, I only uploaded the data for this version of CryptoMiniSat. I might upload a couple of different ones later.

Gray bars show min&max values. Vertical blue lines are the inprocessing points. You can zoom in by clicking and horizontally dragging. Double-click to unzoom. Enjoy!

Notes: If the problem decomposed into smaller sub-problems, the SAT solver run of the decomposed part is not shown. This is particularly annoying for aloul-chnl11-13. Total data size in MySQL table is about 400MB.

CryptoMiniSat 3.2.0 released

CyptoMinSat 3.2.0 has been released. This code should be extremely stable and should contain no bugs. In case it does, CryptoMiniSat will fail quite bady at the competition. I have fuzzed the solver for about 2-3000 CPU hours, with some sophisticated fuzzers (all available here — most of them not mine) so all should be fine, but fingers are crossed.

Additions and fixes

The main addition this time is certification proofs for UNSAT through the use of DRUP. This allows for use of the solver where certainty of the UNSAT result is a necessity — e.g. where lives could potentially depend on it. Unfortunately, proof checking is relatively slow through any system, though DRUP seems to be the best and fastest method. Other than the implementation of DRUP, I have fixed some issues with variable replacement.

SAT Competition’13

The description of the solver sent in to the SAT Competition’13 is available from the subfolder “desc” of the tarball. The code of 3.2.0 is actually the same that will run during the competition, the only changes made were:

  • the DRUP output had to be put into the standard output
  • the line “o proof DRUP” had to be printed
  • certified UNSAT binary uses the “–unsat 1” option by default
  • compilation was changed to use the m4ri library that was included with the tarball
  • linking is static so m4ri and other requirements don’t cause trouble
  • boost minimum version had to be lowered

You can download my submissions to the competition, forl, from here and here.