Certified DQBF solving by definition extraction

DOI10.1007/978-3-030-80223-3_34OpenAlexW3183677195MaRDI QIDQ2118343

Friedrich Slivovsky, Stefan Szeider, Franz-Xaver Reichl

Publication date: 22 March 2022

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

Mathematics Subject Classification ID

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

Related Items

A resolution proof system for dependency stochastic Boolean satisfiability, Mining definitions in Kissat with Kittens

Uses Software

• MiniSat
• Runsolver
• iProver
• PySAT
• HQSpre
• AIGER
• CaDiCaL
• Paracooba
• Kissat
• RAReQS
• dCAQE

Cites Work

• Unnamed Item
• Unnamed Item
• Solving QBF with counterexample guided refinement
• Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
• PySAT: a Python toolkit for prototyping with SAT oracles
• A theory of formal synthesis via inductive learning
• A resolution-style proof system for DQBF
• From DQBF to QBF by dependency elimination
• Fast interpolating BMC
• Clausal abstraction for DQBF
• Interpolation-based semantic gate extraction and its applications to QBF preprocessing
• The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
• Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
• Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
• Incremental Determinization
• Dependency Schemes for DQBF
• SAT-Based Synthesis Methods for Safety Specs
• Fast DQBF Refutation
• Encodings of Bounded Synthesis
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1
• CAQE and QuAbS: Abstraction Based QBF Solvers
• Theory and Applications of Satisfiability Testing
• On Propositional QBF Expansions and Q-Resolution
• Dependency Quantified Horn Formulas: Models and Complexity
• Lower bounds for multiplayer noncooperative games of incomplete information
• What's hard about Boolean functional synthesis?