Hey you guys,
I am doing a transformation from a customoized set cover problem to a sat, so i can mayhaps use a sat solver for my problem. My problem is, that i have several sets of variables that interact together in a term of the sat problem. something along the lines of x_i v x_j v x_k; y_i v y_j v y_k
. However what i cant seem to get right is, that both sets of variables must not have the same occupancy as a combination. e.q. X_i
can be equal to x_j
, but the whole set must not be equally occupated.
How do i express that so i can use it in a sat-solver?
cheers