On subclasses of minimal unsatisfiable formulas

DOI10.1016/S0166-218X(00)00245-6zbMath0965.03016OpenAlexW1978107969WikidataQ127754366 ScholiaQ127754366MaRDI QIDQ1841884

Hans Kleine Büning

Publication date: 4 July 2001

Published in: Discrete Applied Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0166-218x(00)00245-6

zbMATH Keywords

propositional formulasminimal unsatisfiabilityconjunctive normal form

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Mechanization of proofs and logical operations (03B35) Complexity of computation (including implicit computational complexity) (03D15) Classical propositional logic (03B05) Complexity of proofs (03F20)

Related Items

Optimal length resolution refutations of difference constraint systems, Local-search extraction of mUSes, On Davis-Putnam reductions for minimally unsatisfiable clause-sets, How Many Conflicts Does It Need to Be Unsatisfiable?, Are hitting formulas hard for resolution?, Irreducible subcube partitions, On the structure of some classes of minimal unsatisfiable formulas, Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets, On Variables with Few Occurrences in Conjunctive Normal Forms, Finding the Hardest Formulas for Resolution, Fixed-parameter tractability of satisfying beyond the number of variables, Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable, The Lovász Local Lemma and Satisfiability, A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas, Using local search to find MSSes and MUSes, Polynomial time algorithms for computing a representation for minimal unsatisfiable formulas with fixed deficiency., Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.

Cites Work

• The complexity of facets (and some facets of complexity)
• The intractability of resolution
• Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
• The complexity of facets resolved
• Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Hard examples for resolution
• Unnamed Item