文章基本信息

标题：Finding the Hardest Formulas for Resolution
本地全文：下载
作者：Yotam Gafni ; Ron Lavi ; Moshe Tennenholtz 等
期刊名称：Journal of Artificial Intelligence Research
印刷版ISSN：1076-9757
出版年度：2021
卷号：72
页码：1-29
DOI：10.1613/jair.1.12589
语种：English
出版社：American Association of Artificial
摘要：A CNF formula is harder than another CNF formula with the same number of clauses if it requires a longer resolution proof. In this paper 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 for- mulas and an efficient SAT encoding for computing a shortest resolution proof of a given candidate formula.
关键词：satisfiability;automated reasoning;mathematical foundations