Too much information: why CDCL solvers need to forget learned clauses

TL;DR

This paper investigates how clause forgetting impacts CDCL SAT solvers, revealing that excessive clause retention can impair performance, and shows that solver runtimes follow multimodal Weibull mixture distributions, explaining the benefits of clause deletion.

Contribution

It provides the first empirical analysis linking clause forgetting to solver performance deterioration and models runtime distributions with Weibull mixtures.

Findings

Clause learning without clause deletion can worsen solver performance.

Solver runtime distributions are multimodal and can be modeled with Weibull mixtures.

Clause forgetting helps prevent long-tail runtimes, improving solver efficiency.

Abstract

Conflict-driven clause learning (CDCL) is a remarkably successful paradigm for solving the satisfiability problem of propositional logic. Instead of a simple depth-first backtracking approach, this kind of solver learns the reason behind occurring conflicts in the form of additional clauses. However, despite the enormous success of CDCL solvers, there is still only a limited understanding of what influences the performance of these solvers in what way. Considering different measures, this paper demonstrates, quite surprisingly, that clause learning (without being able to get rid of some clauses) can not only help the solver but can oftentimes deteriorate the solution process dramatically. By conducting extensive empirical analysis, we furthermore find that the runtime distributions of CDCL solvers are multimodal. This multimodality can be seen as a reason for the deterioration phenomenon described above. Simultaneously, it also gives an indication of why clause learning in combination with clause deletion is virtually the de facto standard of SAT solving, in spite of this phenomenon. As a final contribution, we show that Weibull mixture distributions can accurately describe the multimodal distributions. Thus, adding new clauses to a base instance has an inherent effect of making runtimes long-tailed. This insight provides an explanation as to why the technique of forgetting clauses is useful in CDCL solvers apart from the optimization of unit propagation speed.