Building strategies into QBF proofs

DOI10.1007/s10817-020-09560-1OpenAlexW3028147070WikidataQ113901241 ScholiaQ113901241MaRDI QIDQ2031411

Joshua Blinkhorn, Meena Mahajan, Olaf Beyersdorff

Publication date: 9 June 2021

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

Full work available at URL: https://doi.org/10.1007/s10817-020-09560-1

zbMATH Keywords

resolutionproof complexityQBFDQBF

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

A resolution proof system for dependency stochastic Boolean satisfiability, Towards Uniform Certification in QBF, QBFFam: a tool for generating QBF families from proof complexity, Davis and Putnam meet Henkin: solving DQBF with resolution

Uses Software

• Quaffle
• Easychair
• CAQE
• HQSpre
• sKizzo
• dCAQE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Towards NP-P via proof complexity and search
• Local soundness for QBF calculi
• Polynomial-time validation of QCDCL certificates
• Dependency learning for QBF
• A resolution-style proof system for DQBF
• Resolution for quantified Boolean formulas
• Proof complexity of fragments of long-distance Q-resolution
• Clausal abstraction for DQBF
• Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
• Expansion-based QBF solving versus Q-resolution
• Conformant planning as a case study of incremental QBF solving
• Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
• Unified QBF certification and its applications
• Lower Bounds
• Lifting QBF Resolution Calculi to DQBF
• Long Distance Q-Resolution with Dependency Schemes
• Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
• Fast DQBF Refutation
• Encodings of Bounded Synthesis
• Preprocessing for DQBF
• The relative efficiency of propositional proof systems
• Handbook of Model Checking
• A Non-prenex, Non-clausal QBF Solver with Game-State Learning
• New Resolution-Based QBF Calculi and Their Proof Complexity
• Robust QBF Encodings for Sequential Circuits with Applications to Verification, Debug, and Test
• Automated Deduction – CADE-20
• Theory and Applications of Satisfiability Testing
• Dependency Quantified Horn Formulas: Models and Complexity
• Lower bounds for multiplayer noncooperative games of incomplete information