Finding the Hardest Formulas for Resolution (Extended Abstract)

Peitl, Tomáš; Szeider, Stefan

doi:10.24963/ijcai.2021/657

Finding the Hardest Formulas for Resolution (Extended Abstract)

Download BibTeX Cite

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

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

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.

Tomáš Peitl, and Stefan Szeider. 2021. Finding the Hardest Formulas for Resolution (Extended Abstract). In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21. IJCAI, 4814–4818. https://doi.org/10.24963/ijcai.2021/657

@inproceedings{ijcai2021p657,
  title     = {Finding the Hardest Formulas for Resolution (Extended Abstract)},
  author    = {Peitl, Tomáš and Szeider, Stefan},
  booktitle = {Proceedings of the Thirtieth International Joint Conference on
               Artificial Intelligence, {IJCAI-21}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  editor    = {Prof. Zhi-Hua Zhou},
  pages     = {4814--4818},
  year      = {2021},
  month     = {8},
  note      = {Sister Conferences Best Papers},
  doi       = {10.24963/ijcai.2021/657},
  url       = {https://doi.org/10.24963/ijcai.2021/657},
}

TY  - CPAPER
TI  - Finding the Hardest Formulas for Resolution (Extended Abstract)
AU  - Peitl, Tomáš
AU  - Szeider, Stefan
T2  - Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21
PB  - International Joint Conferences on Artificial Intelligence Organization
PY  - 2021
SP  - 4814
EP  - 4818
DO  - 10.24963/ijcai.2021/657
UR  - https://doi.org/10.24963/ijcai.2021/657
ER  -