On the structure of some classes of minimal unsatisfiable formulas

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

Hans Kleine Büning, Zhao, Xishun

Publication date: 15 September 2003

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

Full work available at URL: https://doi.org/10.1016/s0166-218x(02)00405-5

zbMATH Keywords

Marginal formulasMaximal formulasMinimal unsatisfiabilityPropositional formulasSplitting of formulas

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25)

Related Items (7)

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

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

This page was built for publication: On the structure of some classes of minimal unsatisfiable formulas