Improving and Understanding the Power of Satisfaction-Driven Clause Learning
Abstract
In this paper, we explain how to improve Satisfaction-Driven Clause Learning (SDCL) SAT solvers by using a MaxSAT-based technique that enables them to learn shorter, and hence better, redundant clauses. A thorough empirical evaluation of an implementation on the MapleSAT solver shows that the resulting system solves Mutilated Chess Board (MCB) problems significantly faster than CDCL solvers, without requiring any alteration to the branching heuristic used by the underlying CDCL SAT solver. Additionally we improve the understanding of the power of these solvers by proving that, given a refutation of a formula that consists of resolution and redundant-clause addition steps, an SDCL solver is able to produce a proof whose size is polynomial with respect to the size of the original refutation.
Cite
Text
Oliveras et al. "Improving and Understanding the Power of Satisfaction-Driven Clause Learning." Journal of Artificial Intelligence Research, 2025. doi:10.1613/JAIR.1.18286Markdown
[Oliveras et al. "Improving and Understanding the Power of Satisfaction-Driven Clause Learning." Journal of Artificial Intelligence Research, 2025.](https://mlanthology.org/jair/2025/oliveras2025jair-improving/) doi:10.1613/JAIR.1.18286BibTeX
@article{oliveras2025jair-improving,
title = {{Improving and Understanding the Power of Satisfaction-Driven Clause Learning}},
author = {Oliveras, Albert and Li, Chunxiao and Wu, Darryl and Chung, Jonathan and Ganesh, Vijay},
journal = {Journal of Artificial Intelligence Research},
year = {2025},
doi = {10.1613/JAIR.1.18286},
volume = {83},
url = {https://mlanthology.org/jair/2025/oliveras2025jair-improving/}
}