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

Question

在 SCIP Optimization Suite 6.0 论文中，有一节是关于 Aggregation Presolver 的。给出的示例是具有 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

这真的很像 4 个案例中的第 2 个（来自 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 的替换版本，这对我来说有些意义。

最终的聚合项也符合事实-table:

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

-> 基本上是异或取反 -> 相等 -> 真当且仅当两者相等

由于蕴涵图是推理 2-sat 子句的自然之物，我倾向于说，这确实是 scips 内部机制的一部分。

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

What does Aggregation mean for SAT problems in SCIP?

mathematical-optimization

scip

sat