During this decade, it has been observed that many real-world graphs, like the web and some social and metabolic networks,
have a
scale-free structure. These graphs are characterized by a big variability in the arity of nodes, that seems to follow a power-law distribution.
This came as a big surprise to researchers steeped in the tradition of classical random networks.
SAT instances can also be seen as (bi-partite) graphs. In this paper we study many families of industrial SAT instances used
in SAT competitions, and show that most of them also present this scale-free structure. On the contrary, random SAT instances,
viewed as graphs, are closer to the classical random graph model, where arity of nodes follows a Poisson distribution with
small variability. This would explain their distinct nature.
We also analyze what happens when we instantiate a fraction of the variables, at random or using some heuristics, and how
the scale-free structure is modified by these instantiations. Finally, we study how the structure is modified during the execution
of a SAT solver, concluding that the scale-free structure is preserved.
Research partially supported by the projects TIN2007-68005-C04-{01,03,04} and TIN2006-15662-C02-02 funded by the MEC.