On variables with few occurrences in conjunctive normal forms

DOI10.1007/978-3-642-21581-0_5MaRDI QIDQ3007672zbMATH OpenOpenAlexFDO

Authors Oliver Kullmann, Xishun Zhao

Publication date 17 June 2011

Published in Theory and Applications of Satisfiability Testing - SAT 2011 (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1010.5756

Mathematics Subject Classification ID

Classical propositional logic (03B05) Analysis of algorithms and problem complexity (68Q25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Abstract: 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.

Recommendations

• Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets
• Investigations on autark assignments
• DNF tautologies with a limited number of occurrences of every variable
• On the use of autarkies for satisfiability decision

Cites work

• A simplified NP-complete satisfiability problem
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• Green-Tao Numbers and SAT
• Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets
• Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
• On subclasses of minimal unsatisfiable formulas
• On variables with few occurrences in conjunctive normal forms
• Two tractable subclasses of minimal unsatisfiable formulas

Cited in

(3)

• Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets
• On variables with few occurrences in conjunctive normal forms
• Computing maximal autarkies with few and simple oracle queries

This page was built for publication: On variables with few occurrences in conjunctive normal forms

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3007672)