Not Logged In

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

University of Alberta Logo AICML Logo