Graduate and Postdoctoral Studies
Random CNF-XOR Formulas
Tuesday, April 18, 2017
to 11:00 AM
1049 Duncan Hall
The Boolean-Satisfaction Problem (SAT) is fundamental in many diverse areas such as artificial intelligence, formal verification, and biology. A large body of work explains the runtime performance of modern SAT solvers through analysis of random k-CNF formulas. Recent universal-hashing based approaches to the problems of sampling and counting crucially depend on the runtime performance of specialized SAT solvers on formulas expressed as the conjunction of both k-CNF constraints and variable-width XOR constraints (known as CNF-XOR formulas), but random CNF-XOR formulas are unexplored in prior work.
In this work, we present the first study of random CNF-XOR formulas. We show empirical evidence of a surprising phase-transition in the satisfiability of random CNF-XOR formulas that follows a linear trade-off between k-CNF and XOR constraints. Moreover, we prove that a phase-transition in the satisfiability of random CNF-XOR formulas exists for k=2 and (when the number of k-CNF constraints is small) for k>2. 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. Finally, we prove that the solution space of random CNF-XOR formulas 'shatters' at all nonzero XOR-clause densities into well-separated components.