The Hard Problems Are Almost Everywhere For Random CNF-XOR Formulas

TL;DR

This paper investigates the computational difficulty of solving random CNF-XOR formulas, showing both empirical exponential scaling of SAT solvers and theoretical solution space shattering, highlighting the complexity of these formulas.

Contribution

It provides the first empirical analysis of SAT solver performance on CNF-XOR formulas and proves the solution space shattering phenomenon at all nonzero XOR densities.

Findings

SAT solvers scale exponentially on random CNF-XOR formulas

The solution space shatters at all nonzero XOR densities

Peak difficulty occurs near the phase transition

Abstract

Recent universal-hashing based approaches to sampling and counting crucially depend on the runtime performance of SAT solvers on formulas expressed as the conjunction of both CNF constraints and variable-width XOR constraints (known as CNF-XOR formulas). In this paper, we present the first study of the runtime behavior of SAT solvers equipped with XOR-reasoning techniques on random CNF-XOR formulas. We empirically demonstrate that a state-of-the-art SAT solver scales exponentially on random CNF-XOR formulas across a wide range of XOR-clause densities, peaking around the empirical phase-transition location. On the theoretical front, we prove that the solution space of a random CNF-XOR formula 'shatters' at all nonzero XOR-clause densities into well-separated components, similar to the behavior seen in random CNF formulas known to be difficult for many SAT algorithms.