Backdoor sets of quantified Boolean formulas

DOI10.1007/s10817-008-9114-5zbMath1191.68353OpenAlexW2039585983WikidataQ60060023 ScholiaQ60060023MaRDI QIDQ1040783

Marko Samer, Stefan Szeider

Publication date: 25 November 2009

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-008-9114-5

zbMATH Keywords

parameterized complexitybackdoor setsquantified Boolean formulasvariable dependencies

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items (26)

Quantifier reordering for QBF ⋮ Preprocessing for DQBF ⋮ Backdoors to Satisfaction ⋮ Conformant planning as a case study of incremental QBF solving ⋮ Small Resolution Proofs for QBF using Dependency Treewidth ⋮ Long-distance Q-resolution with dependency schemes ⋮ Soundness of \(\mathcal{Q}\)-resolution with dependency schemes ⋮ Never trust your solver: certification for SAT and QBF ⋮ Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search ⋮ Backdoor Sets for CSP. ⋮ Backdoors for linear temporal logic ⋮ Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers ⋮ Augmenting tractable fragments of abstract argumentation ⋮ Backdoors into heterogeneous classes of SAT and CSP ⋮ Pruning external minimality checking for answer set programs using semantic dependencies ⋮ On the Hardness of SAT with Community Structure ⋮ Q-Resolution with Generalized Axioms ⋮ Dependency Schemes for DQBF ⋮ Long Distance Q-Resolution with Dependency Schemes ⋮ Using decomposition-parameters for QBF: mind the prefix! ⋮ A Compact Representation for Syntactic Dependencies in QBFs ⋮ Backdoors to planning ⋮ Reinterpreting dependency schemes: soundness meets incompleteness in DQBF ⋮ Backdoors to tractable answer set programming ⋮ The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1 ⋮ Computational Short Cuts in Infinite Domain Constraint Satisfaction

Uses Software

• QUBOS
• Quantor

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Backdoor sets for DLL subsolvers
• An efficient fixed-parameter algorithm for 3-hitting set
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• Variable and term removal from Boolean formulae
• Generalizations of matched CNF formulas
• Resolution for quantified Boolean formulas
• Solving \#SAT using vertex covers
• Kernelization Algorithms for d-Hitting Set Problems
• Matched Formulas and Backdoor Sets
• Backdoor Sets of Quantified Boolean Formulas
• Bounded Universal Expansion for Preprocessing QBF
• Structure and Problem Hardness: Goal Asymmetry and DPLL Proofs in SAT-Based Planning
• Variable Dependencies of Quantified CSPs
• Depth-First Search and Linear Graph Algorithms
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency
• Binary Clause Reasoning in QBF
• Improved Parameterized Upper Bounds for Vertex Cover

This page was built for publication: Backdoor sets of quantified Boolean formulas