Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
T. Peitl, S. Szeider:
"Finding the Hardest Formulas for Resolution (Extended Abstract)";
Vortrag: IJCAI 2021 - 30th International Joint Conference on Artificial Intelligence,
Montreal, Canada;
19.08.2021
- 27.08.2021; in: "Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence (IJCAI-21)",
(2021),
ISBN: 978-0-9992411-9-6;
S. 4814
- 4818.
Kurzfassung englisch:
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.
"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.24963/ijcai.2021/657
Elektronische Version der Publikation:
https://publik.tuwien.ac.at/files/publik_300143.pdf
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.