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

【问题标题】：What does Aggregation mean for SAT problems in SCIP?聚合对 SCIP 中的 SAT 问题意味着什么？
【发布时间】：2020-03-25 10:04:23
【问题描述】：

在 SCIP 优化套件 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>

由于逻辑或约束，我不明白在这两种情况下聚合是如何工作的。请有人向我解释一下吗？谢谢！

【问题讨论】：

标签： mathematical-optimization scip sat

【解决方案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

这真的很像case 2 of 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 内部结构的一部分。

【讨论】：