Exploiting Isomorphic Subgraphs in SAT (Long version)

TL;DR

This paper introduces a novel approach to exploit isomorphic subgraphs in SAT problems, allowing for dynamic symmetry breaking without requiring full symmetry, thus broadening the scope of symmetry exploitation in SAT solving.

Contribution

It demonstrates that isomorphism between subgraphs, not full symmetry, suffices for adding extra clauses, and shows how to detect such subgraphs from high-level problem structures.

Findings

Isomorphism between subgraphs can be exploited for symmetry breaking.

Detecting subgraphs is feasible from high-level problem analysis.

The approach applies to problems like Van der Waerden numbers and Pythagorean triples.

Abstract

While static symmetry breaking has been explored in the SAT community for decades, only as of 2010 research has focused on exploiting the same discovered symmetry dynamically, during the run of the SAT solver, by learning extra clauses. The two methods are distinct and not compatible. The former prunes solutions, whereas the latter does not -- it only prunes areas of the search that do not have solutions, like standard conflict clauses. Both approaches, however, require what we call \emph{full symmetry}, namely a propositionally-consistent mapping $\sigma$ between the literals, such that $\sigma(\varphi) \equiv \varphi$, where here $\equiv$ means syntactic equivalence modulo clause ordering and literal ordering within the clauses. In this article we show that such full symmetry is not a necessary condition for adding extra clauses: isomorphism between possibly-overlapping subgraphs of the colored incidence graph is sufficient. While finding such subgraphs is a computationally hard problem, there are many cases in which they can be detected a priory by analyzing the high-level structure of the problem from which the CNF was derived. We demonstrate this principle with several well-known problems, including Van der Waerden numbers, bounded model checking and Boolean Pythagorean triples.