通过嵌套输入归结推广单元反驳完备性与 SLUR
摘要
我们基于 1995 年引入的 SLUR（单次前瞻单元反驳）类和 1994 年引入的 UC（单元反驳完备）类，引入了两个子句集层次结构：SLUR_k 和 UC_k。SLUR 类由 Annexstein 等人于 1995 年引入，指那些单元子句传播（记为 r_1）能检测出不可满足性，或者否则通过前瞻避免明显错误赋值后的迭代赋值总能产生满足赋值的子句集。考虑如何基于 SLUR 构建层次结构是自然的。此类研究始于 Cepek 等人（2012）和 Balyo 等人（2012）。我们提出了我们认为的“极限层次”SLUR_k，其基于将 r_1 推广为 r_k，即使用 Kullmann（1999, 2004）引入的广义单元子句传播。Del Val（1994）研究的 UC 类是单元反驳完备子句集类，即那些在任何 falsifying 赋值下，其不可满足性均可由 r_1 判定的子句集。对于不可满足子句集 F，使得 r_k 判定 F 不可满足的最小 k 值正是 [Ku 99, 04] 中引入的 F 的“硬度”。对于可满足的 F，我们采用 Ansotegui 等人（2008）提及的一个扩展：硬度是指在任何 falsifying 部分赋值应用后，使得 r_k 判定不可满足的最小 k 值。UC_k 类由硬度 <= k 的子句集构成。我们观察到 UC_1 恰好就是 UC。由于硬度与树归结之间的关系，UC_k 具有证明论特征，而 SLUR_k 具有算法特征。r_k 与 k 次嵌套输入归结（或使用子句空间 k+1 的树归结）之间的对应关系意味着 r_k 具有双重性质：既是算法的也是证明论的。这对应于本文的一个基本结果，即 SLUR_k = UC_k。
引用
@article{arxiv.1204.6529,
title = {Generalising unit-refutation completeness and SLUR via nested input resolution},
author = {Matthew Gwynne and Oliver Kullmann},
journal= {arXiv preprint arXiv:1204.6529},
year = {2015}
}
备注
41 pages; second version improved formulations and added examples, and more details regarding future directions, third version further examples, improved and extended explanations, and more on SLUR, fourth version various additional remarks and editorial improvements, fifth version more explanations and references, typos corrected, improved wording