ML Anthology

Finding the Hardest Formulas for Resolution (Extended Abstract)

Tomás Peitl, Stefan Szeider
IJCAI 2021 pp. 4814-4818
doi:10.24963/IJCAI.2021/657 /ijcai/2021/peitl2021ijcai-finding/

Abstract

A CNF formula is harder than another CNF formula with the same number of clauses if it requires a longer resolution proof. 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 formulas, and an efficient SAT encoding for computing a shortest resolution proof of a given candidate formula.

PDF IJCAI Semantic Scholar

Cite

Text

Peitl and Szeider. "Finding the Hardest Formulas for Resolution (Extended Abstract)." International Joint Conference on Artificial Intelligence, 2021. doi:10.24963/IJCAI.2021/657

Markdown

[Peitl and Szeider. "Finding the Hardest Formulas for Resolution (Extended Abstract)." International Joint Conference on Artificial Intelligence, 2021.](https://mlanthology.org/ijcai/2021/peitl2021ijcai-finding/) doi:10.24963/IJCAI.2021/657

BibTeX

@inproceedings{peitl2021ijcai-finding,
  title     = {{Finding the Hardest Formulas for Resolution (Extended Abstract)}},
  author    = {Peitl, Tomás and Szeider, Stefan},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2021},
  pages     = {4814-4818},
  doi       = {10.24963/IJCAI.2021/657},
  url       = {https://mlanthology.org/ijcai/2021/peitl2021ijcai-finding/}
}