feat: Semantic Minimisation during Conflict Analysis

[ImkoMarijnissen]

Closes #397.

After discussing with @maartenflippo, I implemented a very simple implementation of the conjoin function from "Semantic Learning for Lazy Clause Generation - Feydy et al.".

Some anecdotal examples of the effect:
For an RCPSP instance (01.dzn), the number of failures goes from 3,711 to 3,376 and for another instance (J120_60_5), the number of failures to get to a solution of 108 is reduced from 28,303 to 27,855. For foxgeesecorn, the number of failures to get to an objective of 32 goes from 114,811 to 81,268.

There are a few things which are not entirely clear to me:

• Currently, whenever replacing a predicate with a fully new one (e.g., we replace $[x \geq 5]$ and $[x \neq 5]$ with $[x \geq 6]$), then I do a check that it will not be resolved on next to avoid infinite loops. Is this the correct way to handle it or is something else going wrong?
• In the paper, the conjoin function is underspecified, and it is somewhat unclear what exactly it does; for now, we assume that the elements in the working nogood are in the left side of the rewrite rules, and the added propagation reasons are on the right side of the rewrite rules. It was unclear to us what the reason for this is, but it appears to create incorrect nogoods otherwise.
• I have removed the check that a predicate has not already been seen. We think that this led to incorrectness but it would be good to double-check.

TODOs

• Implement more efficiently, likely with a data structure which is similar to the one used for semantic minimisation.
• Do not log all initial bounds but only when they are used
• Profile on larger benchmark set

[EmirDe]

This sounds great! Those are nice reductions in conflict. We can discuss next week.

Quick points.

1. It is surprising that you would get a predicate you have already seen. Once you process's it off the trail it should not appear again.
2. Please check the proofs using the checker. It might be that something goes wrong. The proofs should still be correct with semantic minimisation in between, I think!
3. Why do we use a simple conjoin in between and not the semantic minimisation procedure? Conjoin in the paper seems to do what we call semantic minimisation. Note that I did not get the comment about left and right side, not sure what you are referring to.
4. About replacing x>=5 & x!=5 with x>=6. Good idea, but it is tricky! If we replace those two and we get an asserting nogood, then it is a good idea to replace them. But if one if the two are next for resolving, and we do not get an asserting nogood by replacing then there is no point in replacing. Good point!

[maartenflippo]

Docs :)

[maartenflippo]

If I understand this correctly, it introduces $[x \neq v]$ for the initial holes. Why not just iterate the holes? Also note that if we introduce $\top \rightarrow [x \ge 5]$, then there is no need to introduce $\top \rightarrow [x \ne v]$ for $v < 5$.

[ImkoMarijnissen]

It only introduces the hole(s) when we have an element $[x \geq v]$ in the nogood, and a sequence of holes caused the lower-bound to become $v'$ (such that $v'$ > $v$)