views:

12

answers:

1

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

A: 

Ok, i have done it with

and(not((xnor x_i) and (xnor y_i))

tarrasch