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 wellseparated components, similar to the behavior seen
in random CNF formulas known to be difficult for
many SAT-solving algorithms