Small resolution proofs for QBF using dependency treewidth
From MaRDI portal
Complexity of proofs (03F20) Parameterized complexity, tractability and kernelization (68Q27) Computational aspects of satisfiability (68R07) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Abstract: In spite of the close connection between the evaluation of quantified Boolean formulas (QBF) and propositional satisfiability (SAT), tools and techniques which exploit structural properties of SAT instances are known to fail for QBF. This is especially true for the structural parameter treewidth, which has allowed the design of successful algorithms for SAT but cannot be straightforwardly applied to QBF since it does not take into account the interdependencies between quantified variables. In this work we introduce and develop dependency treewidth, a new structural parameter based on treewidth which allows the efficient solution of QBF instances. Dependency treewidth pushes the frontiers of tractability for QBF by overcoming the limitations of previously introduced variants of treewidth for QBF. We augment our results by developing algorithms for computing the decompositions that are required to use the parameter.
Recommendations
Cites work
- A Computing Procedure for Quantification Theory
- A linear time algorithm for finding tree-decompositions of small treewidth
- An empirical study of QBF encodings: from treewidth estimation to useful preprocessing
- An infinite antichain of permutations
- Automata, logics, and infinite games. A guide to current research
- Backdoor sets of quantified Boolean formulas
- Bounded-width QBF is PSPACE-complete
- Computing Resolution-Path Dependencies in Linear Time ,
- Decomposing Quantified Conjunctive (or Disjunctive) Formulas
- Fundamentals of parameterized complexity
- scientific article; zbMATH DE number 1305704 (Why is no real title available?)
- scientific article; zbMATH DE number 610968 (Why is no real title available?)
- scientific article; zbMATH DE number 1470716 (Why is no real title available?)
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- Integrating dependency schemes in search-based QBF solvers
- Parameterized algorithms
- Parametrized complexity theory.
- QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency
- Quantifier reordering for QBF
- Recognition algorithms for orders of small width and graphs of small Dilworth number
- Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
- Theory and Applications of Satisfiability Testing
- Treewidth. Computations and approximations
- Variable independence and resolution paths for quantified Boolean formulas
Cited in
(8)- Shortening QBF proofs with dependency schemes
- Using decomposition-parameters for QBF: mind the prefix!
- Strong (D)QBF dependency schemes via tautology-free resolution paths
- An empirical study of QBF encodings: from treewidth estimation to useful preprocessing
- Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
- Expansion-based QBF solving on tree decompositions
- Treewidth: A Useful Marker of Empirical Hardness in Quantified Boolean Logic Encodings
- Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
This page was built for publication: Small resolution proofs for QBF using dependency treewidth
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3304126)
