Talks and Poster Presentations (with Proceedings-Entry):
T. Peitl, S. Szeider:
"Finding the Hardest Formulas for Resolution";
Talk: International Conference on Principles and Practice of Constraint Programming (CP),
Louvain-la-Neuve, Belgium;
2020-09-07
- 2020-09-11; in: "CP 2020: Principles and Practice of Constraint Programming",
LNCS,
12333
(2020),
ISBN: 978-3-030-58474-0;
514
- 530.
English abstract:
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.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-030-58475-7_30
Electronic version of the publication:
https://publik.tuwien.ac.at/files/publik_292405.pdf
Created from the Publication Database of the Vienna University of Technology.