xor n наборов переменных для использования в преобразовании SAT

Question

Я делаю преобразование из настраиваемой проблемы с обложкой набора на сидение, поэтому я могу использовать сит-решатель для своей проблемы.

Моя проблема: у меня есть несколько наборов переменных, которые взаимодействуют вместе в терминах проблемы с сидением; что-то вроде линий x_i v x_j v x_k; y_i v y_j v y_k.

Однако то, что я не могу понять, состоит в том, что оба набора переменных не должны иметь такое же заполнение, как и комбинация. например X_i может быть равно x_j, но весь набор не должен быть одинаково занят.

Как это выразить, чтобы я мог использовать его в сат-решателе?

Answer 1

мне удалось с:

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