通过嵌套输入归结推广单位反驳完备性和SLUR
Generalising unit-refutation completeness and SLUR via nested input resolution
摘要：
我们介绍了两个层次的子句集，SLUR_k和UC_k，基于类SLUR（单前瞻单元反驳），在1995年推出，和UC（单元反驳完成），在1994年推出。在[Annexstein et al，1995]中引入的类SLUR是子句集的类，对于该子句集，单位子句传播（由r_1表示）检测不可满足性，或者在其他情况下迭代分配，通过前瞻避免明显的错误分配，总是产生令人满意的分配。考虑如何形成基于SLUR的层次结构是很自然的。此类研究始于[Cepek et al，2012]和[Balyo et al，2012]。我们提出了我们认为的“极限层次”SLUR_k，根据推广r_1的r_k，也就是说，使用广义单位子句传播介绍[Kullmann，1999年，2004年]。在[Del Val，1994]中研究的UC类是单位反驳完备子句集类，即在任意证伪指派下，r_1都可判定其不可满足性的子句集。对于不可满足子句集F，使r_k决定F的不可满足性的最小值k正是F的“硬度”，如[Ku 99，04]中所介绍的。对于可满足的F，我们现在使用[Ansotegui et al，2008]中提到的扩展：硬度是最小的k，使得在应用任何伪造部分赋值之后，r_k确定不可满足性。类UC_k由硬度<= k的子句集给出。我们观察到UC_1恰好是UC。UC_k具有证明论性质，这是由于硬度和树分辨率之间的关系，而SLUR_k具有算法性质。r_k与k次嵌套输入归结（或使用子句空间k+1的树归结）之间的对应意味着r_k具有双重性质：算法和证明理论。这对应于本文的一个基本结果，即SLUR_k = UC_k。
英文摘要：
We introduce two hierarchies of clause-sets, SLUR_k and UC_k, based on the classes SLUR (Single Lookahead Unit Refutation), introduced in 1995, and UC (Unit refutation Complete), introduced in 1994. The class SLUR, introduced in [Annexstein et al, 1995], is the class of clause-sets for which unit-clause-propagation (denoted by r_1) detects unsatisfiability, or where otherwise iterative assignment, avoiding obviously false assignments by look-ahead, always yields a satisfying assignment. It is natural to consider how to form a hierarchy based on SLUR. Such investigations were started in [Cepek et al, 2012] and [Balyo et al, 2012]. We present what we consider the "limit hierarchy" SLUR_k, based on generalising r_1 by r_k, that is, using generalised unit-clause-propagation introduced in [Kullmann, 1999, 2004]. The class UC, studied in [Del Val, 1994], is the class of Unit refutation Complete clause-sets, that is, those clause-sets for which unsatisfiability is decidable by r_1 under any falsifying assignment. For unsatisfiable clause-sets F, the minimum k such that r_k determines unsatisfiability of F is exactly the "hardness" of F, as introduced in [Ku 99, 04]. For satisfiable F we use now an extension mentioned in [Ansotegui et al, 2008]: The hardness is the minimum k such that after application of any falsifying partial assignments, r_k determines unsatisfiability. The class UC_k is given by the clause-sets which have hardness <= k. We observe that UC_1 is exactly UC. UC_k has a proof-theoretic character, due to the relations between hardness and tree-resolution, while SLUR_k has an algorithmic character. The correspondence between r_k and k-times nested input resolution (or tree resolution using clause-space k+1) means that r_k has a dual nature: both algorithmic and proof theoretic. This corresponds to a basic result of this paper, namely SLUR_k = UC_k.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
