On QBF Proofs and Preprocessing

DOI10.1007/978-3-642-45221-5_32MaRDI QIDQ2870148zbMATH OpenOpenAlexFDO

Authors Mikoláš Janota, Radu Grigore, Joao Marques-Silva

Publication date 17 January 2014

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Abstract: QBFs (quantified boolean formulas), which are a superset of propositional formulas, provide a canonical representation for PSPACE problems. To overcome the inherent complexity of QBF, significant effort has been invested in developing QBF solvers as well as the underlying proof systems. At the same time, formula preprocessing is crucial for the application of QBF solvers. This paper focuses on a missing link in currently-available technology: How to obtain a certificate (e.g. proof) for a formula that had been preprocessed before it was given to a solver? The paper targets a suite of commonly-used preprocessing techniques and shows how to reconstruct certificates for them. On the negative side, the paper discusses certain limitations of the currently-used proof systems in the light of preprocessing. The presented techniques were implemented and evaluated in the state-of-the-art QBF preprocessor bloqqer.

Recommendations

• A unified proof system for QBF preprocessing
• QBF Resolution Systems and Their Proof Complexities
• Proof complexity of symbolic QBF reasoning
• Proof complexity of resolution-based QBF calculi
• scientific article; zbMATH DE number 2174393
• Provability logics with quantifiers on proofs
• On Stronger Calculi for QBFs
• A First Step Towards a Unified Proof Checker for QBF
• On propositional QBF expansions and Q-resolution

Cited in

(25)

• QBF as an alternative to Courcelle's theorem
• Shortening QBF proofs with dependency schemes
• Building strategies into QBF proofs
• Short proofs in QBF expansion
• QRATPre+: effective QBF preprocessing via strong redundancy properties
• Interpolation-based semantic gate extraction and its applications to QBF preprocessing
• Using decomposition-parameters for QBF: mind the prefix!
• Solution validation and extraction for QBF preprocessing
• Conformant planning as a case study of incremental QBF solving
• Quantified maximum satisfiability
• Incremental determinization
• On Stronger Calculi for QBFs
• An empirical study of QBF encodings: from treewidth estimation to useful preprocessing
• Fast DQBF Refutation
• A unified proof system for QBF preprocessing
• Enhancing search-based QBF solving by dynamic blocked clause elimination
• Bounded Universal Expansion for Preprocessing QBF
• Understanding Gentzen and Frege Systems for QBF
• sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• CAQE and QuAbS: Abstraction Based QBF Solvers
• scientific article; zbMATH DE number 7278086 (Why is no real title available?)
• Blocked clause elimination for QBF
• Theory and Applications of Satisfiability Testing
• True crafted formula families for benchmarking quantified satisfiability solvers

Describes a project that uses

Uses Software

• NiVER
• sQueezeBF
• Bloqqer
• Nenofex

This page was built for publication: On QBF Proofs and Preprocessing

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