Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > KEYWORD > SAT SOLVING:
Reports tagged with SAT solving:
TR04-016 | 3rd March 2004
Michael Alekhnovich, Eli Ben-Sasson

Linear Upper Bounds for Random Walk on Small Density Random 3CNFs

We analyze the efficiency of the random walk algorithm on random 3CNF instances, and prove em linear upper bounds on the running time
of this algorithm for small clause density, less than 1.63. Our upper bound matches the observed running time to within a multiplicative factor. This is the ... 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 >>>


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

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

Revisions: 1

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 >>>


TR23-051 | 18th April 2023
Benjamin Böhm, Olaf Beyersdorff

QCDCL vs QBF Resolution: Further Insights

We continue the investigation on the relations of QCDCL and QBF resolution systems. In particular, we introduce QCDCL versions that tightly characterise QU-Resolution and (a slight variant of) long-distance Q-Resolution. We show that most QCDCL variants - parameterised by different policies for decisions, unit propagations and reductions -- lead to ... more >>>




ISSN 1433-8092 | Imprint