Backdoors to q-Horn

DOI10.1007/s00453-014-9958-5zbMath1336.68126OpenAlexW2162347299MaRDI QIDQ261394

Sebastian Ordyniak, M. S. Ramanujan, Stefan Szeider, Serge Gaspers, Saket Saurabh

Publication date: 23 March 2016

Published in: Algorithmica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00453-014-9958-5

zbMATH Keywords

algorithmsdata structuressatisfiabilityfixed-parameter tractabilitybackdoor sets

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Classical propositional logic (03B05) Data structures (68P05)

Related Items

SAT backdoors: depth beats size ⋮ Faster graph bipartization ⋮ Backdoors to planning

Uses Software

• Velev SAT Benchmarks

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Satisfiability, branch-width and Tseitin tautologies
• Almost 2-SAT is fixed-parameter tractable
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• Recognition of \(q\)-Horn formulae in linear time
• Polynomial-time inference of all valid implications for Horn and related formulae
• Variable and term removal from Boolean formulae
• Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
• Algorithms for propositional model counting
• Counting truth assignments of formulas of bounded tree-width or clique-width
• Parametrized complexity theory.
• Backdoors to Satisfaction
• Maximal Flow Through a Network
• Parameterized Approximation Problems
• Renaming a Set of Clauses as a Horn Set
• Linear Time Parameterized Algorithms via Skew-Symmetric Multicuts
• The complexity of satisfiability problems
• The complexity of theorem-proving procedures