Fast DQBF Refutation

DOI10.1007/978-3-319-09284-3_19MaRDI QIDQ3192073zbMATH OpenOpenAlexFDO

Authors Bernd Finkbeiner, Leander Tentrup

Publication date 26 September 2014

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-09284-3_19

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• A resolution-style proof system for DQBF
• The equivalences of refutational QRAT
• Short proofs in QBF expansion
• scientific article; zbMATH DE number 1670747
• Logical Approaches to Computational Barriers
• Lifting QBF resolution calculi to DQBF
• scientific article; zbMATH DE number 3928966
• Proving as fast as computing: succinct arguments with constant prover overhead
• Compressing propositional refutations
• On QBF Proofs and Preprocessing

Cited in

(14)

• Henkin quantifiers and Boolean formulae
• Dependency schemes for DQBF
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• Certified DQBF solving by definition extraction
• DQBDD: an efficient BDD-based DQBF solver
• Lifting QBF resolution calculi to DQBF
• Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
• Building strategies into QBF proofs
• Clausal abstraction for DQBF
• Solving dependency quantified Boolean formulas using quantifier localization
• Incremental determinization
• Preprocessing for DQBF
• CAQE and QuAbS: Abstraction Based QBF Solvers
• Partial quantifier elimination and property generation

This page was built for publication: Fast DQBF Refutation

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