SAT Preprocessors and Symmetry

TL;DR

This paper introduces a symmetry-aware SAT preprocessor that enhances symmetry detection and breaking, reduces detection time, and uncovers hidden symmetries, improving the efficiency of solving symmetric SAT instances.

Contribution

It develops a theoretical framework linking SAT preprocessing and symmetry detection, and creates a preprocessor that preserves and reveals symmetries for better exploitation.

Findings

Preprocessing can remove or hide symmetries in SAT formulas.

The symmetry-aware preprocessor reduces symmetry detection time.

The preprocessor uncovers hidden symmetries not visible in original formulas.

Abstract

Exploitation of symmetries is an indispensable approach to solve certain classes of difficult SAT instances. Numerous techniques for the use of symmetry in SAT have evolved over the past few decades. But no matter how symmetries are used precisely, they have to be detected first. We investigate how to detect more symmetry, faster. The initial idea is to reap the benefits of SAT preprocessing for symmetry detection. As it turns out, applying an off-the-shelf preprocessor before handling symmetry runs into problems: the preprocessor can haphazardly remove symmetry from formulas, severely impeding symmetry exploitation. Our main contribution is a theoretical framework that captures the relationship of SAT preprocessing techniques and symmetry. Based on this, we create a symmetry-aware preprocessor that can be applied safely before handling symmetry. We then demonstrate that applying the preprocessor does not only substantially decrease symmetry detection and breaking times, but also uncovers hidden symmetry not detectable in the original instances. Overall, we depart the conventional view of treating symmetry detection as a black-box, presenting a new application-specific approach to symmetry detection in SAT.