On subclasses of minimal unsatisfiable formulas

DOI10.1016/S0166-218X(00)00245-6MaRDI QIDQ1841884zbMATH OpenOpenAlexWikidataFDO

Authors 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

conjunctive normal formminimal unsatisfiabilitypropositional formulas

Mathematics Subject Classification ID

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

Recommendations

• Two tractable subclasses of minimal unsatisfiable formulas
• The complexity of some subclasses of minimal unsatisfiable formulas.
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• Complexity results on minimal unsatisfiable formulas
• On the structure of some classes of minimal unsatisfiable formulas

Cites work

• 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
• Hard examples for resolution
• scientific article; zbMATH DE number 1342212 (Why is no real title available?)
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
• Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem
• The complexity of facets (and some facets of complexity)
• The complexity of facets resolved
• The intractability of resolution

Cited in

(26)

• A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas
• Using local search to find MSSes and MUSes
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• On the structure of some classes of minimal unsatisfiable formulas
• Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets
• Minimal unsatisfiability and minimal strongly connected digraphs
• Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
• The complexity of homomorphisms and renamings for minimal unsatisfiable formulas
• 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.
• Two tractable subclasses of minimal unsatisfiable formulas
• Local-search extraction of mUSes
• On variables with few occurrences in conjunctive normal forms
• Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
• Complexity results on minimal unsatisfiable formulas
• How Many Conflicts Does It Need to Be Unsatisfiable?
• The Lovász Local Lemma and Satisfiability
• Finding the hardest formulas for resolution
• Fixed-parameter tractability of satisfying beyond the number of variables
• The complexity of some subclasses of minimal unsatisfiable formulas.
• Advances in Computer Science - ASIAN 2004. Higher-Level Decision Making
• Theory and Applications of Models of Computation
• Classes of propositional UMU formulas and their extensions to minimal unsatisfiable formulas
• Are hitting formulas hard for resolution?
• Irreducible subcube partitions
• Optimal length resolution refutations of difference constraint systems

This page was built for publication: On subclasses of minimal unsatisfiable formulas

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