On Davis-Putnam reductions for minimally unsatisfiable clause-sets

TL;DR

This paper analyzes the structure of minimally unsatisfiable clause-sets using singular Davis-Putnam reductions, establishing confluence properties and structural invariants, which advances understanding of their classification based on deficiency.

Contribution

It provides a detailed analysis of singular DP-reduction in MU clause-sets, proving confluence modulo isomorphism and structural invariants, especially for saturated and eventually saturated cases.

Findings

n(F') = n(F'') for all F', F'' in sDP(F)

Unique sDP(F) for saturated F in SMU

Confluence modulo isomorphism for MU(2) clause-sets

Abstract

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.