异或 n 组变量用于 SAT 转换
我正在将定制的集合覆盖问题转换为 sat，因此我也许可以使用 sat 求解器来解决我的问题。
我的问题是：我有几组变量在卫星问题中相互作用；类似于 x_i v x_j v x_k 的东西； y_i v y_j v y_k 。
然而，我似乎无法理解的是，两组变量的组合不得具有相同的占用率。例如，X_i 可以等于x_j，但整个集合不得被同等占用。
我如何表达它以便我可以在卫星求解器中使用它？
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 have 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?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
我成功了：
I succeeded with: