Efficiently representing existential dependency sets for expansion-based QBF solvers

DOI10.1016/J.ENTCS.2009.08.029MaRDI QIDQ5170277zbMATH OpenOpenAlexFDO

Authors Florian Lonsing, Armin Biere

Publication date 23 July 2014

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2009.08.029

zbMATH Keywords

dependenciesexpansionQBFquantified Boolean formulae

Mathematics Subject Classification ID

Logic in computer science (03B70)

Recommendations

• A Compact Representation for Syntactic Dependencies in QBFs
• Dependency learning for QBF
• Integrating dependency schemes in search-based QBF solvers
• Dependency Learning for QBF
• Computing Resolution-Path Dependencies in Linear Time ,

Cites work

• A Compact Representation for Syntactic Dependencies in QBFs
• A machine program for theorem-proving
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Automated Deduction – CADE-20
• Backdoor sets of quantified Boolean formulas
• Backjumping for quantified Boolean logic satisfiability
• Bounded Universal Expansion for Preprocessing QBF
• Compressing BMC encodings with QBF
• Efficiency of a Good But Not Linear Set Union Algorithm
• scientific article; zbMATH DE number 5542982 (Why is no real title available?)
• scientific article; zbMATH DE number 3560737 (Why is no real title available?)
• scientific article; zbMATH DE number 1979551 (Why is no real title available?)
• Nenofex: Expanding NNF for QBF Solving
• Resolution for quantified Boolean formulas
• The Transitive Reduction of a Directed Graph
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and applications of satisfiability testing. 8th international conference, SAT 2005, St Andrews, UK, June 19--23, 2005. Proceedings.

Cited in

(7)

• DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
• Dependency schemes for DQBF
• Preprocessing for DQBF
• A Compact Representation for Syntactic Dependencies in QBFs
• Quantifier elimination by dependency sequents
• Dependency Learning for QBF
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation

Describes a project that uses

Uses Software

• sKizzo
• Nenofex
• QUBOS
• Quaffle

This page was built for publication: Efficiently representing existential dependency sets for expansion-based QBF solvers

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