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.