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