transformation - xor n 组变量用于 SAT 转换

Question

我正在从定制的集合封面问题转换为 sat，所以我也许可以使用 sat 求解器来解决我的问题。

我的问题是：我有几组变量在 sat 问题中相互作用；类似的东西x_i v x_j v x_k; y_i v y_j v y_k。

但是，我似乎无法正确理解的是，两组变量的占用率不得与组合相同。egX_i可以等于x_j，但整个集合不能相等。

我该如何表达，以便我可以在 sat-solver 中使用它？

Answer 1

我成功了：

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