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.
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.
|
|
(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 |
(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 |
| Abbreviation | Explanation |
|---|---|
| red. | reducible, also called learnt |
| irred. | irreducible, also called non-learnt |
| confl | conflict reached by the solver |
| learnt | clause learnt during 1UIP conflict analysis |
| trail depth | depth of serach i.e. the number of variables set when the solver reached a conflict |
| brach depth | the number of branches made before conflict was encountered |
| trail depth delta | the number of variables we jumped back when doing conflict-directed backjumping |
| branch depth delta | the number of branches jumped back during conflict-directed backjumping |
| propagations/decision | number of variables set due to the propagation of a decision (note that there is always at least one, the variable itself) |
| vars replaced | the number or variables replaced due to equivalent literal simplfication |
| polarity flipped | polarities of variables are saved and then used if branching is needed, but if propagation takes place, they are sometimes flipped |
| std dev | standard deviation, the square root of variance |
| confl by | the clause that caused the conflict |
| agility | See here. |
| glue | the 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. |
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.
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.
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