Finding the Hardest Formulas for Resolution (Extended Abstract)

Finding the Hardest Formulas for Resolution (Extended Abstract)

Tomáš Peitl, Stefan Szeider

Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence
Sister Conferences Best Papers. Pages 4814-4818. https://doi.org/10.24963/ijcai.2021/657

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.
Keywords:
Constraints and SAT: SAT: Solvers and Applications
Constraints and SAT: Constraints: Modeling, Solvers, Applications
Constraints and SAT: SAT: Algorithms and Techniques
Constraints and SAT: Constraint Satisfaction