IJCAI 2021poster0 citations
Finding the Hardest Formulas for Resolution (Extended Abstract)
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.
Constraints and SAT: SAT: Solvers and ApplicationsConstraints and SAT: Constraints: Modeling, Solvers, ApplicationsConstraints and SAT: SAT: Algorithms and TechniquesConstraints and SAT: Constraint Satisfaction
BibTeX
@inproceedings{ijcai2021p657,
title = {Finding the Hardest Formulas for Resolution (Extended Abstract)},
author = {Peitl, Tomáš and Szeider, Stefan},
booktitle = {Proceedings of the Thirtieth International Joint Conference on
Artificial Intelligence, {IJCAI-21}},
publisher = {International Joint Conferences on Artificial Intelligence Organization},
editor = {Zhi-Hua Zhou},
pages = {4814--4818},
year = {2021},
month = {8},
note = {Sister Conferences Best Papers},
doi = {10.24963/ijcai.2021/657},
url = {https://doi.org/10.24963/ijcai.2021/657},
}