The Fractal Dimension of SAT Formulas
Marı́a Luisa Bonet, Jordi Levy · 2014
Abstract. Modern SAT solvers have experienced a remarkable progress on solving industrial instances. Most of the techniques have been devel-oped after an intensive experimental process. It is believed that these techniques exploit the underlying structure of industrial instances. How-ever, there is not a precise definition of the notion of structure. Recently, there have been some attempts to analyze this structure in terms of complex networks, with the long-term aim of explaining the success of SAT solving techniques, and possibly improving them. We study the fractal dimension of SAT instances with the aim of comple-menting the model that describes the structure of industrial instances. We show that many industrial families of formulas are self-similar, with a small fractal dimension. We also show how this dimension is affected by the addition of learnt clauses during the execution of SAT solvers. 1