This is probably a downstream bug in Exact, but posting it here for archival purposes.
While working on the mtz-circuit branch (#354) I encountered the following extremely confusing bug.
I'm not very sure to what it is related, at first I thought the Circuit decomp was to blame but it seems to be something else instead.
The model below has a Circuit constraint as the objective function, which internally gets reified and decomposed.
It also has some seemingly unrelated constraint a + b + c >= 1.
Now, I make the bounds of these variables large enough (> 8) they will be log-encoded by exact using the heuristic value set in the CPMpy interface.
When this happens, the result of the optimization process is that the reification variable (Boolean) is True instead of False, and hence; the Circuit constraint is enforced.
This is not the correct behaviour as it should be asserted to False (as we are minimizing).
# Random model with just some vars
ivs = cp.intvar(0,7,shape=3, name=tuple("abc")) # -> these variables will be order-encoded
# ivs = cp.intvar(0,10,shape=3, name=tuple("abc")) # -> these variables will be log-encoded
x,y,z = cp.intvar(-3,5, shape=3, name=tuple("xyz"))
cons = cp.Circuit(x,y,z)
solver = cp.SolverLookup.get("exact")
solver += cp.sum(ivs) >= 1
solver.minimize(cons)
assert solver.solve()
print(solver.status())
print(f"Value of {cons} is", cons.value(), [x.value(), y.value(), z.value()])
assert cons.value() is FalseI know it is very convoluted, and weird but I could not find any more minimal example than this...
Perhaps @JoD can shed some light on this?
CPMpy commit 68a3fc6
Exact commit 5da02b6
This is probably a downstream bug in Exact, but posting it here for archival purposes.
While working on the mtz-circuit branch (#354) I encountered the following extremely confusing bug.
I'm not very sure to what it is related, at first I thought the Circuit decomp was to blame but it seems to be something else instead.
The model below has a Circuit constraint as the objective function, which internally gets reified and decomposed.
It also has some seemingly unrelated constraint
a + b + c >= 1.Now, I make the bounds of these variables large enough (> 8) they will be log-encoded by exact using the heuristic value set in the CPMpy interface.
When this happens, the result of the optimization process is that the reification variable (Boolean) is True instead of False, and hence; the Circuit constraint is enforced.
This is not the correct behaviour as it should be asserted to False (as we are minimizing).
I know it is very convoluted, and weird but I could not find any more minimal example than this...
Perhaps @JoD can shed some light on this?
CPMpy commit 68a3fc6
Exact commit 5da02b6