聚合对SCIP中的SAT问题意味着什么

Question

在SCIP Optimization Suite 6.0的论文中，有一节是关于聚合预分解器的。给出的例子是一个具有2个变量a1x1+a2x2=b的线性约束，其中x1或x2是主体，然后将其替换为其他约束。当这是一个线性程序时，我理解它的逻辑。

但是，对于SAT问题，我的problem文件和transproblem文件显示以下内容：

[logicor] <c301>: logicor(<x591>[B],<~x666>[B]); (This comes from problem file)
[logicor] <c302>: logicor(<~x591>[B],<x666>[B]);

转换为

[binary] <t_x666>: obj=-0, global bounds=[-0,1], local bounds=[-0,1], aggregated: +1<t_x591>

和

[logicor] <c1402>: logicor(<x538>[B],<x138>[B]); (This comes from problem file)
[logicor] <c1403>: logicor(<~x538>[B],<~x138>[B]);

转换为

[binary] <t_x138>: obj=-0, global bounds=[-0,1], local bounds=[-0,1], aggregated: 1 -1<t_x538>

由于逻辑的限制，我不理解聚合在这两种情况下是如何工作的。有人能向我解释一下吗？非常感谢。

Answer 1

(很多猜测，因为我对scip内部不太了解(

示例

[logicor] <c301>: logicor(<x591>[B],<~x666>[B]); (This comes from problem file)
[logicor] <c302>: logicor(<~x591>[B],<x666>[B]);

等价于(布尔代数(：

~591 -> ~x666
x591 -> x666

这看起来确实像第2种情况(共4种((来自presol_implics.h(：

x=0 ⇒ y=lb and x=1 ⇒ y=ub : aggregate y == lb + (ub − lb)x

带有：

lb = 0 
ub = 1

导致：

aggregate y == lb + (ub − lb)x
<-> x666 == 0 + (1-0) x591 
<-> x666 == +1 x591
for comparison:
[binary] <t_x666>: obj=-0, global bounds=[-0,1], local bounds=[-0,1], aggregated: +1<t_x591>

因此，如果scip的输出意味着t_x666是x666的替换版本，这对我来说是有意义的

最后的聚合项也符合真值表：

a    b    (a | ~b) & (~a | b)
0    0        1
0    1        0
1    0        0
1    1        1

->基本上是一个否定的XOR->相等->真，当两者都相等时

由于蕴涵图是对2-sat子句进行推理的自然结果，我倾向于说，这实际上是scips内部作用的一部分。