Publication Type: Conference Paper
Source: Proc. of the 15th Int. Conf. on Principles and Practice of Constraint Programming, CP'09, Springer, Volume 5732, Lisbon, Portugal, p.127-141 (2009)
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.