Phase Transition Behavior of Cardinality and XOR Constraints
  The runtime performance of modern SAT solvers is deeply connected to the
phase transition behavior of CNF formulas. While CNF solving has witnessed
significant runtime improvement over the past two decades, the same does not
hold for several other classes such as the conjunction of cardinality and XOR
constraints, denoted as CARD-XOR formulas. The problem of determining the
satisfiability of CARD-XOR formulas is a fundamental problem with a wide
variety of applications ranging from discrete integration in the field of
artificial intelligence to maximum likelihood decoding in coding theory. The
runtime behavior of random CARD-XOR formulas is unexplored in prior work. In
this paper, we present the first rigorous empirical study to characterize the
runtime behavior of 1-CARD-XOR formulas. We show empirical evidence of a
surprising phase-transition that follows a non-linear tradeoff between CARD and
XOR constraints.
