The Fractal Dimension of SAT Formulas

TL;DR

This paper investigates the fractal dimension of SAT formulas, revealing that industrial instances are self-similar with low fractal dimension, which remains stable despite adding learnt clauses, and explores their use in SAT instance characterization.

Contribution

It introduces the analysis of fractal dimension in SAT formulas, linking structural properties to solver performance and portfolio selection.

Findings

Industrial SAT formulas are self-similar with low fractal dimension.

Adding learnt clauses does not significantly change the fractal dimension.

Graph properties, including fractal dimension, can improve SAT portfolio effectiveness.

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.