Clausal Proofs of Mutilated Chessboards

机译：残缺棋盘的条款证明

获取原文

页面导航

摘要
著录项
相似文献
相关主题

摘要

Mutilated chessboard problems have been called a 'tough nut to crack' for automated reasoning. They are, for instance, hard for resolution, resulting in exponential runtime of current SAT solvers. Although there exists a well-known short argument for solving mutilated chessboard problems, this argument is based on an abstraction that is challenging to discover by automated-reasoning techniques. In this paper, we present another short argument that is much easier to compute and that can be expressed within the recent (clausal) PR proof system for propositional logic. We construct short clausal proofs of mutilated chessboard problems using this new argument and validate them using a formally-verified proof checker.

机译：残缺的棋盘问题被称为自动推理的“难题”。例如，它们很难解析，从而导致当前SAT求解器的运行时间成指数增长。尽管存在解决残缺的棋盘问题的众所周知的简短论点，但该论点基于的抽象很难通过自动推理技术来发现。在本文中，我们提出了另一个简短的论点，该论点更容易计算，并且可以在命题逻辑的最新（子句）PR证明系统中表达。我们使用这个新的论点构造残缺的棋盘问题的简短证明，并使用正式验证的证明检查器对其进行验证。

著录项

来源
《NASA Formal Methods Symposium》|2019年|204-210|共7页
会议地点 Houston(US)
作者
Marijn J. H. Heule; Benjamin Kiesl; Armin Biere;
展开▼
作者单位

Department of Computer Science The University of Texas Austin USA;

Institute of Logic and Computation TU Wien Vienna Austria CISPA Helmholtz Center for Information Security Saarbruecken Germany;

Institute for Formal Models and Verification JKU Linz Linz Austria;

展开▼
会议组织
原文格式 PDF
正文语种
中图分类
关键词

相似文献

外文文献
中文文献
专利

1. The Complexity of Multi-source Variants of the End-of-Line Problem, and the Concise Mutilated Chessboard [J] . Alexandros Hollender, Paul Goldberg Electronic Colloquium on Computational Complexity . 2018,第4期

机译：行尾问题的多源变体的复杂性以及简明的残缺棋盘
2. Mutilated chessboard problem is exponentially hard for resolution [J] . Michael Alekhnovich Theoretical computer science . 2004,第1a3期

机译：残缺的棋盘问题很难解决
3. Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis [J] . Farka Frantisek, Komendantskya Ekaterina, Hammond Kevin Theory and Practice of Logic Programming . 2018,第3a4期

机译：相关类型推断和术语合成的与证明相关的Horn子句
4. Clausal Proofs of Mutilated Chessboards [C] . Marijn J. H. Heule, Benjamin Kiesl, Armin Biere NASA Formal Methods Symposium . 2019

机译：肢解棋盘的责任证明
5. Proof System of Higher-Order Clausal Logic and its Parallel Implementation [D] . Miura, Kinya 1995

机译：高阶从句逻辑的证明系统及其并行实现
6. Labelled Interpolation Systems for Hyper-Resolution Clausal and Local Proofs [O] . Matthias Schlaipfer, Georg Weissenbacher -1

机译：标记的插值系统用于超分辨率从句和局部证明
7. Mutilated chessboard problem is exponentially hard for resolution [O] . Alekhnovich Michael 2004

机译：残缺的棋盘问题很难解决

Clausal Proofs of Mutilated Chessboards

摘要

著录项

相似文献

相关主题

期刊订阅