On Davis-Putnam reductions for minimally unsatisfiable clause-sets

Details On Davis-Putnam reductions for minimally unsatisfiable clause-sets On Davis-Putnam reductions for minimally unsatisfiable clause-sets

2012-02-13

arxiv.org/abs/1202.2600v2

Computer Science

Discrete Mathematics

17 pages; various editorial improvements for the second version

Scientific paper

For investigations into the structure of MU (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.) 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.

Affiliated with

Also associated with

No associations

Rating

On Davis-Putnam reductions for minimally unsatisfiable clause-sets does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with On Davis-Putnam reductions for minimally unsatisfiable clause-sets, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On Davis-Putnam reductions for minimally unsatisfiable clause-sets will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-680800