A framework for good SAT translations, with applications to CNF representations of XOR constraints

Matthew Gwynne, Oliver Kullmann

We present a general framework for good CNF-representations of boolean constraints, to be used for translating decision problems into SAT problems (i.e., deciding satisfiability fo…