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)

Electronic version of the publication:

Created from the Publication Database of the Vienna University of Technology.