In the SCIP Optimization Suite 6.0 paper, there is a section on Aggregation Presolver. The example given is a linear constraint with 2 variables a1x1+a2x2=b where either x1 or x2 is made the subject, then substituting it to the other constraints. I understand the logic when this is a linear program.
However, for SAT problems, my problem file and transproblem files show the following:
[logicor] <c301>: logicor(<x591>[B],<~x666>[B]); (This comes from problem file)
[logicor] <c302>: logicor(<~x591>[B],<x666>[B]);
is transformed to
[binary] <t_x666>: obj=-0, global bounds=[-0,1], local bounds=[-0,1], aggregated: +1<t_x591>
and
[logicor] <c1402>: logicor(<x538>[B],<x138>[B]); (This comes from problem file)
[logicor] <c1403>: logicor(<~x538>[B],<~x138>[B]);
is transformed to
[binary] <t_x138>: obj=-0, global bounds=[-0,1], local bounds=[-0,1], aggregated: 1 -1<t_x538>
I don't understand how aggregation works in these 2 cases because of the logicor constraints. Would anybody explain this to me please? Thank you!
(Lots of guessing as i don't know much about scip internals)
The example
[logicor] <c301>: logicor(<x591>[B],<~x666>[B]); (This comes from problem file)
[logicor] <c302>: logicor(<~x591>[B],<x666>[B]);
is equivalent (boolean alg) to:
~591 -> ~x666
x591 -> x666
This really looks like case 2 of 4 (from presol_implics.h):
x=0 ⇒ y=lb and x=1 ⇒ y=ub : aggregate y == lb + (ub − lb)x
with:
lb = 0
ub = 1
leading to:
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>
So if scip's output means t_x666 is the replaced version of x666 this makes some sense to me.
The final aggregation-term also fits the truth-table:
a b (a | ~b) & (~a | b)
0 0 1
0 1 0
1 0 0
1 1 1
-> basically a negated XOR -> equality -> true iff both are equal
As the implication-graph is the natural thing to reason about 2-sat clauses, i'm inclined to say, that this really is the part of scips internals acting here.