为何两组单独可满足的Dimacs CNF表达式合并后不可满足？

我是计算机科学专业新生，还没完全搞懂可满足性（satisfiability）概念。我为SAT求解器写了两组Dimacs CNF表达式，单独验证都是可满足（Satisfiable）的，但合并后就变成不可满足（Unsatisfiable）了。我本来以为两组表达式语义等价，完全搞不懂为什么会冲突。我的需求是构建一个表达式，判断十字路口里哪些信号灯能同时亮绿灯而不引发碰撞。

第一组表达式（单独可满足） #

-1 -2 0
-1 -4 0
-2 -1 0
-2 -3 0
-3 -2 0
-3 -4 0
-4 -3 0
-4 -1 0

Satisfiable

这组表达式的核心是互斥约束：每个子句-a -b 0的意思是「信号灯a和b不能同时亮绿灯」。而且这里有很多重复子句（比如-1 -2 0和-2 -1 0是完全等价的），本质上是约束信号灯1、2、3、4中，任意两个都不能同时亮绿灯。所以它的可行解是：最多亮一个绿灯，或者全灭。

第二组表达式（单独可满足） #

1 3 0
3 1 0
2 4 0
4 2 0

Satisfiable

这组表达式的核心是**「至少一个亮」的约束**：每个子句a b 0的意思是「信号灯a和b中至少有一个亮绿灯」。同样这里也有重复子句（1 3 0和3 1 0等价），实际约束是「1和3至少亮一个」，且「2和4至少亮一个」。它的可行解包括：1亮3灭、1灭3亮、1亮3亮、2亮4灭、2灭4亮、2亮4亮，或者这些组合的叠加（比如1亮3亮+2亮4亮）。

合并后的表达式（不可满足） #

-1 -2 0
-1 -4 0
-2 -1 0
-2 -3 0
-3 -2 0
-3 -4 0
-4 -3 0
-4 -1 0
1 3 0
3 1 0
2 4 0
4 2 0

Unsatisfiable

冲突原因：两组表达式语义完全不等价，约束矛盾 #

第一组要求「任意两个信号灯不能同时亮」，第二组要求「1和3至少亮一个，且2和4至少亮一个」——这两个约束放在一起根本无法同时满足：

• 要满足第二组，至少需要亮两个信号灯（比如1和2、3和4、1和3、2和4），但第一组禁止任何两个信号灯同时亮；
• 哪怕只亮一个信号灯，比如亮1，那第二组的「2和4至少亮一个」就无法满足；亮3同理，亮2的话「1和3至少亮一个」无法满足，亮4也一样；全灭的话两组约束都不满足。

所以合并后的表达式没有可行解，自然是不可满足的。

修正后的正确表达式 #

如果你的需求是十字路口信号灯（通常对向信号灯可同时亮，比如1和3是对向，2和4是对向），正确的约束应该是：

1. 互斥约束：禁止同向/交叉的信号灯同时亮（去掉重复子句）：

   -1 -2 0
   -1 -4 0
   -2 -3 0
   -3 -4 0
   

2. 对向同步约束：对向信号灯必须同时亮或同时灭（用等价子句-a b 0和-b a 0表示「a亮当且仅当b亮」）：

   -1 3 0
   -3 1 0
   -2 4 0
   -4 2 0
   

把这两组合并后，SAT求解器会给出两个可行解：

• 1亮、3亮，2灭、4灭；
• 2亮、4亮，1灭、3灭；
  完全符合十字路口的实际通行规则。

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