Arrow Research search
Back to SAT

SAT 2017

An Adaptive Prefix-Assignment Technique for Symmetry Reduction

Conference Paper Clause Learning and Symmetry Handling Logic in Computer Science · Satisfiability

Abstract

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.

Authors

Keywords

No keywords are indexed for this paper.

Context

Venue
International Conference on Theory and Applications of Satisfiability Testing
Archive span
2003-2025
Indexed papers
824
Paper id
527803884609295605
v2026.09.13