DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL

DOI10.1007/978-3-319-63046-5_23MaRDI QIDQ2405263zbMATH OpenOpenAlexFDO

Authors Florian Lonsing, Uwe Egly

Publication date 22 September 2017

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

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Abstract: We present the latest major release version 6.0 of the quantified Boolean formula (QBF) solver DepQBF, which is based on QCDCL. QCDCL is an extension of the conflict-driven clause learning (CDCL) paradigm implemented in state of the art propositional satisfiability (SAT) solvers. The Q-resolution calculus (QRES) is a QBF proof system which underlies QCDCL. QCDCL solvers can produce QRES proofs of QBFs in prenex conjunctive normal form (PCNF) as a byproduct of the solving process. In contrast to traditional QCDCL based on QRES, DepQBF 6.0 implements a variant of QCDCL which is based on a generalization of QRES. This generalization is due to a set of additional axioms and leaves the original Q-resolution rules unchanged. The generalization of QRES enables QCDCL to potentially produce exponentially shorter proofs than the traditional variant. We present an overview of the features implemented in DepQBF and report on experimental results which demonstrate the effectiveness of generalized QRES in QCDCL.

Recommendations

• Integrating dependency schemes in search-based QBF solvers
• Incremental QBF solving by DepQBF
• The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
• Efficiently representing existential dependency sets for expansion-based QBF solvers
• Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
• Formal Methods in Computer-Aided Design
• The seventh QBF solvers evaluation (QBFEVAL'10)
• From DQBF to QBF by dependency elimination
• Enhancing search-based QBF solving by dynamic blocked clause elimination

Cited in

(41)

• Relating size and width in variants of Q-resolution
• Polynomial-time validation of QCDCL certificates
• Dual proof generation for quantified Boolean formulas with a BDD-based solver
• Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
• QBFFam: a tool for generating QBF families from proof complexity
• Lower bounds for QCDCL via formula gauge
• Advanced algorithms for abstract dialectical frameworks based on complexity analysis of subclasses and SAT solving
• The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
• Computing smallest MUSes of quantified Boolean formulas
• On Q-resolution and CDCL QBF solving
• Q-resolution with generalized axioms
• HordeQBF: a modular and massively parallel QBF solver
• Incremental QBF solving by DepQBF
• \(\mathsf{MPIDepQBF}\): towards parallel QBF solving without knowledge sharing
• Integrating dependency schemes in search-based QBF solvers
• Solving Advanced Argumentation Problems with Answer Set Programming
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• GhostQ. System description
• CAQE and QuAbS: Abstraction Based QBF Solvers
• Planning with Incomplete Information in Quantified Answer Set Programming
• Lower bounds for QCDCL via formula gauge
• OuterCount: a first-level solution-counter for quantified Boolean formulas
• True crafted formula families for benchmarking quantified satisfiability solvers
• Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
• Tackling universal properties of minimal trap spaces of Boolean networks
• Quantified Boolean Solving for Achievement Games
• Making \(\mathsf{IP}=\mathsf{PSPACE}\) practical: efficient interactive protocols for BDD algorithms
• Transforming quantified Boolean formulas using biclique covers
• Dependency schemes in CDCL-based QBF solving: a proof-theoretic study
• Feature necessity and relevancy in machine learning explanations
• Models and counter-models of quantified Boolean formulas (invited talk)
• Refinement-based enumeration of QBF solutions
• Encoding action reversibility in planning using quantified ASP and Bule
• Runtime vs. extracted proof size: an exponential gap for CDCL on QBFs
• Strong (D)QBF dependency schemes via implication-free resolution paths
• QCDCL with cube learning or pure literal elimination -- what is best?
• Counting QBF solutions at level two
• Quantifier shifting for quantified Boolean formulas revisited
• Understanding the relative strength of QBF CDCL solvers and QBF resolution
• On the interplay of cube learning and dependency schemes in QCDCL proof systems
• Proof complexity of modal resolution

Describes a project that uses

Uses Software

• DepQBF

This page was built for publication: DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL

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