Small Resolution Proofs for QBF using Dependency Treewidth
From MaRDI portal
Publication:3304126
DOI10.4230/LIPIcs.STACS.2018.28zbMath1487.68135arXiv1711.02120OpenAlexW2963205836MaRDI QIDQ3304126
Robert Ganian, Sebastian Ordyniak, Eduard Eiben
Publication date: 5 August 2020
Full work available at URL: https://arxiv.org/abs/1711.02120
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Complexity of proofs (03F20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Parameterized complexity, tractability and kernelization (68Q27) Computational aspects of satisfiability (68R07)
Related Items
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Quantifier reordering for QBF
- Fundamentals of parameterized complexity
- Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
- Backdoor sets of quantified Boolean formulas
- Treewidth. Computations and approximations
- Recognition algorithms for orders of small width and graphs of small Dilworth number
- Automata, logics, and infinite games. A guide to current research
- An infinite antichain of permutations
- Bounded-width QBF is PSPACE-complete
- Parametrized complexity theory.
- Computing Resolution-Path Dependencies in Linear Time ,
- Variable Independence and Resolution Paths for Quantified Boolean Formulas
- Integrating Dependency Schemes in Search-Based QBF Solvers
- A linear time algorithm for finding tree-decompositions of small treewidth
- Theory and Applications of Satisfiability Testing
- Parameterized Algorithms
- Decomposing Quantified Conjunctive (or Disjunctive) Formulas
- A Computing Procedure for Quantification Theory
- QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency
This page was built for publication: Small Resolution Proofs for QBF using Dependency Treewidth
