2021/03/18 by Alexander Ivrii, Ivrii, Alexander, Ofer Strichman +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #cs.LO
paper · pdf · doi:10.48550/arxiv.2103.10267
The short version appeared in fmcad'21
openalex publication_date 2021/03/18 · arxiv created 2021/08/12 · arxiv updated 2021/08/13 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 full symmetry, namely a propositionally-consistent mapping σ between the literals, such that σ(φ) ≡ φ, where here ≡ 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.