A Proofs

The proof directly follows from Theorem 3.2 from V ergari et al. [75]. Note that O ( |q ||c|) is a loose upperbound and the size of r is in practice smaller [75]. Analogously, the second statement of Theorem 3.1 follows from Proposition A.1 and by recalling For our experiments we use standard compilation tools to obtain a constraint circuit starting from a propositional logical formula in conjunctive normal form. We now illustrate step-by-step one example of such a compilation for a simple logical formula. Deterministic sum units represent disjoint solutions to the logical formula, meaning there exists distinct assignments, characterized by the children, that satisfy the logical constraint e.g.