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

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

Jeffrey M. Dudek, Kuldeep S. Meel, Moshe Y. Vardi

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
Main track. Pages 600-606. https://doi.org/10.24963/ijcai.2017/84

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.
Keywords:
Constraints and Satisfiability: Constraint Satisfaction
Constraints and Satisfiability: Constraints and Satisfiability