Two tractable subclasses of minimal unsatisfiable formulas

DOI10.1007/BF02878991MaRDI QIDQ1961649zbMATH OpenFDO

Authors Xishun Zhao, Decheng Ding

Publication date 28 February 2000

Published in Science in China. Series A (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BF02878991

zbMATH Keywords

polynomial timesplittingminimal unsatisfiabilitycollapsingconjunctive normal formsatisfiability testsimplification procedure

Mathematics Subject Classification ID

Classical propositional logic (03B05) Complexity of computation (including implicit computational complexity) (03D15)

Recommendations

• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• On subclasses of minimal unsatisfiable formulas
• The complexity of some subclasses of minimal unsatisfiable formulas.
• Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
• Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable

Cites work

• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem
• Solvable matrices
• The complexity of facets (and some facets of complexity)
• The complexity of facets resolved

Cited in

(25)

• On minimum representations of matched formulas
• Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
• PURL: a new polynomial-time solvable class of satisfiability
• Generating clause sequences of a CNF formula
• On the structure of some classes of minimal unsatisfiable formulas
• The complexity of variable minimal formulas
• Theory and Applications of Models of Computation
• Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets
• Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
• On variables with few occurrences in conjunctive normal forms
• On subclasses of minimal unsatisfiable formulas
• Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
• The complexity of some subclasses of minimal unsatisfiable formulas.
• Applications of minimal unsatisfiable formulas to polynomially reduction for formulas
• On the size of minimal unsatisfiable formulas
• Complexity results on minimal unsatisfiable formulas
• Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
• Minimum Witnesses for Unsatisfiable 2CNFs
• Advances in Computer Science - ASIAN 2004. Higher-Level Decision Making
• On minimal unsatisfiability and time-space trade-offs for k-DNF resolution
• scientific article; zbMATH DE number 2201270 (Why is no real title available?)
• scientific article; zbMATH DE number 1678383 (Why is no real title available?)
• Polynomial time algorithms for computing a representation for minimal unsatisfiable formulas with fixed deficiency.
• Satisfiable formulas closed under replacement
• Minimally unsatisfiable CNF formulas

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

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