xor n sets of variables for use in SAT transformation
I am doing a transformation from a customoized set cover problem to a sat, so I can perhaps use a sat solver for my problem.
My problem is: 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 can't seem to get right is that both sets of variables must not hav开发者_JAVA百科e the same occupancy as a combination. e.g. 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?
I succeeded with:
and(not((xnor x_i) and (xnor y_i))
精彩评论