Characterization of Glue Variables in CDCL SAT Solving
arXiv: Artificial Intelligence, 2019.
A state-of-the-art criterion to evaluate the importance of a given learned clause is called Literal Block Distance (LBD) score. It measures the number of distinct decision levels in a given learned 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, ...More
PPT (Upload PPT)