On variables with few occurrences in conjunctive normal forms

Abstract

We consider the question of the existence of variables with few occurrences in boolean conjunctive normal forms (clause-sets). Let μvd(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 μvd(F) ≤ nM(σ(F)) ≤ σ(F) + 1 + log2(σ(F)) for lean clause-sets F in dependency on the surplus σ(F). Lean clause-sets, defined as having no non-trivial autarkies, generalise minimally unsatisfiable clause-sets. For the surplus we have σ(F) ≤ δ(F) = c(F) - n(F), using the deficiency δ(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 2n - 1. As an application of the upper bound we obtain that clause-sets F violating μvd(F) ≤ nM(σ(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. © 2011 Springer-Verlag.