Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
T. Peitl, S. Szeider:
"Finding the Hardest Formulas for Resolution";
Vortrag: International Conference on Principles and Practice of Constraint Programming (CP),
Louvain-la-Neuve, Belgium;
07.09.2020
- 11.09.2020; in: "CP 2020: Principles and Practice of Constraint Programming",
LNCS,
12333
(2020),
ISBN: 978-3-030-58474-0;
S. 514
- 530.
Kurzfassung englisch:
A CNF formula is harder than another CNF formula with
the same number of clauses if it requires a longer resolution proof. The
resolution hardness numbers 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.
We achieve this by a candidate filtering and symmetry breaking search
scheme for limiting the number of potential candidates for 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.1007/978-3-030-58475-7_30
Elektronische Version der Publikation:
https://publik.tuwien.ac.at/files/publik_292405.pdf
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.