I'm exploring the use of SAT solvers to find a permutation of the numbers 1, 2, and 3, subject to specific constraints. Initially, I considered employing nine variables: $x_{1,1}, x_{1,2}, \dots, x_{3,3}$, where $x_{i,j}$ is true if the number $i$ is placed in position $j$ in the permutation.
However, since there are only $3! = 6$ possible permutations, it seems excessive to use nine variables. I'm contemplating using just three boolean variables, $y_1, y_2, y_3$. My idea is to map each permutation to a unique combination of true or false values of these $y_i$'s. But I'm finding it challenging to formulate the constraints under this scheme.
Could there be a more efficient encoding strategy that strikes a balance between the number of variables and their expressive power? I'm seeking a method that simplifies the representation of permutations and constraints in a SAT solver context.
In isolation, the obvious answer is to enumerate all 6 permutations and check which ones satisfy the conditions.
Without more context, this is not answerable. There are many ways to represent a permutation of 3 elements. We can't tell you which is best, because that depends on the rest of your model.
Here are some candidate options to consider:
A one-hot encoding of which of the 6 permutations has been chosen. This requires 6 boolean variables.
A binary encoding of which of the 6 permutations has been chosen. This requires $\lceil \lg 6 \rceil = 3$ boolean variables.
For each pair $i,j$, a boolean variable indicating whether $\pi(i)<\pi(j)$. This requires 6 boolean variables.