tumblr page counter

Cryptominisat 3

Replacing wordy authority with visible certainty

This webpage shows the partial solving of two SAT instances, visually. I was amazed by Edward Tufte's work (hence the subtitle) and this came out of it. Tufte would probably not approve, as some of the layout is terrible. However, it might allow you to understand SAT better, and may offer inspiration... or, rather, vision. Enjoy.

Search restart statistics

Below you will find conflicts in the X axis and several interesting data on the Y axis. There are two columns, the left column is solving mizh-md5-47-3.cnf (a crypto problem), the right column is solving UTI-20-10-p0.cnf (a diagnosis problem) - both were aborted at 60'000 conflicts. Every datapoint corresponds to a restart. You may zoom in by clicking on an interesting point and dragging the cursor along the X axis. Double-click to unzoom. You can rearrange the order and layout by dragging the labels on the right. Blue vertical lines indicate the positions of simplification sessions. Between the blue lines are search sessions. The angle of the "time" graph indicates conflicts/second. Simplification sessions are not detailed. However, time jumps during simplifcaition, and the solver behaviour changes afterwards. The angle of the "restart no." graph indicates how often restarts were made. You can find a full list of terms below.

no support for canvas
(0) Newly learnt clause size distribution. Bottom: unitary clause. Top: largest clause. Black: Many learnt. White: None learnt. Horizontal resolution: 1000 conflicts. Vertical resolution: 1 literal
no support for canvas
(1) Newly learnt clause size distribution. Bottom: unitary clause. Top: largest clause. Black: Many learnt. White: None learnt. Horizontal resolution: 1000 conflicts. Vertical resolution: 1 literal

Terms used

red.reducible, also called learnt
irred.irreducible, also called non-learnt
conflconflict reached by the solver
learntclause learnt during 1UIP conflict analysis
trail depthdepth of serach i.e. the number of variables set when the solver reached a conflict
brach depththe number of branches made before conflict was encountered
trail depth deltathe number of variables we jumped back when doing conflict-directed backjumping
branch depth deltathe number of branches jumped back during conflict-directed backjumping
propagations/decisionnumber of variables set due to the propagation of a decision (note that there is always at least one, the variable itself)
vars replacedthe number or variables replaced due to equivalent literal simplfication
polarity flippedpolarities of variables are saved and then used if branching is needed, but if propagation takes place, they are sometimes flipped
std devstandard deviation, the square root of variance
confl bythe clause that caused the conflict
agilitySee here.
gluethe number of different decision levels of the literals found in newly learnt clauses. See here
conflict after conflict %How often does it happen that a conflict, after backtracking and propagating immeediately (i.e. without branching) leads to a conflict. This is displayed because it's extremely high percentage relative to what most would expect. Thanks to Said Jabbour for this.

Why did I do this?

There has been some past work on statically visualizing SAT problems by Carsten Sinz, but not much on dynamic solving visualization - in fact, nothing comes to my mind that is comparable to what is above. However, the point of this excercise was not only to visually display dynamic solver behaviour. Rather, I think we could do dynamic analysis and heuristic adjustment instead of the static analysis and static heuristic selection as done by current portifolio solvers. Accordingly, CryptoMiniSat 3 has an extremely large set of options - e.g. swithcing between cleaning using glues, activities, clause sizes, or number of propagations+conflicts made by a clause is only a matter of setting a variable, and can be done on-the-fly. Problems tend to evolve as simplication and solving steps are made, so search heuristics should evolve with the problem.

Future work

Data displayed above is nothing but a very small percentage of data that is gathered during solving. In particular, no data at all is shown about simplifcations. Also, note that the data above displays only ~40/400 seconds of solving time on a very slow machine. Time-out for SAT competition, considering computing speed, is on the order of 20x more. Futhermore, there are probably better ways to present the data that is displayed. Future work should try to fix these shortcomings. You can either send me a mail if you have an idea, or implement it yourself - all is up in the GIT, including SQL, PHP, HTML, CSS and more.

The End

If you enjoyed this visualization, there are two things you can do. First, tell me about your impressions here and send the link to a friend. Second, you can contact my employer, and he will be happy to find a way for us to help you with your SAT problems.


I would like to thank my employer for letting me play with SAT, my collegue Luca Melette for helping me with ideas and coding, Vegard Nossum for the many discussions we had about visualization, George Katsirelos for improvement ideas, Said Jabbour for further improvement ideas, Dygraphs for the visually pleasing graphs, Portal for the drag-and-drop feature and Edward Tufte for all his wonderful books.

Copyright Mate Soos, 2012. Licensed under CC BY-NC-SA 2.5