47 citations · 160 across the 17 of their papers we have counts for
17 papers
QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties
Florian Lonsing, Uwe Egly
We present version 2.0 of QRATPre+, a preprocessor for quantified Boolean formulas (QBFs) based on the QRAT proof system and its generalization QRAT+. These systems rely on strong…
Expansion-Based QBF Solving Without Recursion
Roderick Bloem, Nicolas Braud-Santoni, Vedad Hadzic +3
In recent years, expansion-based techniques have been shown to be very powerful in theory and practice for solving quantified Boolean formulas (QBF), the extension of propositional…
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property
Florian Lonsing, Uwe Egly
The QRAT (quantified resolution asymmetric tautology) proof system simulates virtually all inference rules applied in state of the art quantified Boolean formula (QBF) reasoning to…
DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL
Florian Lonsing, Uwe Egly
We present the latest major release version 6.0 of the quantified Boolean formula (QBF) solver DepQBF, which is based on QCDCL. QCDCL is an extension of the conflict-driven clause…
Evaluating QBF Solvers: Quantifier Alternations Matter
Florian Lonsing, Uwe Egly
We present an experimental study of the effects of quantifier alternations on the evaluation of quantified Boolean formula (QBF) solvers. The number of quantifier alternations in a…
Q-Resolution with Generalized Axioms
Florian Lonsing, Uwe Egly, Martina Seidl
Q-resolution is a proof system for quantified Boolean formulas (QBFs) in prenex conjunctive normal form (PCNF) which underlies search-based QBF solvers with clause and cube learnin…