如何将OPB格式的x1+x2+x3+x4=2约束转换为CNF格式？

要把OPB格式中的x1 + x2 + x3 + x4 = 2（四个变量恰好2个为真）转换成CNF格式，只需将约束拆分为至少2个变量为真和至多2个变量为真两部分，再分别转换为对应的子句，最后将所有子句合取即可。

1. 至少2个变量为真 #

这部分约束等价于“不能有3个或4个变量同时为假”，因此需要生成所有“任意3个变量的析取”子句（确保任意3个变量中至少有一个为真）：

• x1 ∨ x2 ∨ x3
• x1 ∨ x2 ∨ x4
• x1 ∨ x3 ∨ x4
• x2 ∨ x3 ∨ x4

2. 至多2个变量为真 #

这部分约束等价于“不能有3个或4个变量同时为真”，因此需要生成所有“任意3个变量的否定的析取”子句（确保任意3个变量中至少有一个为假）：

• ¬x1 ∨ ¬x2 ∨ ¬x3
• ¬x1 ∨ ¬x2 ∨ ¬x4
• ¬x1 ∨ ¬x3 ∨ ¬x4
• ¬x2 ∨ ¬x3 ∨ ¬x4

完整CNF子句集合 #

将上述两部分子句组合，就是等价于原约束的CNF：

x1 ∨ x2 ∨ x3
x1 ∨ x2 ∨ x4
x1 ∨ x3 ∨ x4
x2 ∨ x3 ∨ x4
¬x1 ∨ ¬x2 ∨ ¬x3
¬x1 ∨ ¬x2 ∨ ¬x4
¬x1 ∨ ¬x3 ∨ ¬x4
¬x2 ∨ ¬x3 ∨ ¬x4

通用转换思路 #

对于n个变量恰好k个为真的约束，通用转换方法是：

• 至少k个为真：生成所有C(n, n-k+1)个子句，每个子句是任意n-k+1个变量的析取（禁止n-k+1个变量同时为假）。
• 至多k个为真：生成所有C(n, k+1)个子句，每个子句是任意k+1个变量的否定的析取（禁止k+1个变量同时为真）。

内容的提问来源于stack exchange，提问作者Abraham