Understanding Literal Block Distance in SAT solvers

Abstract

Donem un nou punt de vista sobre les heurístiques basades en la Literal Block Distance (LBD) i el glue, actualment utilitzades en SAT solvers. Per fer això, primer hem introduït el concepte de stickiness: donada una execució d'un SAT solver CDCL, per a cada parell de literals definim, amb un valor real entre 0 i 1, que enganxosos són entre si, bàsicament, amb quina freqüència trobem aquest parell en el mateix nivell de decisió. Mitjançant un detallat disseny d'experiments i una anàlisi posterior, confirmem un fet sorprenent: donat un problema SAT, quan executem diferents SAT solvers CDCL, no importa les seves configuracions, la relació d'stickiness entre literals sempre és bastant similar, en un sentit definit precisament. Després d'això hem analitzat com de ràpid s'estabilitza l'stickiness en una execució, i també, com aquestes mesures són estables fins i tot sota diferents codificacions de restriccions cardinals. A continuació descrivim com poden aquestes noves mesures portar cap a un refinament de les heurístiques de SAT (i altres extensions, com SMT) i millorar la informació compartida dels solvers paral·lels.

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 then analyze how quickly stickiness stabilizes in a run, 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.