A New Clause Learning Scheme for Efficient Unsatisfiability Proofs
Abstract
We formalize in this paper a key property of asserting clauses (the most common type of clauses learned by SAT solvers). We show that the formalized property, which is called empowerment, is not exclusive to asserting clauses, and introduce a new class of learned clauses which can also be empowering. We show empirically that (1) the new class of clauses tends to be much shorter and induce further backtracks than asserting clauses and (2) an empowering subset of this new class of clauses significantly improves the performance of the Rsat solver on unsatisfiable problems.
Cite
Text
Pipatsrisawat and Darwiche. "A New Clause Learning Scheme for Efficient Unsatisfiability Proofs." AAAI Conference on Artificial Intelligence, 2008.Markdown
[Pipatsrisawat and Darwiche. "A New Clause Learning Scheme for Efficient Unsatisfiability Proofs." AAAI Conference on Artificial Intelligence, 2008.](https://mlanthology.org/aaai/2008/pipatsrisawat2008aaai-new-a/)BibTeX
@inproceedings{pipatsrisawat2008aaai-new-a,
title = {{A New Clause Learning Scheme for Efficient Unsatisfiability Proofs}},
author = {Pipatsrisawat, Knot and Darwiche, Adnan},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2008},
pages = {1481-1484},
url = {https://mlanthology.org/aaai/2008/pipatsrisawat2008aaai-new-a/}
}