T. Peitl, S. Szeider:

"Finding the Hardest Formulas for Resolution (Extended Abstract)";

Talk: IJCAI 2021 - 30th International Joint Conference on Artificial Intelligence, Montreal, Canada; 2021-08-19 - 2021-08-27; in: "Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence (IJCAI-21)", (2021), ISBN: 978-0-9992411-9-6; 4814 - 4818.

A CNF formula is harder than another CNF formula

with the same number of clauses if it requires

a longer resolution proof. We introduce resolution

hardness numbers; they 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. To achieve this, we devise

a candidate filtering and symmetry breaking search

scheme for limiting the number of potential candidates

for hardest formulas, and an efficient SAT

encoding for computing a shortest resolution proof

of a given candidate formula.

http://dx.doi.org/10.24963/ijcai.2021/657

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

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