Preprint and software

    Sam Buss and Oliver Kullmann
    Dual Depth First Search for Binary Clause Reasoning
    Preprint. March 2024

    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-δ)ⁿ) time algorithms for δ>0 for Max-k-SAT for all constants k, resolving a major open problem.