Finding the Hardest Formulas for Resolution
Abstract
A CNF formula is harder than another CNF formula with the same number of clauses if it requires a longer resolution proof. In this paper we introduce resolution hardness numbers; they give for m=1,2,... the length of a shortest proof of a hardest formula on m clauses. We compute the first ten resolution hardness numbers, along with the corresponding hardest formulas. To achieve this, we devise a candidate filtering and symmetry breaking search scheme for limiting the number of potential candidates for hardest for- mulas, and an efficient SAT encoding for computing a shortest resolution proof of a given candidate formula.
Cite
Text
Peitl and Szeider. "Finding the Hardest Formulas for Resolution." Journal of Artificial Intelligence Research, 2021. doi:10.1613/JAIR.1.12589Markdown
[Peitl and Szeider. "Finding the Hardest Formulas for Resolution." Journal of Artificial Intelligence Research, 2021.](https://mlanthology.org/jair/2021/peitl2021jair-finding/) doi:10.1613/JAIR.1.12589BibTeX
@article{peitl2021jair-finding,
title = {{Finding the Hardest Formulas for Resolution}},
author = {Peitl, Tomás and Szeider, Stefan},
journal = {Journal of Artificial Intelligence Research},
year = {2021},
pages = {69-97},
doi = {10.1613/JAIR.1.12589},
volume = {72},
url = {https://mlanthology.org/jair/2021/peitl2021jair-finding/}
}