__Preprint and software__

**
Sam Buss and Oliver Kullmann
Dual Depth First Search for Binary Clause Reasoning
Preprint. March 2024, revised May 7, 2025.
**

Download preprint version.

**Abstract:**
We present a new algorithm called DualDFS which analyzes a set
of binary clauses to determine the complete backbone of
forced literals. DualDFS generalizes the failed literal algorithm
by starting with a chain *S* of implications and using
a dual depth-first search to find all literals that can
be seen to be forced true or false via a literal in *S*.
Experiments indicate that DualDFS performs comparably to,
or better than, the state-of-the-art method KB3 of
Frolysks, Yu, and Biere (2023) on sets of binary clauses
arising in CDCL solvers in SAT competitions, and that it
performs substantially better on many hard cases.
The performance of DualDFS is analyzed on some crafted
hard instances of binary clause reasoning. We give a
reduction from the problem of detecting *k*-cycles in
directed graphs to the problem of finding even a single
forced literal in binary clause reasoning. Thus a
sub-quadratic time algorithm for detecting backbone variables
in binary clauses would improve on the best known algorithms
for *k*-cycle detection. Due to known reductions from
Max-*k*-SAT to cycle detection, a near-linear time algorithm
for the 2-CNF backbone would imply O((2-δ)^{n}) time algorithms
for δ>0 for Max-*k*-SAT for all constants *k*,
resolving a major open problem.