Predicting Learnt Clauses Quality in Modern SAT Solvers
Proceedings of the Twenty-First International Joint Conference on Artificial Intelligence. Pages 399-403.
Abstract
Beside impressive progresses made by SAT solvers over the last ten years, only few works tried to understand why Conflict Directed Clause Learning algorithms (CDCL) are so strong and efficient on most industrial applications. We report in this work a key observation of CDCL solvers behavior on this family of benchmarks and explain it by an unsuspected side effect of their particular Clause Learning scheme. This new paradigm allows us to solve an important, still open, question: How to designing a fast, static, accurate, and predictive measure of new learnt clauses pertinence. Our paper is followed by empirical evidences that show how our new learning scheme improves state-of-the art results by an order of magnitude on both SAT and UNSAT industrial problems.Gilles Audemard, Laurent Simon
@inproceedings{ijcai2009p74,
title = {Predicting Learnt Clauses Quality in Modern SAT Solvers},
author = {Audemard, Gilles and Simon, Laurent},
booktitle = {Proceedings of the Twenty-First International Joint Conference on
Artificial Intelligence, {IJCAI-09}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Hiroaki Kitano},
pages = {399--403},
year = {2009},
url = {https://ijcai.org/proceedings/2009/74},
}
TY - CPAPER TI - Predicting Learnt Clauses Quality in Modern SAT Solvers AU - Audemard, Gilles AU - Simon, Laurent T2 - Proceedings of the Twenty-First International Joint Conference on Artificial Intelligence, IJCAI-09 PB - International Joint Conferences on Artificial Intelligence PY - 2009 SP - 399 EP - 403 UR - https://ijcai.org/proceedings/2009/74 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
