Towards Uniform Certification in QBF

DOI10.46298/LMCS-20(1:14)2024arXiv2210.07085v4OpenAlexW3215442047MaRDI QIDQ6151563FDOQ6151563

Authors: Leroy Chew, Friedrich Slivovsky 

Publication date: 11 March 2024

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2210.07085v4

zbMATH Keywords

verificationQBFFregeproof complexityextended Fregestrategy extraction

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites Work

• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Resolution for quantified Boolean formulas
• Expansion-based QBF solving versus Q-resolution
• Unified QBF certification and its applications
• Solving QBF with counterexample guided refinement
• On Unification of QBF Resolution-Based Calculi
• Title not available (Why is that?)
• Contributions to the theory of practical quantified Boolean formula solving
• Computational Complexity
• Dependency Learning for QBF
• Long-distance resolution: proof generation and strategy extraction in search-based QBF solving
• QBF Resolution Systems and Their Proof Complexities
• The relative efficiency of propositional proof systems
• Automated testing and debugging of SAT and QBF solvers
• Integrating dependency schemes in search-based QBF solvers
• Quantified propositional calculi and fragments of bounded arithmetic
• Frege systems for quantified Boolean logic
• Efficient certified RAT verification
• On the correspondence between arithmetic theories and propositional proof systems – a survey
• Proof Complexity
• New resolution-based QBF calculi and their proof complexity
• A First Step Towards a Unified Proof Checker for QBF
• Local soundness for QBF calculi
• A little blocked literal goes a long way
• Understanding cutting planes for QBFs
• Proof Complexity Modulo the Polynomial Hierarchy: Understanding Alternation as a Source of Hardness
• Building strategies into QBF proofs
• Multi-linear strategy extraction for QBF expansion proofs via local soundness
• Solution validation and extraction for QBF preprocessing
• Hardness and optimality in QBF proof systems modulo NP
• Long-distance Q-resolution with dependency schemes

Cited In (1)

• QBF merge resolution is powerful but unnatural

This page was built for publication: Towards Uniform Certification in QBF

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6151563)