No Cover Image

Conference Paper/Proceeding/Abstract 1570 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!
first_indexed 2014-05-29T10:24:51Z
last_indexed 2019-06-05T09:41:41Z
id cronfa18003
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2019-06-04T14:10:56.7708120</datestamp><bib-version>v2</bib-version><id>18003</id><entry>2014-05-27</entry><title>On SAT Representations of XOR Constraints</title><swanseaauthors><author><sid>2b410f26f9324d6b06c2b98f67362d05</sid><ORCID>0000-0003-3021-0095</ORCID><firstname>Oliver</firstname><surname>Kullmann</surname><name>Oliver Kullmann</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2014-05-27</date><deptcode>SCS</deptcode><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.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>Language and Automata Theory and Applications</journal><volume>8370</volume><paginationEnd>420</paginationEnd><publisher>International Conference on Language and Automata Theory and Applications</publisher><keywords>SAT, boolean functions, monotone circuits, parity constraints, arc consistency, fixed parameter tractable, lower bounds</keywords><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2014</publishedYear><publishedDate>2014-12-31</publishedDate><doi>10.1007/978-3-319-04921-2_33</doi><url>http://www.cs.swan.ac.uk/~csoliver/papers.html#XOR2013LATA</url><notes></notes><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2019-06-04T14:10:56.7708120</lastEdited><Created>2014-05-27T06:31:27.3088859</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Matthew</firstname><surname>Gwynne</surname><order>1</order></author><author><firstname>Oliver</firstname><surname>Kullmann</surname><orcid>0000-0003-3021-0095</orcid><order>2</order></author></authors><documents><document><filename>0018003-15052015115932.pdf</filename><originalFilename>83700409.pdf</originalFilename><uploaded>2015-05-15T11:59:32.9670000</uploaded><type>Output</type><contentLength>288158</contentLength><contentType>application/pdf</contentType><version>Author's Original</version><cronfaStatus>true</cronfaStatus><embargoDate>2015-05-15T00:00:00.0000000</embargoDate><documentNotes/><copyrightCorrect>true</copyrightCorrect></document></documents><OutputDurs/></rfc1807>
spelling 2019-06-04T14:10:56.7708120 v2 18003 2014-05-27 On SAT Representations of XOR Constraints 2b410f26f9324d6b06c2b98f67362d05 0000-0003-3021-0095 Oliver Kullmann Oliver Kullmann true false 2014-05-27 SCS 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. Conference Paper/Proceeding/Abstract Language and Automata Theory and Applications 8370 420 International Conference on Language and Automata Theory and Applications SAT, boolean functions, monotone circuits, parity constraints, arc consistency, fixed parameter tractable, lower bounds 31 12 2014 2014-12-31 10.1007/978-3-319-04921-2_33 http://www.cs.swan.ac.uk/~csoliver/papers.html#XOR2013LATA COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2019-06-04T14:10:56.7708120 2014-05-27T06:31:27.3088859 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Matthew Gwynne 1 Oliver Kullmann 0000-0003-3021-0095 2 0018003-15052015115932.pdf 83700409.pdf 2015-05-15T11:59:32.9670000 Output 288158 application/pdf Author's Original true 2015-05-15T00:00:00.0000000 true
title On SAT Representations of XOR Constraints
spellingShingle On SAT Representations of XOR Constraints
Oliver Kullmann
title_short On SAT Representations of XOR Constraints
title_full On SAT Representations of XOR Constraints
title_fullStr On SAT Representations of XOR Constraints
title_full_unstemmed On SAT Representations of XOR Constraints
title_sort On SAT Representations of XOR Constraints
author_id_str_mv 2b410f26f9324d6b06c2b98f67362d05
author_id_fullname_str_mv 2b410f26f9324d6b06c2b98f67362d05_***_Oliver Kullmann
author Oliver Kullmann
author2 Matthew Gwynne
Oliver Kullmann
format Conference Paper/Proceeding/Abstract
container_title Language and Automata Theory and Applications
container_volume 8370
publishDate 2014
institution Swansea University
doi_str_mv 10.1007/978-3-319-04921-2_33
publisher International Conference on Language and Automata Theory and Applications
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
url http://www.cs.swan.ac.uk/~csoliver/papers.html#XOR2013LATA
document_store_str 1
active_str 0
description 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.
published_date 2014-12-31T03:20:59Z
_version_ 1763750612356300800
score 11.037056

Similar Items