0
$\begingroup$

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?

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

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.

$\endgroup$
  • $\begingroup$ I don't see what mean. $\endgroup$ – reuns Mar 20 '17 at 1:05
  • $\begingroup$ 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. $\endgroup$ – Marcelo Fornet Mar 20 '17 at 1:09
  • $\begingroup$ 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. $\endgroup$ – reuns Mar 20 '17 at 1:15
  • $\begingroup$ 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 $\endgroup$ – reuns Mar 20 '17 at 1:15
  • $\begingroup$ Ok, I understood, you are totally right. $\endgroup$ – Marcelo Fornet Mar 20 '17 at 1:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.