The Fractal Dimension of SAT Formulas
MetadataShow full item record
Modern SAT solvers have experienced a remarkable progress on solving industrial instances. Most of the techniques have been developed after an intensive experimental process. It is believed that these techniques exploit the underlying structure of industrial instances. However, 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 complementing 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.
Is part ofLecture Notes in Computer Science, 2014, vol. 8562, p. 107-121
European research projects
Showing items related by title, author, creator and subject.
Ansótegui Gil, Carlos José; Bonet, Maria Luisa; Levy, Jordi (Elsevier, 2013)Many industrial optimization problems can be translated to MaxSAT. Although the general problem is NP hard, like SAT, many practical problems may be solved using modern MaxSAT solvers. In this paper we present several ...
Ansótegui Gil, Carlos José; Béjar Torres, Ramón; Fernàndez Camon, César; Mateu Piñol, Carles (Association for the Advancement of Artificial Intelligence, 2008)In this paper we provide a new method to generate hard k-SAT instances. We incrementally construct a high girth bipartite incidence graph of the k-SAT instance. Having high girth assures high expansion for the graph, and ...
Ansótegui Gil, Carlos José; Béjar Torres, Ramón; Fernàndez Camon, César; Mateu Piñol, Carles (Springer Verlag, 2008)In this paper we provide a new method to generate hard k-SAT instances. Basically, we construct the bipartite incidence graph of a k-SAT instance where the left side represents the clauses and the right side represents ...