PyChoco中如何实现O3=(O1+O2)%2的约束？

核心问题分析 #

你当前的代码存在两个关键问题：

1. O3的变量范围设为0-2，但模2运算的结果只能是0或1，这会允许无效取值存在；
2. 仅用O1[k] + O2[k] = O3[k]无法表达模2约束，当O1和O2同时为1时，和为2，O3会被错误约束为2而非0。

两种可行解决方案 #

方案1：使用异或约束（推荐） #

对于0/1变量，(O1 + O2) % 2和**异或（XOR）**运算完全等价，Choco内置的xor约束可以直接实现需求：

from choco import Model

model = Model()

# 所有向量元素都限定为0或1
O1 = model.intvars(2, 0, 1)
O2 = model.intvars(2, 0, 1)
O3 = model.intvars(2, 0, 1)

for k in range(2):
    # 异或约束等价于模2加法结果：O3[k] = (O1[k] + O2[k]) % 2
    model.xor(O1[k], O2[k], O3[k])

方案2：使用算术约束表达模2关系 #

如果更倾向于用算术等式表达，可以直接约束(O1[k] + O2[k] - O3[k])能被2整除：

from choco import Model

model = Model()

O1 = model.intvars(2, 0, 1)
O2 = model.intvars(2, 0, 1)
O3 = model.intvars(2, 0, 1)

for k in range(2):
    # 约束差值为偶数，等价于模2相等
    model.arithm(O1[k], '+', O2[k], '-', O3[k], 'mod', 2, '=', 0)

也可以通过进位变量实现更直观的加法逻辑：

for k in range(2):
    t = model.intvar(0, 1)  # 进位变量，仅当O1、O2同时为1时取1
    model.arithm(O1[k], '+', O2[k], '=', 2, '*', t, '+', O3[k])

效果验证 #

无论采用哪种方案，O3的元素都会被严格约束为0或1，且完全符合O3 = (O1 + O2) %2的逻辑要求。

内容的提问来源于stack exchange，提问作者Arnaud Bégyn