xor用於SAT轉換的變量集合

Question

我正在做一個從定製的集合覆蓋問題到sat的轉換，所以我可以使用sat解決方案來解決我的問題。

我的問題是：我有幾組變量在sat問題的術語中相互作用;沿着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))