开发者

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))
0

上一篇:

下一篇:

精彩评论

暂无评论...
验证码 换一张
取 消

最新问答

问答排行榜