On Davis-Putnam reductions for minimally unsatisfiable clause-sets

详细信息    查看全文

• 作者：Oliver Kullmann^a ; ^{O.Kullmann@Swansea.ac.uk} ; Xishun Zhao^b ;
• 关键词：Clause-sets (CNFs) ; Minimal unsatisfiability ; DP-reduction (Davis&ndash ; Putnam reduction) ; Variable elimination ; Confluence ; Isomorphism ; Singular variables ; Singular DP-reduction ; Deficiency
• 刊名：Theoretical Computer Science
• 出版年：2013
• 出版时间：24 June, 2013
• 年：2013
• 卷：492
• 期：Complete
• 页码：70-87
• 全文大小：548 K

文摘

DP-reduction , applied to a clause-set and a variable , replaces all clauses containing by their resolvents (on ). A basic case, where the number of clauses is decreased (i.e., ), is singular DP-reduction (sDP-reduction), where must occur in one polarity only once. For minimally unsatisfiable , sDP-reduction produces another with the same deficiency, that is, ; recall , using for the number of variables. Let for be the set of results of complete sDP-reduction for ; so fulfil , are nonsingular (every literal occurs at least twice), and we have . We show that for all complete reductions by sDP must have the same length, establishing the singularity index of . In other words, for we have . In general the elements of are not even (pairwise) isomorphic. Using the fundamental characterisation by Kleine B¨¹ning, we obtain as application of the singularity index, that we have confluence modulo isomorphism (all elements of are pairwise isomorphic) in case . In general we prove that we have confluence (i.e., ) for saturated (i.e., ). More generally, we show confluence modulo isomorphism for eventually saturated, that is, where we have , yielding another proof for confluence modulo isomorphism in case of .