Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

All reports by Author Benjamin Böhm:

TR21-131 | 10th September 2021
Olaf Beyersdorff, Benjamin Böhm

QCDCL with Cube Learning or Pure Literal Elimination - What is best?

Quantified conflict-driven clause learning (QCDCL) is one of the main approaches for solving quantified Boolean formulas (QBF). We formalise and investigate several versions of QCDCL that include cube learning and/or pure-literal elimination, and formally compare the resulting solving models via proof complexity techniques. Our results show that almost all of ... more >>>

TR20-053 | 16th April 2020
Olaf Beyersdorff, Benjamin Böhm

Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution

QBF solvers implementing the QCDCL paradigm are powerful algorithms that
successfully tackle many computationally complex applications. However, our
theoretical understanding of the strength and limitations of these QCDCL
solvers is very limited.

In this paper we suggest to formally model QCDCL solvers as proof systems. We
define different policies that ... more >>>

ISSN 1433-8092 | Imprint