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

---

Experimentation

Overall Results

main

{'ERROR': 5,
 'OOM': 8,
 'OPTIMAL': 100,
 'SATISFIABLE': 156,
 'SATISFIABLE_WITH_OOM': 26,
 'UNKNOWN': 93,
 'UNSATISFIABLE': 5}

new

{'ERROR': 5,
 'OOM': 6,
 'OPTIMAL': 100,
 'SATISFIABLE': 162,
 'SATISFIABLE_WITH_OOM': 21,
 'UNKNOWN': 94,
 'UNSATISFIABLE': 5}

main-free

{'ERROR': 8,
 'OOM': 5,
 'OPTIMAL': 141,
 'SATISFIABLE': 149,
 'SATISFIABLE_WITH_OOM': 18,
 'UNKNOWN': 66,
 'UNSATISFIABLE': 6}

new-free

{'ERROR': 8,
 'OOM': 5,
 'OPTIMAL': 143,
 'SATISFIABLE': 147,
 'SATISFIABLE_WITH_OOM': 16,
 'UNKNOWN': 68,
 'UNSATISFIABLE': 6}

main-no-recursive

{'ERROR': 5,
 'OOM': 14,
 'OPTIMAL': 100,
 'SATISFIABLE': 121,
 'SATISFIABLE_WITH_OOM': 61,
 'UNKNOWN': 87,
 'UNSATISFIABLE': 5}

new-no-recursive

{'ERROR': 5,
 'OOM': 13,
 'OPTIMAL': 102,
 'SATISFIABLE': 124,
 'SATISFIABLE_WITH_OOM': 55,
 'UNKNOWN': 89,
 'UNSATISFIABLE': 5}

MiniZinc Score

{
    'main': 653.42,
    'new': 664.42,
    'main-free': 1010.45,
    'new-free': 1010.05,
    `main-no-recursive`: 742.20,
    `new-no-recursive`: 747.46,
}

Average Primal Integral

{
    'main': 145.50,
    'new': 141.34,
    'main-free': 67.18,
    'new-free': 71.24,
    `main-no-recursive`: 143.33,
    `new-no-recursive` 143.27,
}

[maartenflippo]

Do we still need semantic minimisation if we have this?

[ImkoMarijnissen]

After adding some additional checks, I think that they are only used to merge and unmerge the disequalities. We can do this manually, what do you think?

[maartenflippo]

I think that would be better. Now it is a bit confusing why we would have both

[ImkoMarijnissen]

I have implemented this, but I am not sure whether this is exactly clearer, since it is quite a lot of case differentiation...

Review re-requested

[maartenflippo]

I still have some minor comments, but overall looks good enough to merge if we have exhausted the good will to work on this feature.

[maartenflippo]

I think this can just be private?

[maartenflippo]

to_process_heap is unknown in this context now

[maartenflippo]

It feels like this logic should also be encapsulated in the drain_predicates function. At this point in the interface of WorkingNogood it is not clear what the difference is between add_asserting_predicate and add_predicate. I get the impression this is still an artifact from before this abstraction, but perhaps I am wrong.

[ImkoMarijnissen]

I have moved this method to be part of the drain_predicates function; this also makes the add_asserting_predicate a private function. The main difference with other methods is that it does not perform a redundancy check for asserting predicates.