Enhancing search-based QBF solving by dynamic blocked clause elimination
DOI10.1007/978-3-662-48899-7_29zbMATH Open1471.68251OpenAlexW2294843272MaRDI QIDQ3460072FDOQ3460072
Authors: Florian Lonsing, Fahiem Bacchus, Armin Biere, Uwe Egly, Martina Seidl
Publication date: 12 January 2016
Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-662-48899-7_29
Recommendations
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Logic in computer science (03B70)
Cited In (18)
- Local redundancy in SAT: generalizations of blocked clauses
- Solving QBF with counterexample guided refinement
- Conformant planning as a case study of incremental QBF solving
- The power of non-ground rules in Answer Set Programming
- Interpolation-based semantic gate extraction and its applications to QBF preprocessing
- The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
- DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
- A game characterisation of tree-like Q-resolution size
- Super-blocked clauses
- Truth assignments as conditional autarkies
- CAQE and QuAbS: Abstraction Based QBF Solvers
- Solution validation and extraction for QBF preprocessing
- Long-distance Q-resolution with dependency schemes
- HordeQBF: a modular and massively parallel QBF solver
- Blocked clause elimination for QBF
- Dynamically Partitioning for Solving QBF
- Q-resolution with generalized axioms
- Long distance Q-resolution with dependency schemes
Uses Software
This page was built for publication: Enhancing search-based QBF solving by dynamic blocked clause elimination
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3460072)