Some SAT Benchmarks Visualised as Graphs

The following sections highlight the differences in graph representations of some SAT problems. It also provides insight into the usefulness of visualising a problem or problem domains. Note that while only one problem is shown from a particular set, we noticed the same kinds of structures and appearances from each domain or set of problems. We generated graphs for many groups of benchmark problems, and the following examples are some of the most informative. Some visualisations of benchmark problem domains did not appear to be informative using these techniques.

The benchmark problems described below are taken from the DIMACS benchmark suite and the Beijing benchmark suite. Both of these collections are available from satlib: http://www.satlib.org.