QBF Resolution Systems and Their Proof Complexities

DOI10.1007/978-3-319-09284-3_12zbMath1423.68406OpenAlexW25993968MaRDI QIDQ3192061

Jie-Hong R. Jiang, Magdalena Widl, Valeriy Balabanov

Publication date: 26 September 2014

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-09284-3_12

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Complexity of proofs (03F20)

Related Items (32)

Quantified maximum satisfiability ⋮ The QBF Gallery: behind the scenes ⋮ Feasible Interpolation for QBF Resolution Calculi ⋮ QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving ⋮ Unnamed Item ⋮ Relating size and width in variants of Q-resolution ⋮ A simple proof of QBF hardness ⋮ Lower Bound Techniques for QBF Proof Systems ⋮ Long-distance Q-resolution with dependency schemes ⋮ Unnamed Item ⋮ Functional synthesis via input-output separation ⋮ Never trust your solver: certification for SAT and QBF ⋮ A game characterisation of tree-like Q-resolution size ⋮ Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution ⋮ Towards Uniform Certification in QBF ⋮ Lower bound techniques for QBF expansion ⋮ Lower bounds for QCDCL via formula gauge ⋮ Understanding cutting planes for QBFs ⋮ A Game Characterisation of Tree-like Q-resolution Size ⋮ Short proofs for some symmetric quantified Boolean formulas ⋮ On Stronger Calculi for QBFs ⋮ Q-Resolution with Generalized Axioms ⋮ Lifting QBF Resolution Calculi to DQBF ⋮ Long Distance Q-Resolution with Dependency Schemes ⋮ HordeQBF: A Modular and Massively Parallel QBF Solver ⋮ Unnamed Item ⋮ Reinterpreting dependency schemes: soundness meets incompleteness in DQBF ⋮ Unnamed Item ⋮ Unnamed Item ⋮ QBFFam: a tool for generating QBF families from proof complexity ⋮ Lower bounds for QCDCL via formula gauge ⋮ Proof complexity of symbolic QBF reasoning

This page was built for publication: QBF Resolution Systems and Their Proof Complexities