  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.
