Too much information: Why CDCL solvers need to forget learned clauses.

Area of Science:

• Artificial Intelligence
• Computer Science
• Computational Logic

Background:

• Conflict-driven clause learning (CDCL) solvers are highly effective for propositional satisfiability (SAT) problems.
• CDCL solvers learn from conflicts by adding clauses, improving upon simple backtracking.
• Limited understanding exists regarding factors influencing CDCL solver performance.

Purpose of the Study:

• To investigate the impact of clause learning on CDCL solver performance.
• To analyze the reasons behind performance variations and potential deterioration.
• To explain the necessity of clause deletion in SAT solving.

Main Methods:

• Conducted extensive empirical analysis of CDCL solver performance.
• Examined runtime distributions and their characteristics.
• Modeled runtime distributions using Weibull mixture distributions.

Main Results:

• Clause learning, without deletion, can significantly deteriorate CDCL solver performance.
• CDCL solver runtime distributions exhibit multimodality.
• Weibull mixture distributions accurately model these multimodal runtimes.

Conclusions:

• Clause learning's negative impact is linked to multimodal runtime distributions.
• Clause deletion is essential for efficient SAT solving, mitigating performance deterioration.
• Multimodal distributions explain the utility of clause forgetting in CDCL solvers.