I have the following scenario which I need to represent in CNF: we have $n$ bins, and $A_{ij}$ holds iff balls $i$ and $j$ are in a consecutive pair of bins such that the first bin of the pair is even-numbered. Let $B_{ik}$ denote that ball $i$ is in bin $k$.
To start, I came up with the following equivalence:
$$A_{ij} \Leftrightarrow \bigvee\limits_{k=0, 2, 4 ...n-2}(B_{jk} \wedge B_{i(k+1)}) \vee (B_{ik} \wedge B_{j(k+1)})$$
Then I got rid of the implications:
$$(\neg A_{ij} \vee \bigvee\limits_{k=0, 2, 4 ...n-2}(B_{jk} \wedge B_{i(k+1)}) \vee (B_{ik} \wedge B_{j(k+1)})) \wedge (A_{ij} \vee \neg \bigvee\limits_{k=0, 2, 4 ...n-2}(B_{jk} \wedge B_{i(k+1)}) \vee (B_{ik} \wedge B_{j(k+1)}))$$
But here I sort of ran out of ideas. Converting a sum of products to a product of sums like this seems it would require a great deal of clauses, which isn't totally out of the question but I'm hoping for something more elegant. I kind of have a feeling that maybe there's an alternate way of encoding these constraints that maps fairly easily to CNF.
