"The Nature of Industrial SAT Instances"
Jordi Levy
The Artificial Intelligence Research Institute (IIIA)
Monday, July 29, 2013, 2:00 pm
EBU3B, Room 4217
Abstract:
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 annual SAT race
competition. 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 scalefree structure, where
variable-nodes degree (number of occurrences of variables) follow a
powerlaw 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 scalefree 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
scalefree 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.
Joint work with Carlos Ansotegui, Maria Luisa Bonet and Jesus Giraldez.