Two tractable subclasses of minimal unsatisfiable formulas

DOI10.1007/BF02878991zbMath0937.03009MaRDI QIDQ1961649

Ding, Decheng, Zhao, Xishun

Publication date: 28 February 2000

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

zbMATH Keywords

splittingpolynomial timecollapsingminimal unsatisfiabilityconjunctive normal formsatisfiability testsimplification procedure

Mathematics Subject Classification ID

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

Related Items (5)

On Davis-Putnam reductions for minimally unsatisfiable clause-sets ⋮ Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets ⋮ On Variables with Few Occurrences in Conjunctive Normal Forms ⋮ The complexity of variable minimal formulas ⋮ Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.

Cites Work

• The complexity of facets (and some facets of complexity)
• 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
• Solvable matrices
• Linear-time algorithms for testing the satisfiability of propositional horn formulae

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