首页    期刊浏览 2024年11月08日 星期五
登录注册

文章基本信息

  • 标题: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
国家哲学社会科学文献中心版权所有