On SAT Representations of XOR Constraints

We consider the problem of finding good representations, via boolean conjunctive normal forms

F

(clause-sets), of systems

S

of XOR-constraints

x

1

 ⊕ … ⊕ 

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.