An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
From MaRDI portal
Publication:1277336
DOI10.1023/A:1018924526592zbMath0913.68090OpenAlexW1525293204MaRDI QIDQ1277336
Gennady Davydov, Hans Kleine Büning, Inna Davydova
Publication date: 7 June 1999
Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1023/a:1018924526592
Related Items (28)
Local-search extraction of mUSes ⋮ Disproof of the neighborhood conjecture with implications to SAT ⋮ On Davis-Putnam reductions for minimally unsatisfiable clause-sets ⋮ The Discrepancy of Unsatisfiable Matrices and a Lower Bound for the Komlós Conjecture Constant ⋮ Irreducible subcube partitions ⋮ On the structure of some classes of minimal unsatisfiable formulas ⋮ Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets ⋮ Homomorphisms of conjunctive normal forms. ⋮ On the Computational Complexity of Read once Resolution Decidability in 2CNF Formulas ⋮ 2000 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium 2000 ⋮ On Variables with Few Occurrences in Conjunctive Normal Forms ⋮ Generalization of the Chinese remainder theorem ⋮ Finding the Hardest Formulas for Resolution ⋮ Finding read-once resolution refutations in systems of 2CNF clauses ⋮ Computational complexity of quantified Boolean formulas with fixed maximal deficiency ⋮ Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable ⋮ Computing unsatisfiable \(k\)-SAT instances with few occurrences per variable ⋮ An upper bound for the circuit complexity of existentially quantified Boolean formulas ⋮ The complexity of homomorphisms and renamings for minimal unsatisfiable formulas ⋮ Towards logical operations research -- propositional case ⋮ The Lovász Local Lemma and Satisfiability ⋮ An approach for extracting a small unsatisfiable core ⋮ On the complexity of inconsistency measurement ⋮ A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas ⋮ Using local search to find MSSes and MUSes ⋮ On subclasses of 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.
This page was built for publication: An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
