Unsatisfiability Proofs for Parity Reasoning in SAT

increase    in code complexity.   To  increase   the  reliability  of  solvers,
unsatisfiability witnesses in the form of proofs can be emitted for standard
CDCL-style solving. However, extensions of this system need to generate
ad hoc proof fragments that must be integrated in the full proof. When this
is not possible, users must decide whether to disable proof generation or
disable extensions such as inprocessing rules.
In this talk, I introduce two translations between a proof system for parity
constraints and the state-of-the-art DRAT proof system for CNF formulae.
These translations allow the generation of unsatisfiability proofs for SAT
solvers coupled with parity reasoning modules, which was an unsolved
problem.