[Back]


Talks and Poster Presentations (with Proceedings-Entry):

T. Peitl, S. Szeider:
"Finding the Hardest Formulas for Resolution (Extended Abstract)";
Talk: IJCAI 2021 - 30th International Joint Conference on Artificial Intelligence, Montreal, Canada; 2021-08-19 - 2021-08-27; in: "Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence (IJCAI-21)", (2021), ISBN: 978-0-9992411-9-6; 4814 - 4818.



English 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.


"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.24963/ijcai.2021/657

Electronic version of the publication:
https://publik.tuwien.ac.at/files/publik_300143.pdf


Created from the Publication Database of the Vienna University of Technology.