No Cover Image

Conference Paper/Proceeding/Abstract 1563 views 201 downloads

On SAT Representations of XOR Constraints

Matthew Gwynne, Oliver Kullmann Orcid Logo

Language and Automata Theory and Applications, Volume: 8370

Swansea University Author: Oliver Kullmann Orcid Logo

DOI (Published version): 10.1007/978-3-319-04921-2_33

Abstract

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 = e, e in {0,1} (also called parity constraints), i.e., systems of linear equations over the two-element field . These representations are to...

Full description

Published in: Language and Automata Theory and Applications
Published: International Conference on Language and Automata Theory and Applications 2014
Online Access: http://www.cs.swan.ac.uk/~csoliver/papers.html#XOR2013LATA
URI: https://cronfa.swan.ac.uk/Record/cronfa18003
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: 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 = e, e in {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. The basic quality criterion is "arc consistency". 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 on the relation between monotone circuits and ``consistency checkers'', adapted and simplified in the underlying report , with the lower bound on monotone circuits for monotone span programs in Babai et al. 1999 . 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 . The stronger criterion is now F in 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 PC, but fails badly so already for m=2, and we show how to repair this.
Keywords: SAT, boolean functions, monotone circuits, parity constraints, arc consistency, fixed parameter tractable, lower bounds
College: Faculty of Science and Engineering
End Page: 420

Similar Items