摘要：Modern SAT solvers have experienced a remarkable progress on solving industrial instances.
It is believed that most of these successful techniques exploit the underlying
structure of industrial instances. Recently, there have been some attempts to analyze
the structure of industrial SAT instances in terms of complex networks, with the aim of
explaining the success of SAT solving techniques, and possibly improving them.
In this paper, we study the community structure, or modularity, of industrial SAT instances.
In a graph with clear community structure, or high modularity, we can find a
partition of its nodes into communities such that most edges connect variables of the same
community. Representing SAT instances as graphs, we show that most application benchmarks
are characterized by a high modularity. On the contrary, random SAT instances
are closer to the classical Erd¨os-R´enyi random graph model, where no structure can be
observed. We also analyze how this structure evolves by the effects of the execution of a
CDCL SAT solver, and observe that new clauses learned by the solver during the search
contribute to destroy the original structure of the formula. Motivated by this observation,
we finally present an application that exploits the community structure to detect relevant
learned clauses, and we show that detecting these clauses results in an improvement on the
performance of the SAT solver. Empirically, we observe that this improves the performance
of several SAT solvers on industrial SAT formulas, especially on satisfiable instances.
其他摘要：Modern SAT solvers have experienced a remarkable progress on solving industrial instances. It is believed that most of these successful techniques exploit the underlying structure of industrial instances. Recently, there have been some attempts to analyze the structure of industrial SAT instances in terms of complex networks, with the aim of explaining the success of SAT solving techniques, and possibly improving them. In this paper, we study the community structure, or modularity, of industrial SAT instances. In a graph with clear community structure, or high modularity, we can find a partition of its nodes into communities such that most edges connect variables of the same community. Representing SAT instances as graphs, we show that most application benchmarks are characterized by a high modularity. On the contrary, random SAT instances are closer to the classical Erdös-Rényi random graph model, where no structure can be observed. We also analyze how this structure evolves by the effects of the execution of a CDCL SAT solver, and observe that new clauses learned by the solver during the search contribute to destroy the original structure of the formula. Motivated by this observation, we finally present an application that exploits the community structure to detect relevant learned clauses, and we show that detecting these clauses results in an improvement on the performance of the SAT solver. Empirically, we observe that this improves the performance of several SAT solvers on industrial SAT formulas, especially on satisfiable instances.
