关于2CNF公式中只读一次分辨可判定性的计算复杂性
On the computational complexity of read once resolution decidability in 2CNF formulas
摘要：
本文从只读一次归结（ROR）反驳方案的角度分析了2CNF公式。我们关注两种类型的ROR反驳，即，变元一次反驳和子句一次反驳。在前者中，每个变量在推导反驳时最多使用一次，而在后者中，每个子句最多使用一次。我们证明了在这两种方案下检验给定的2CNF公式是否有ROR反驳的问题是NP-完全的。这是令人惊讶的事实，存在多项式反驳计划（树分辨率和DAG分辨率）的2CNF公式。在积极的一面，我们证明了2CNF公式的复制复杂度为2，这意味着任何不可满足的2CNF公式都有一个反驳，其中任何子句最多需要使用两次。
英文摘要：
In this paper, we analyze 2CNF formulas from the perspectives of Read-Once resolution (ROR) refutation schemes. We focus on two types of ROR refutations, viz., variable-once refutation and clause-once refutation. In the former, each variable may be used at most once in the derivation of a refutation, while in the latter, each clause may be used at most once. We show that the problem of checking whether a given 2CNF formula has an ROR refutation under both schemes is NP-complete. This is surprising in light of the fact that there exist polynomial refutation schemes (tree-resolution and DAG-resolution) for 2CNF formulas. On the positive side, we show that 2CNF formulas have copy-complexity 2, which means that any unsatisfiable 2CNF formula has a refutation in which any clause needs to be used at most twice.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
