On SAT representations of XOR constraints
Matthew Gwynne, Oliver Kullmann · 2013
Abstract. We consider the problem of finding good representations, via boolean conjunctive normal forms F (clause-sets), of systems S of XOR-constraints x1 ⊕ · · · ⊕ xn = ε, ε ∈ {0, 1} (also called parity constraints), i.e., systems of linear equations over the two-element field. These repre-sentations 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 xi = ε 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 PC of propagation-complete clause-sets, as introduced in Bordeaux et al. 2012 [4]. The stronger criterion is now F ∈ PC, which requires for all partial assignments, possibly involv-ing also the auxiliary (new) variables in F, that forced assignments can be determined by unit-clause propagation. We analyse the basic trans-lation, which for m = 1 lies in PC, but fails badly so already for m = 2, and we show how to repair this.