Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable

DOI10.1016/j.jcss.2004.04.009zbMath1108.68065OpenAlexW2133544949WikidataQ60060024 ScholiaQ60060024MaRDI QIDQ1765303

Stefan Szeider

Publication date: 23 February 2005

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: http://dro.dur.ac.uk/610/1/610.pdf

zbMATH Keywords

SAT problemTree-widthExpansionMinimal unsatisfiabilityBipartite matching\(D^P\)-complete problemFixed-parameter complexity

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Graph theory (including graph drawing) in computer science (68R10) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15)

Related Items (16)

Computing Maximal Autarkies with Few and Simple Oracle Queries ⋮ Community Structure Inspired Algorithms for SAT and #SAT ⋮ Constraint Satisfaction Problems Parameterized above or below Tight Bounds: A Survey ⋮ On Davis-Putnam reductions for minimally unsatisfiable clause-sets ⋮ A new bound for 3-satisfiable MaxSat and its algorithmic application ⋮ Unnamed Item ⋮ How Many Conflicts Does It Need to Be Unsatisfiable? ⋮ An Isomorphism-Invariant Distance Function on Propositional Formulas in CNF ⋮ On the parameterized complexity of \((k,s)\)-SAT ⋮ Counting solutions to CSP using generating polynomials ⋮ New width parameters for SAT and \#SAT ⋮ Finding the Hardest Formulas for Resolution ⋮ Fixed-parameter tractability of satisfying beyond the number of variables ⋮ A new lower bound on the maximum number of satisfied clauses in Max-SAT and its algorithmic applications ⋮ A New Bound for 3-Satisfiable Maxsat and Its Algorithmic Application ⋮ A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Satisfiability, branch-width and Tseitin tautologies
• A simplified NP-complete satisfiability problem
• Graph minors. V. Excluding a planar graph
• Solving satisfiability in less than \(2^ n\) steps
• Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
• Matching theory
• The complexity of facets resolved
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• Call routing and the ratcatcher
• Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets
• Fixed-parameter complexity in AI and nonmonotonic reasoning
• Generalizations of matched CNF formulas
• 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
• Improving a fixed parameter tractability time bound for the shadow problem
• An algorithm for the class of pure implicational formulas
• Upper bounds to the clique width of graphs
• Complexity of Finding Embeddings in a k-Tree
• The Complexity of Propositional Proofs
• Theory and Applications of Satisfiability Testing
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Graph-Theoretic Concepts in Computer Science
• On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic

This page was built for publication: Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable