Extending CDCL to disjunctions of parity equations

Paul Beame, Glenn Sun

Because CDCL produces proofs in the Resolution proof system, problems provably hard for Resolution are also provably hard for CDCL. Exponentially shorter proofs can sometimes be fo…