The fractal dimension of SAT formulas

DOI10.1007/978-3-319-08587-6_8MaRDI QIDQ3192184zbMATH OpenOpenAlexWikidataFDO

Authors Carlos Ansótegui, Maria Luisa Bonet, Jesús Giráldez-Cru, Jordi Levy

Publication date 26 September 2014

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1308.5046, http://hdl.handle.net/10459.1/65063

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Graph theory (including graph drawing) in computer science (68R10) Fractals (28A80)

Abstract: Modern SAT solvers have experienced a remarkable progress on solving industrial instances. Most of the techniques have been developed after an intensive experimental testing process. Recently, there have been some attempts to analyze the structure of these formulas in terms of complex networks, with the long-term aim of explaining the success of these SAT solving techniques, and possibly improving them. We study the fractal dimension of SAT formulas, and show that most industrial families of formulas are self-similar, with a small fractal dimension. We also show that this dimension is not affected by the addition of learnt clauses. We explore how the dimension of a formula, together with other graph properties can be used to characterize SAT instances. Finally, we give empirical evidence that these graph properties can be used in state-of-the-art portfolios.

Recommendations

• The community structure of SAT formulas
• Community structure in industrial SAT instances
• Generating SAT instances with community structure
• Popularity-similarity random SAT formulas
• Empirical study of the anatomy of modern SAT solvers

Cited in

(12)

• Fractal Parallelism: Solving SAT in Bounded Space and Time
• scientific article; zbMATH DE number 7561554 (Why is no real title available?)
• On the hierarchical community structure of practical Boolean formulas
• Solving non-uniform planted and filtered random SAT formulas greedily
• Evaluating CDCL variable scoring schemes
• Fractal structure on \(k\)-SAT
• Generating SAT instances with community structure
• Bounds on the satisfiability threshold for power law distributed random SAT
• New width parameters for SAT and \#SAT
• Popularity-similarity random SAT formulas
• Backdoor DNFs
• Community structure inspired algorithms for SAT and \#SAT

This page was built for publication: The fractal dimension of SAT formulas

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3192184)