DRAT 与不带新变量的传播冗余证明
DRAT and Propagation Redundancy Proofs Without New Variables
AI总结：
研究不带新变量的冗余证明系统，引入更一般的 SR 规则，证明带删除时 DRAT⁻、DSPR⁻、DPR⁻ 等价，不带删除时 SPR⁻ 可模拟 PR⁻ 且能处理多种困难原理，并给出 RAT⁻ 的指数下界。
摘要：
我们研究了一系列命题证明系统的复杂性，这些系统允许如下形式的推理规则：从一组子句 Γ 推导出子句集 Γ ∪ { C }，其中，由于某种语法条件，如果 Γ 是可满足的，则 Γ ∪ { C } 也是可满足的，但 Γ 并不一定蕴含 C。这些推理规则包括 BC、RAT、SPR 和 PR（分别代表阻塞子句、消解非对称重言式、子集传播冗余和传播冗余），它们源于可满足性（SAT）求解方面的工作。我们引入了一个新的、更一般的规则 SR（替换冗余）。如果允许新子句 C 包含新变量，则基于这些规则的系统都等价于扩展消解。我们专注于不允许新变量的受限系统。带删除的系统，即我们可以随时从子句集中删除一个子句，分别记为 DBC⁻、DRAT⁻、DSPR⁻、DPR⁻ 和 DSR⁻。不带删除的系统分别为 BC⁻、RAT⁻、SPR⁻、PR⁻ 和 SR⁻。对于带删除的情况，我们证明了 DRAT⁻、DSPR⁻ 和 DPR⁻ 是等价的。根据 Kiesl、Rebola-Pardo 和 Heule 的早期工作，它们也等价于 DBC⁻。对于不带删除的情况，我们证明了 SPR⁻ 可以模拟 PR⁻，前提是 SPR 推理只推断短子句。我们还证明了许多著名的“困难”原理具有小的 SPR⁻ 反驳，包括鸽巢原理、位鸽巢原理、奇偶原理、Tseitin 重言式和团-着色重言式。SPR⁻ 还可以处理 or-化、xor-化以及带索引装置的提升。我们的最终结果是 RAT⁻ 反驳的指数级下界，给出了 RAT⁻ 与 DRAT⁻ 和 SPR⁻ 之间的指数分离。
英文摘要：
We study the complexity of a range of propositional proof systems which allow inference rules of the form: from a set of clauses $Γ$ derive the set of clauses $Γ\cup \{ C \}$ where, due to some syntactic condition, $Γ\cup \{ C \}$ is satisfiable if $Γ$ is, but where $Γ$ does not necessarily imply $C$. These inference rules include BC, RAT, SPR and PR (respectively short for blocked clauses, resolution asymmetric tautologies, subset propagation redundancy and propagation redundancy), which arose from work in satisfiability (SAT) solving. We introduce a new, more general rule SR (substitution redundancy). If the new clause $C$ is allowed to include new variables then the systems based on these rules are all equivalent to extended resolution. We focus on restricted systems that do not allow new variables. The systems with deletion, where we can delete a clause from our set at any time, are denoted DBC${}^-$, DRAT${}^-$, DSPR${}^-$, DPR${}^-$ and DSR${}^-$. The systems without deletion are BC${}^-$, RAT${}^-$, SPR${}^-$, PR${}^-$ and SR${}^-$. With deletion, we show that DRAT${}^-$, DSPR${}^-$ and DPR${}^-$ are equivalent. By earlier work of Kiesl, Rebola-Pardo and Heule, they are also equivalent to DBC${}^-$. Without deletion, we show that SPR${}^-$ can simulate PR${}^-$ provided only short clauses are inferred by SPR inferences. We also show that many of the well-known "hard" principles have small SPR${}^-$ refutations. These include the pigeonhole principle, bit pigeonhole principle, parity principle, Tseitin tautologies and clique-coloring tautologies. SPR${}^-$ can also handle or-fication and xor-ification, and lifting with an index gadget. Our final result is an exponential size lower bound for RAT${}^-$ refutations, giving exponential separations between RAT${}^-$ and both DRAT${}^-$ and SPR${}^-$.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
