English   español  
Please use this identifier to cite or link to this item: http://hdl.handle.net/10261/197391
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 | DATACITE
Exportar a otros formatos:


A branching heuristic for SAT solvers based on complete implication graphs

AuthorsXiao, Fan; Li, Chu Min ; Luo, Mao; Manyà, Felip CSIC ORCID ; Lu, Zhipeng; Li, Yu
Branching heuristic
Conflict-driven clause learning
Implication graph
Issue DateJul-2019
PublisherSpringer Nature
CitationScience China Information Sciences 62: 72103 (2019)
AbstractThe performance of modern conflict-driven clause learning (CDCL) SAT solvers strongly depends on branching heuristics. State-of-the-art branching heuristics, such as variable state independent decaying sum (VSIDS) and learning rate branching (LRB), are computed and maintained by aggregating the occurrences of the variables in conflicts. However, these heuristics are not sufficiently accurate at the beginning of the search because they are based on very few conflicts. We propose the distance branching heuristic, which, given a conflict, constructs a complete implication graph and increments the score of a variable considering the longest distance between the variable and the conflict rather than the simple presence of the variable in the graph. We implemented the proposed distance branching heuristic in Maple_LCM and Glucose-3.0, two of the best CDCL SAT solvers, and used the resulting solvers to solve instances from the application and crafted tracks of the 2014 and 2016 SAT competitions and the main track of the 2017 SAT competition. The empirical results demonstrate that using the proposed distance branching heuristic in the initialization phase of Maple_LCM and Glucose-3.0 solvers improves performance. The Maple_LCM solver with the proposed distance branching heuristic in the initialization phase won the main track of the 2017 SAT competition.
Publisher version (URL)http://dx.doi.org/10.1007/s11432-017-9467-7
Appears in Collections:(IIIA) Artículos
Files in This Item:
File Description SizeFormat 
accesoRestringido.pdf15,35 kBAdobe PDFThumbnail
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.