Techniques for solving SAT with known symmetry

Suppose you have a boolean equation $E$ in $n$ variables in CNF form. In addition you have a symmetry group $G \subset S_n$ which you know if $v$ is a vector of boolean values which satisfies $E$ then for all $\pi \in G$ we have $\pi(v)$ is also a solution.

Is there any way to modify DPLL to use this information?

• For each clause $C_i(v)$ add $C_i(\sigma(v))$ to your SAT problem in CNF. – reuns Mar 20 '17 at 1:13

If I understood you well, in case there is at least one valid assignment, we can find other valid assignment where the first $k$ variables are true, and the last $n - k$ variables are false, being $k$ the number of truth variables in your first assignments. Using this fact, you only need to check $n+1$ assignments.
• If you are in a simmetry group it means that if you have a valid assignment, the only that matters here is the count of variables in true and in false, i.e. v = (0, 1, 1, 0, 1) there is a permutation $\pi$ wich satisfy: $\pi(v) = (1, 1, 1, 0, 0)$ and is also a valid assignment. There are only $n+1$ assignments where the true values are at the prefix. – Marcelo Fornet Mar 20 '17 at 1:09
• Ok I see, what you say is correct only if $G = S_n$, in which case as you showed there are only $n+1$ assignment to try. – reuns Mar 20 '17 at 1:15
• But here we only know there is a subset of $S_n$ (well a subgroup) such that $v$ is a solution iff $\sigma(v)$ is a solution – reuns Mar 20 '17 at 1:15