Decision levels are stable: towards better SAT heuristics
Visualitza/Obre
Main article (438,0Kb) (Accés restringit)
Sol·licita una còpia a l'autor
Què és aquest botó?
Aquest botó permet demanar una còpia d'un document restringit a l'autor. Es mostra quan:
- Disposem del correu electrònic de l'autor
- El document té una mida inferior a 20 Mb
- Es tracta d'un document d'accés restringit per decisió de l'autor o d'un document d'accés restringit per política de l'editorial
Cita com:
hdl:2117/349696
Tipus de documentText en actes de congrés
Data publicació2020
EditorEasyChair Publications
Condicions d'accésAccés restringit per política de l'editorial
Tots els drets reservats. Aquesta obra està protegida pels drets de propietat intel·lectual i
industrial corresponents. Sense perjudici de les exempcions legals existents, queda prohibida la seva
reproducció, distribució, comunicació pública o transformació sense l'autorització del titular dels drets
ProjecteSOLUCIONES EFECTIVAS BASADAS EN LA LOGICA (MINECO-TIN2015-69175-C4-3-R)
RAZONAMIENTO FORMAL PARA TECNOLOGIAS FACILITADORAS Y EMERGENTES (AEI-RTI2018-094403-B-C33)
RAZONAMIENTO FORMAL PARA TECNOLOGIAS FACILITADORAS Y EMERGENTES (AEI-RTI2018-094403-B-C33)
Abstract
We shed new light on the Literal Block Distance (LBD) and glue-based heuristics used in current SAT solvers. For this, we first introduce the concept of stickiness: given a run of a CDCL SAT solver, for each pair of literals we define, by a real value between 0 and 1, how sticky they are, basically, how frequently they are set at the same decision level.
By means of a careful and detailed experimental setup and analysis, we confirm the following quite surprising fact: given a SAT instance, when running different CDCL SAT solvers on it, no matter their settings or random seeds, the stickiness relation between literals is always very similar, in a precisely defined sense.
We analyze how quickly stickiness stabilizes in a run (quite quickly), and show that it is stable even under different encodings of cardinality constraints. We then describe how and why these solid new insights lead to heuristics refinements for SAT (and extensions, such as SMT) and improved information sharing in parallel solvers.
CitacióNieuwenhuis, R. [et al.]. Decision levels are stable: towards better SAT heuristics. A: International Conference on Logic for Programming, Artificial Intelligence and Reasoning. "LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (EPiC Series in Computing; 73)". EasyChair Publications, 2020, p. 1-11. ISBN 2398-7340. DOI 10.29007/cz1f.
ISBN2398-7340
Versió de l'editorhttps://easychair.org/publications/paper/Bz5Z
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
Decision_levels ... _better_SAT_heuristics.pdf | Main article | 438,0Kb | Accés restringit |