On variables with few occurrences in conjunctive normal forms

Details On variables with few occurrences in conjunctive normal forms On variables with few occurrences in conjunctive normal forms

2010-10-27

arxiv.org/abs/1010.5756v3

SAT 2011, LNCS 6695, 33

Computer Science

Discrete Mathematics

14 pages. Revision contains more explanations, and more information regarding the sharpness of the bound

Scientific paper

10.1007/978-3-642-21581-0_5

We consider the question of the existence of variables with few occurrences in boolean conjunctive normal forms (clause-sets). Let mvd(F) for a clause-set F denote the minimal variable-degree, the minimum of the number of occurrences of variables. Our main result is an upper bound mvd(F) <= nM(surp(F)) <= surp(F) + 1 + log_2(surp(F)) for lean clause-sets F in dependency on the surplus surp(F). - Lean clause-sets, defined as having no non-trivial autarkies, generalise minimally unsatisfiable clause-sets. - For the surplus we have surp(F) <= delta(F) = c(F) - n(F), using the deficiency delta(F) of clause-sets, the difference between the number of clauses and the number of variables. - nM(k) is the k-th "non-Mersenne" number, skipping in the sequence of natural numbers all numbers of the form 2^n - 1. We conjecture that this bound is nearly precise for minimally unsatisfiable clause-sets. As an application of the upper bound we obtain that (arbitrary!) clause-sets F with mvd(F) > nM(surp(F)) must have a non-trivial autarky (so clauses can be removed satisfiability-equivalently by an assignment satisfying some clauses and not touching the other clauses). It is open whether such an autarky can be found in polynomial time. As a future application we discuss the classification of minimally unsatisfiable clause-sets depending on the deficiency.

Affiliated with

Also associated with

No associations

Rating

On variables with few occurrences in conjunctive normal forms 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 variables with few occurrences in conjunctive normal forms, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On variables with few occurrences in conjunctive normal forms will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-486084