Community structure in industrial SAT instances
Visualitza/Obre
Cita com:
hdl:2117/175104
Tipus de documentArticle
Data publicació2019-10-10
Condicions d'accésAccés obert
Tots els drets reservats. Aquesta obra està protegida pels drets de propietat intel·lectual i
industrial corresponents. Sense perjudici de les exempcions legals existents, queda prohibida la seva
reproducció, distribució, comunicació pública o transformació sense l'autorització del titular dels drets
Projecte
Abstract
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.
CitacióAnsótegui, C. [et al.]. Community structure in industrial SAT instances. "Journal of artificial intelligence research", 10 Octubre 2019, vol. 66, p. 443-472.
ISSN1076-9757
Versió de l'editorhttps://jair.org/index.php/jair/article/view/11741
Col·leccions
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
11741-Article (PDF)-22244-1-10-20191010.pdf | 1,404Mb | Visualitza/Obre |