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),
- 2020-09-11; in: "CP 2020: Principles and Practice of Constraint Programming",
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)
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.