Abstract
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 satisfiability of CARDXOR formulas is a fundamental problem with 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