Revisit Semantic Minimisation during Learning

[ImkoMarijnissen]

At some point, we discussed semantic minimation during conflict analysis but concluded that there were issues with our approach.

Rereading the paper "Semantic Learning for Lazy Clause Generation - Feydy et al." shows that they use a certain approach in the conjoin function. We should re-examine to see how this is different from what we did previously and evaluate it in the solver.

[ImkoMarijnissen]

Looking at the paper again, I think their approach is as follows:

During conflict analysis, they continuously untrail until at least one of the elements is not true in the domain anymore.

There could be multiple atomic constraints which have become unsatisfied due to untrailing a single entry (e.g., there could be an explicitly-trailed atomic constraint and one or more explicitly trailed atomic constraint). They take the reason for this set of atomic constraints and then use the rewrite rules on the working nogood (minus the elements that just became unsatisfied by the last untrailing operation) and the reason for this set of atomic constraints.

I wonder whether there is anything in the conjoin function which places additional restrictions on when this function can be performed (e.g., maybe it restricts it so that one element from one set and one element from the other can be used; implying that if the reason contains $[x \geq 5]$ and $[x \neq 5]$, then this would not be simplified by this rule), this seems to be the only reason for making it a function that takes two arguments instead of a function which takes one argument.

I am still unsure how this would differ from what we tried previously.