On SAT Representations of XOR Constraints

Abstract

We consider the problem of finding good representations, via boolean conjunctive normal forms F (clause-sets), of systems S of XOR-constraints x ₁ ⊕ … ⊕ x _n  = ε, ε ∈ {0,1} (also called parity constraints), i.e., systems of linear equations over the two-element field. These representations are to be used as parts of SAT problems F ^* ⊃ F, such that F ^* has “good” properties for SAT solving. The basic quality criterion is “arc consistency”, that is, for every partial assignment φ to the variables of S, all assignments x _i  = ε forced by φ are determined by unit-clause propagation on the result φ* F of the application. We show there is no arc-consistent representation of polynomial size for arbitrary S. The proof combines the basic method by Bessiere et al. 2009 ([2]) on the relation between monotone circuits and “consistency checkers”, adapted and simplified in the underlying report Gwynne et al. [10], with the lower bound on monotone circuits for monotone span programs in Babai et al. 1999 [1]. On the other side, our basic positive result is that computing an arc-consistent representation is fixed-parameter tractable in the number m of equations of S. To obtain stronger representations, instead of mere arc-consistency we consider the class ${\mathcal{PC}}$ of propagation-complete clause-sets, as introduced in Bordeaux et al. 2012 [4]. The stronger criterion is now $F \in{\mathcal{PC}}$, which requires for all partial assignments, possibly involving also the auxiliary (new) variables in F, that forced assignments can be determined by unit-clause propagation. We analyse the basic translation, which for m = 1 lies in ${\mathcal{PC}}$, but fails badly so already for m = 2, and we show how to repair this.