English   español  
Please use this identifier to cite or link to this item: http://hdl.handle.net/10261/139428
Share/Impact:
Statistics
logo share SHARE logo core CORE   Add this article to your Mendeley library MendeleyBASE

Visualizar otros formatos: MARC | Dublin Core | RDF | ORE | MODS | METS | DIDL
Exportar a otros formatos:
Title

Generating SAT instances with community structure

AuthorsGiraldez-Cru, Jesus; Levy, Jordi
KeywordsSAT solver
SAT generator
Graph modularity
Satisfiability
Issue Date2016
PublisherElsevier
CitationArtificial Intelligence 238: 119- 134 (2016)
AbstractNowadays, modern SAT solvers are able to efficiently solve many industrial, or real-world, SAT instances. However, the process of development and testing of new SAT solving techniques is conditioned to the finite and reduced number of known industrial benchmarks. Therefore, new models of random SAT instances generation that capture realistically the features of real-world problems can be beneficial to the SAT community. 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 work, we use the notion of modularity to define a new model of generation of random SAT instances with community structure, called Community Attachment. For high values of modularity (i.e., clear community structure), we realistically model pseudo-industrial random SAT formulas. This model also generates SAT instances very similar to classical random formulas using a low value of modularity. We also prove that the phase transition point, if exists, is independent on the modularity. We evaluate the adequacy of this model to real industrial SAT problems in terms of SAT solvers performance, and show that modern solvers do actually exploit this community structure. Finally, we use this generator to observe the connections between the modularity of the instance and some components of the solver, such as the variable branching heuristics or the clause learning mechanism.
URIhttp://hdl.handle.net/10261/139428
DOI10.1016/j.artint.2016.06.001
Identifiersdoi: 10.1016/j.artint.2016.06.001
issn: 0004-3702
Appears in Collections:(IIIA) Artículos
Files in This Item:
File Description SizeFormat 
accesoRestringido.pdf15,38 kBAdobe PDFThumbnail
View/Open
Show full item record
Review this work
 

Related articles:


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