Para acceder a los documentos con el texto completo, por favor, siga el siguiente enlace: http://hdl.handle.net/2117/175104

Título:	Community structure in industrial SAT instances
Autor/a:	Ansótegui Gil, Carlos; Bonet Carbonell, M. Luisa; Giráldez Crú, Jesús; Levy Díaz, Jordi; Simon, Laurent
Otros autores:	Universitat Politècnica de Catalunya. Departament de Ciències de la Computació
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.
Abstract:	Peer Reviewed
Materia(s):	-Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica -Graph theory -Benchmarking -Complex networks -Decision theory -Model checking -Grafs, Teoria de
Derechos:
Tipo de documento:	Artículo - Versión publicada Artículo
Compartir:

Mostrar el registro completo del ítem