  The runtime performance of modern SAT solvers on random $k$-CNF formulas is
deeply connected with the 'phase-transition' phenomenon seen empirically in the
satisfiability of random $k$-CNF formulas. 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 $k$-CNF and XOR
constraints (known as $k$-CNF-XOR formulas), but the behavior of random
$k$-CNF-XOR formulas is unexplored in prior work. In this paper, we present the
first study of the satisfiability of random $k$-CNF-XOR formulas. We show
empirical evidence of a surprising phase-transition that follows a linear
trade-off between $k$-CNF and XOR constraints. Furthermore, we prove that a
phase-transition for $k$-CNF-XOR formulas exists for $k = 2$ and (when the
number of $k$-CNF constraints is small) for $k > 2$.
