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.

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.

http://dx.doi.org/10.1007/978-3-030-58475-7_30

https://publik.tuwien.ac.at/files/publik_292405.pdf

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