CAQE and QuAbS: Abstraction Based QBF Solvers
From MaRDI portal
Publication:5015608
DOI10.3233/SAT190121zbMath1484.68224MaRDI QIDQ5015608
Publication date: 9 December 2021
Published in: Journal on Satisfiability, Boolean Modeling and Computation (Search for Journal in Brave)
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
BOCoSy: Small but Powerful Symbolic Output-Feedback Control, QBFFam: a tool for generating QBF families from proof complexity, Certified DQBF solving by definition extraction
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Solving QBF with counterexample guided refinement
- A solver for QBFs in negation normal form
- Circuit-based search space pruning in QBF
- Dependency learning for QBF
- \({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property
- Resolution for quantified Boolean formulas
- On expansion and resolution in CEGAR based QBF solving
- Clausal abstraction for DQBF
- Synthesis from hyperproperties
- The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
- Expansion-based QBF solving versus Q-resolution
- Solution validation and extraction for QBF preprocessing
- DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
- Unified QBF certification and its applications
- Incremental Determinization
- Non-prenex QBF Solving Using Abstraction
- 2QBF: Challenges and Solutions
- Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
- On QBF Proofs and Preprocessing
- Incremental QBF Solving by DepQBF
- SAT-Based Synthesis Methods for Safety Specs
- Antichain-Based QBF Solving
- Fast DQBF Refutation
- A Unified Proof System for QBF Preprocessing
- QBF Encoding of Temporal Properties and QBF-Based Verification
- Encodings of Bounded Synthesis
- Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
- Nenofex: Expanding NNF for QBF Solving
- A Unified Framework for Certificate and Compilation for QBF
- A First Step Towards a Unified Proof Checker for QBF
- Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits
- Beyond CNF: A Circuit-Based QBF Solver
- D-FLAT^2: Subset Minimization in Dynamic Programming on Tree Decompositions Made Easy
- A Non-prenex, Non-clausal QBF Solver with Game-State Learning
- Integrating Dependency Schemes in Search-Based QBF Solvers
- Exploiting Circuit Representations in QBF Solving
- Skolem Function Continuation for Quantified Boolean Formulas
- Blocked Clause Elimination for QBF
- Automated Deduction – CADE-20
- Formal Methods in Computer-Aided Design
- Logic for Programming, Artificial Intelligence, and Reasoning
- Theory and Applications of Satisfiability Testing
- Understanding and extending incremental determinization for 2QBF
