Polynomial time algorithms for computing a representation for minimal unsatisfiable formulas with fixed deficiency.

DOI10.1016/S0020-0190(02)00267-3zbMath1042.68105OpenAlexW2090627305MaRDI QIDQ1853126

Hans Kleine Büning, Zhao, Xishun

Publication date: 21 January 2003

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0020-0190(02)00267-3

zbMATH Keywords

AlgorithmsPropositional LogicMinimal unsatisfiabilityFormula homomorphism

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Classical propositional logic (03B05)

Related Items

The complexity of homomorphisms and renamings for minimal unsatisfiable formulas ⋮ Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems

Cites Work

• Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• Homomorphisms of conjunctive normal forms.
• On subclasses of minimal unsatisfiable formulas
• Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
• A perspective on certain polynomial-time solvable classes of satisfiability