2014/06/28 by Matthew Gwynne, Gwynne, Matthew, Oliver Kullmann +1
Computer Science · Engineering · #Computational Complexity (cs.CC) #Constraint Satisfaction and Optimization #F.4.1 #FOS: Computer and information sciences #Formal Methods in Verification #I.2.4 #Scheduling and Optimization Algorithms
paper · pdf · doi:10.48550/arxiv.1406.7398
openalex publication_date 2014/06/28 · openalex created_date 2022/10/02 · openalex updated_date 2026/07/28
We present a general framework for good CNF-representations of boolean\nconstraints, to be used for translating decision problems into SAT problems\n(i.e., deciding satisfiability for conjunctive normal forms). We apply it to\nthe representation of systems of XOR-constraints, also known as systems of\nlinear equations over the two-element field, or systems of parity constraints.\n The general framework defines the notion of "representation", and provides\nseveral methods to measure the quality of the representation by the complexity\n("hardness") needed for making implicit "knowledge" of the representation\nexplicit (to a SAT-solving mechanism). We obtain general upper and lower\nbounds.\n Applied to systems of XOR-constraints, we show a super-polynomial lower bound\non "good" representations under very general circumstances. A corresponding\nupper bound shows fixed-parameter tractability in the number of constraints.\n The measurement underlying this upper bound ignores the auxiliary variables\nneeded for shorter representations of XOR-constraints. Improved upper bounds\n(for special cases) take them into account, and a rich picture begins to\nemerge, under the various hardness measurements.\n