Non-prenex QBF Solving Using Abstraction

DOI10.1007/978-3-319-40970-2_24zbMath1475.68224OpenAlexW2463075119MaRDI QIDQ2818029

Leander Tentrup

Publication date: 5 September 2016

Published in: Theory and Applications of Satisfiability Testing – SAT 2016 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-40970-2_24

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Computational aspects of satisfiability (68R07)

Related Items

Progress in certifying hardware model checking results, Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification, Unnamed Item, Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems, Non-prenex QBF Solving Using Abstraction, Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations, The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17), CAQE and QuAbS: Abstraction Based QBF Solvers, Proof complexity of symbolic QBF reasoning

Uses Software

• PicoSAT
• Nenofex
• CirQit2
• QMiraXT
• MPIDepQBF
• Acacia+
• CAQE
• RAReQS
• QESTO

Cites Work

• Unnamed Item
• A solver for QBFs in negation normal form
• Non-prenex QBF Solving Using Abstraction
• Solving QBF with Counterexample Guided Refinement
• MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing
• QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving
• Nenofex: Expanding NNF for QBF Solving
• Bounded Synthesis
• Beyond CNF: A Circuit-Based QBF Solver
• A Non-prenex, Non-clausal QBF Solver with Game-State Learning