New answers tagged constraint-programming
4
It looks like your first constraint should instead be
$$0b_1 + a_1 b_2 + a_2 b_3 - d \le 0$$
With this change, the logical implications are
\begin{align}
b_1 = 1 &\implies 0 \le d \le a_1 \\
b_2 = 1 &\implies a_1 \le d \le a_2 \\
b_3 = 1 &\implies a_2 \le d \le a_3
\end{align}
To avoid ambiguous borders, introduce a small tolerance $\epsilon>...
3
CP-SAT uses a SAT backend. But at any moment, just like with SMT solvers, the full model is never fully represented using clauses and Boolean literals. I recommend looking at the CPAIOR 2020 masterclass on CP (on YouTube) to get a better understanding of the architecture of the solver.
Top 50 recent answers are included
