Abstract
This paper presents a technique for symmetry reduction that adaptively assigns a prefix of variables in a system of constraints so that the generated prefix-assignments are pairwise nonisomorphic under the action of the symmetry group of the system. The technique is based on McKay’s canonical extension framework [J. Algorithms 26 (1998), no. 2, 306–324]. Among key features of the technique are (i) adaptability—the prefix sequence can be user-prescribed and truncated for compatibility with the group of symmetries; (ii) parallelisability—prefix-assignments can be processed in parallel independently of each other; (iii) versatility—the method is applicable whenever the group of symmetries can be concisely represented as the automorphism group of a vertex-colored graph; and (iv) implementability—the method can be implemented relying on a canonical labeling map for vertex-colored graphs as the only nontrivial subroutine. To demonstrate the tentative practical applicability of our technique we have prepared a preliminary implementation and report on a limited set of experiments that demonstrate ability to reduce symmetry on hard instances.
Original language | English |
---|---|
Title of host publication | Theory and Applications of Satisfiability Testing – SAT 2017 - 20th International Conference, Proceedings |
Publisher | Springer |
Pages | 101-118 |
Number of pages | 18 |
ISBN (Print) | 9783319662626 |
DOIs | |
Publication status | Published - 2017 |
MoE publication type | A4 Conference publication |
Event | International Conference on Theory and Applications of Satisfiability Testing - Melbourne, Australia Duration: 28 Aug 2017 → 1 Sept 2017 Conference number: 20 |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Publisher | Springer |
Volume | 10491 LNCS |
ISSN (Print) | 03029743 |
ISSN (Electronic) | 16113349 |
Conference
Conference | International Conference on Theory and Applications of Satisfiability Testing |
---|---|
Abbreviated title | SAT |
Country/Territory | Australia |
City | Melbourne |
Period | 28/08/2017 → 01/09/2017 |