Exploiting Glue Clauses to Design Effective CDCL Branching Heuristics
In conflict-directed clause learning (CDCL) SAT solving, a state-of-the-art criterion to measure the importance of a learned clause is called literal block distance (LBD), which is the number of distinct decision levels in the clause. The lower the LBD score of a learned clause, the better is its quality. The learned clauses with LBD score of 2, called glue clauses, are known to possess high pruning power. In this work, we relate glue clauses to decision variables. First, we show experimentally that branching decisions with variables appearing in glue clauses, called glue variables, are more conflict efficient than with nonglue variables. This observation motivated the development of a structure-aware CDCL variable bumping scheme, which increases the heuristic score of a glue variable based on its appearance count in the glue clauses that are learned so far by the search. Empirical evaluation shows the effectiveness of the new method on the main track instances from SAT Competitions 2017 and 2018 with four state-of-the-art CDCL SAT solvers. Finally, we show that the frequency of learned clauses that are glue clauses can be used as a reliable indicator of solving efficiency for some instances, for which the standard performance metrics fail to provide a consistent explanation.Citation
M. Chowdhury, M. Müller, J. You. "Exploiting Glue Clauses to Design Effective CDCL Branching Heuristics". International Conference on Principles and Practice of Constraint Programming (CP), Stamford, USA, (ed: Schiex T., de Givry S.), pp 126-143, September 2019.Keywords: | |
Category: | In Conference |
Web Links: | Springer |
BibTeX
@incollection{Chowdhury+al:CP19, author = {Md Solimul Chowdhury and Martin Müller and Jia-Huai You}, title = {Exploiting Glue Clauses to Design Effective CDCL Branching Heuristics}, Editor = {Schiex T., de Givry S.}, Pages = {126-143}, booktitle = {International Conference on Principles and Practice of Constraint Programming (CP)}, year = 2019, }Last Updated: June 29, 2020
Submitted by Sabina P