On the structure of some classes of minimal unsatisfiable formulas

DOI10.1016/S0166-218X(02)00405-5zbMath1029.68078MaRDI QIDQ1408380

Hans Kleine Büning, Zhao, Xishun

Publication date: 15 September 2003

Published in: Discrete Applied Mathematics (Search for Journal in Brave)

zbMATH Keywords

Marginal formulas; Maximal formulas; Minimal unsatisfiability; Propositional formulas; Splitting of formulas

Mathematics Subject Classification ID

68Q25: Analysis of algorithms and problem complexity

Related Items

Disproof of the neighborhood conjecture with implications to SAT, Computing unsatisfiable \(k\)-SAT instances with few occurrences per variable, Finding read-once resolution refutations in systems of 2CNF clauses, On the Computational Complexity of Read once Resolution Decidability in 2CNF Formulas, Community Structure Inspired Algorithms for SAT and #SAT

Cites Work

• The intractability of resolution
• Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
• The complexity of facets resolved
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• On subclasses of minimal unsatisfiable formulas
• Many hard examples for resolution
• Hard examples for resolution
• CNF-Satisfiability Test by Counting and Polynomial Average Time
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving