---
title: "Finding the Hardest Formulas for Resolution (Extended Abstract)"
authors:
  - "Tomáš Peitl"
  - "Stefan Szeider"
doi: "10.24963/ijcai.2021/657"
url: "https://ijcai.org/proceedings/2021/657"
pdf: "https://ijcai.org/proceedings/2021/0657.pdf"
venue: "Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence"
year: 2021
pages: "4814-4818"
track: "Sister Conferences Best Papers"
keywords:
  - "Constraints and SAT: Constraint Satisfaction"
  - "Constraints and SAT: SAT: Algorithms and Techniques"
  - "Constraints and SAT: Constraints: Modeling, Solvers, Applications"
  - "Constraints and SAT: SAT: Solvers and Applications"
---

# Finding the Hardest Formulas for Resolution (Extended Abstract)

Tomáš Peitl, Stefan Szeider

*Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence*, pages 4814-4818. DOI: [10.24963/ijcai.2021/657](https://doi.org/10.24963/ijcai.2021/657)

## Abstract

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.