Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
From MaRDI portal
Publication:5326456
DOI10.1007/978-3-642-39071-5_9zbMath1390.68579OpenAlexW2160972885MaRDI QIDQ5326456
Florian Lonsing, Uwe Egly, Allen van Gelder
Publication date: 5 August 2013
Published in: Theory and Applications of Satisfiability Testing – SAT 2013 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-39071-5_9
Related Items (8)
Hardness Characterisations and Size-width Lower Bounds for QBF Resolution ⋮ The QBF Gallery: behind the scenes ⋮ Conformant planning as a case study of incremental QBF solving ⋮ Long-distance Q-resolution with dependency schemes ⋮ Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution ⋮ On Q-Resolution and CDCL QBF Solving ⋮ Long Distance Q-Resolution with Dependency Schemes ⋮ Knowledge representation analysis of graph mining
Uses Software
This page was built for publication: Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation