Risc Colloquium

We study the structure of "industrial" SAT formulas representing them as graphs, either as a bi-partite graphs where a variable node and a clause node are connected if the variable occurs in the clause, or as a graph where two variable nodes are connected if they occur together in a clause. We explore the instances used in the SAT competitions. This analysis can help to understand some heuristics and methods use in modern SAT solvers. The final objective is to improve their performance on "real" instances, and to get a better random model of them.

We show that most of the formulas have a scale-free structure, where variable-nodes degree (number of occurrences of variables) follow a power-law distribution, in almost all cases, and clause-nodes degree (size of clauses) too, in most of the cases.  We propose a method to randomly generating scale-free SAT formulas, and check how good are SAT solvers on them.

We analyze also the community structure of industrial SAT formulas. We see that most of them are highly modular (maybe as a consequence of scale-free structure).

Finally, we explore self-similarity of these graphs and compute their fractal dimension. We see that in most of the cases, graphs have a fractal dimension between 2 and 3. This implies that the diameter of graphs grow polynomially, and not logarithmically. This would also mean that industrial SAT solvers could be using some mechanism to focus their search in an area of the formula.