English   español  
Please use this identifier to cite or link to this item: http://hdl.handle.net/10261/158291
logo share SHARE   Add this article to your Mendeley library MendeleyBASE
Visualizar otros formatos: MARC | Dublin Core | RDF | ORE | MODS | METS | DIDL
Exportar a otros formatos:


A Modularity-Based Random SAT Instances Generator

AuthorsGiraldez-Cru, Jesus; Levy, Jordi
KeywordsModel checking
SAT solvers
SAT instances
SAT solving
Issue Date25-Jul-2015
PublisherAAAI Press
CitationIJCAI'15 Proceedings of the 24th International Conference on Artificial Intelligence:1952-1958
AbstractNowadays, many industrial SAT instances can be solved efficiently by modern SAT solvers. However, the number of real-world instances is finite. Therefore, the process of development and test of SAT solving techniques can benefit of new models of random formulas that capture more realistically the features of real-world problems. In many works, the structure of industrial instances has been analyzed representing them as graphs and studying some of their properties, like modularity. In this paper, we use modularity, or community structure, to define a new model of pseudo-industrial random SAT instances, called Community Attachment. We prove that the phase transition point, if exists, is independent on the modularity. We evaluate the adequacy of this model to real industrial problems in terms of SAT solvers performance, and show that modern solvers do actually exploit this community structure.
Identifiersisbn: 978-157735738-4
uri: https://www.ijcai.org/Proceedings/15/Papers/277.pdf
Appears in Collections:(IIIA) Comunicaciones congresos
Files in This Item:
File Description SizeFormat 
IJCAI_15_1952-58.pdf547,65 kBUnknownView/Open
Show full item record
Review this work

WARNING: Items in Digital.CSIC are protected by copyright, with all rights reserved, unless otherwise indicated.