Por favor, use este identificador para citar o enlazar a este item:
http://hdl.handle.net/10261/197391
COMPARTIR / EXPORTAR:
SHARE CORE BASE | |
Visualizar otros formatos: MARC | Dublin Core | RDF | ORE | MODS | METS | DIDL | DATACITE | |
Campo DC | Valor | Lengua/Idioma |
---|---|---|
dc.contributor.author | Xiao, Fan | es_ES |
dc.contributor.author | Li, Chu Min | es_ES |
dc.contributor.author | Luo, Mao | es_ES |
dc.contributor.author | Manyà, Felip | es_ES |
dc.contributor.author | Lu, Zhipeng | es_ES |
dc.contributor.author | Li, Yu | es_ES |
dc.date.accessioned | 2020-01-03T10:39:37Z | - |
dc.date.available | 2020-01-03T10:39:37Z | - |
dc.date.issued | 2019-07 | - |
dc.identifier.citation | Science China Information Sciences 62: 72103 (2019) | es_ES |
dc.identifier.issn | 1674-733X | - |
dc.identifier.uri | http://hdl.handle.net/10261/197391 | - |
dc.description.abstract | The 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. | es_ES |
dc.description.sponsorship | This work was partially supported by National Natural Science Foundation of China (Grant Nos. 61370183, 61370184, 61472147), Matrics Platform of the Université de Picardie Jules Verne, and MINECO-FEDER Project RASO (Grant No. TIN2015-71799-C2-1-P) | es_ES |
dc.language.iso | eng | es_ES |
dc.publisher | Springer Nature | es_ES |
dc.relation | info:eu-repo/grantAgreement/MINECO/Plan Estatal de Investigación Científica y Técnica y de Innovación 2013-2016/TIN2015-71799-C2-1-P | es_ES |
dc.rights | closedAccess | es_ES |
dc.subject | SAT | es_ES |
dc.subject | Branching heuristic | es_ES |
dc.subject | Conflict-driven clause learning | es_ES |
dc.subject | Implication graph | es_ES |
dc.title | A branching heuristic for SAT solvers based on complete implication graphs | es_ES |
dc.type | artículo | es_ES |
dc.identifier.doi | 10.1007/s11432-017-9467-7 | - |
dc.description.peerreviewed | Peer reviewed | es_ES |
dc.relation.publisherversion | http://dx.doi.org/10.1007/s11432-017-9467-7 | es_ES |
dc.identifier.e-issn | 1869-1919 | - |
dc.contributor.funder | National Natural Science Foundation of China | es_ES |
dc.contributor.funder | Université de Picardie Jules Verne (France) | es_ES |
dc.contributor.funder | Ministerio de Economía y Competitividad (España) | es_ES |
dc.contributor.funder | European Commission | es_ES |
dc.relation.csic | Sí | es_ES |
oprm.item.hasRevision | no ko 0 false | * |
dc.identifier.funder | http://dx.doi.org/10.13039/501100000780 | es_ES |
dc.identifier.funder | http://dx.doi.org/10.13039/501100003329 | es_ES |
dc.identifier.funder | http://dx.doi.org/10.13039/501100001809 | es_ES |
dc.type.coar | http://purl.org/coar/resource_type/c_6501 | es_ES |
item.openairecristype | http://purl.org/coar/resource_type/c_18cf | - |
item.fulltext | No Fulltext | - |
item.cerifentitytype | Publications | - |
item.openairetype | artículo | - |
item.languageiso639-1 | en | - |
item.grantfulltext | none | - |
Aparece en las colecciones: | (IIIA) Artículos |
Ficheros en este ítem:
Fichero | Descripción | Tamaño | Formato | |
---|---|---|---|---|
accesoRestringido.pdf | 15,35 kB | Adobe PDF | Visualizar/Abrir |
CORE Recommender
SCOPUSTM
Citations
7
checked on 12-abr-2024
WEB OF SCIENCETM
Citations
7
checked on 22-feb-2024
Page view(s)
184
checked on 19-abr-2024
Download(s)
16
checked on 19-abr-2024
Google ScholarTM
Check
Altmetric
Altmetric
NOTA: Los ítems de Digital.CSIC están protegidos por copyright, con todos los derechos reservados, a menos que se indique lo contrario.