极小不可满足子句集的Davis-Putnam约简
On Davis-Putnam reductions for minimally unsatisfiable clause-sets
摘要：
为了研究MU的结构，即，最小不可满足子句集或合取范式，奇异DP-归约是一个基本工具，在变量v仅在一个极性中出现一次的情况下应用DP-归约F -> DP_v（F）。回想一下，一般来说，DP_v（F）用v上的预解式替换所有包含变量v的子句（另一个名字是“变量消除”）。我们考虑sDP（F），尽可能长地将奇异DP-约简应用于MU中的F的所有结果的集合，获得MU中具有相同缺陷的非奇异F'，即，delta（F '）= delta（F）。(In一般来说，delta（F）是子句数与变量数之差c（F）- n（F）。我们的主要结果是：1.对于SDP（F）中的所有F '，F”，我们有n（F'）= n（F”）。2.如果F是饱和的（SMU中的F），则我们有|SDP（F）|= 1。3.如果F是“最终饱和的”，即sDP（F）<= SMU，则对于sDP（F）中的F '，F”，我们有F'同构F”（建立“汇合模同构”）。通过对MU中F的奇异DP-约化的详细分析，得到了这些结果。作为一个应用，我们得到了MU（2）中F的奇异DP-约化（即，delta（F）= 2）是合流模同构（使用Kleine Buening对MU（2）的基本刻画）。这些考虑的背景是一般项目的分类的MU方面的不足。
英文摘要：
For investigations into the structure of MU, i.e., minimally unsatisfiable clause-sets or conjunctive normal forms, singular DP-reduction is a fundamental tool, applying DP-reduction F -> DP_v(F) in case variable v occurs in one polarity only once. Recall, in general DP_v(F) replaces all clauses containing variable v by their resolvents on v (another name is "variable elimination"). We consider sDP(F), the set of all results of applying singular DP-reduction to F in MU as long as possible, obtaining non-singular F' in MU with the same deficiency, i.e., delta(F') = delta(F). (In general, delta(F) is the difference c(F) - n(F) of the number of clauses and the number of variables.) Our main results are: 1. For all F', F" in sDP(F) we have n(F') = n(F"). 2. If F is saturated (F in SMU), then we have |sDP(F)| = 1. 3. If F is "eventually saturated", that is, sDP(F) <= SMU, then for F', F" in sDP(F) we have F' isomorphic F" (establishing "confluence modulo isomorphism"). The results are obtained by a detailed analysis of singular DP-reduction for F in MU. As an application we obtain that singular DP-reduction for F in MU(2) (i.e., delta(F) = 2) is confluent modulo isomorphism (using the fundamental characterisation of MU(2) by Kleine Buening). The background for these considerations is the general project of the classification of MU in terms of the deficiency.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
