scientific article; zbMATH DE number 7559123

DOI10.4230/LIPIcs.STACS.2019.14MaRDI QIDQ5090460

Meena Mahajan, Joshua Blinkhorn, Olaf Beyersdorff

Publication date: 18 July 2022

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

resolutionproof complexityQBFDQBF

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Related Items

Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution, Building strategies into QBF proofs

Cites Work

• 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
• Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
• 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
• On Unification of QBF Resolution-Based Calculi
• Propositional SAT Solving
• Encodings of Bounded Synthesis
• The relative efficiency of propositional proof systems
• A Non-prenex, Non-clausal QBF Solver with Game-State Learning
• Robust QBF Encodings for Sequential Circuits with Applications to Verification, Debug, and Test
• Theory and Applications of Satisfiability Testing
• Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item