DQBDD: an efficient BDD-based DQBF solver

DOI10.1007/978-3-030-80223-3_36MaRDI QIDQ2118347zbMATH OpenOpenAlexFDO

Authors Juraj Síč, Jan Strejček

Publication date 22 March 2022

Full work available at URL https://doi.org/10.1007/978-3-030-80223-3_36

Mathematics Subject Classification ID

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

Cites work

• scientific article; zbMATH DE number 5510691 (Why is no real title available?)
• scientific article; zbMATH DE number 5539366 (Why is no real title available?)
• Clausal abstraction for DQBF
• Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications
• Fast DQBF Refutation
• From DQBF to QBF by dependency elimination
• Graph-Based Algorithms for Boolean Function Manipulation
• Interpolation-based semantic gate extraction and its applications to QBF preprocessing
• Lower bounds for multiplayer noncooperative games of incomplete information
• On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
• SAT-Based Synthesis Methods for Safety Specs
• Solving quantified bit-vector formulas using binary decision diagrams
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)

Cited in

(1)

• Solving dependency quantified Boolean formulas using quantifier localization

Describes a project that uses

Uses Software

• CUDD
• PicoSAT
• iProver
• antom
• HQSpre
• Q3B
• dCAQE

This page was built for publication: DQBDD: an efficient BDD-based DQBF solver

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