Add difference logic to Huub

[kletzi]

I'm finally preparing the pull request for difference logic. In the difference logic component itself, there are a few points to consider:

• A few open TODOs, mostly regarding potential efficiency gains, future extension points or extra tests.
• Check documentation (and level of detail)
• Check logging (frequency and relevance)
• I noticed that some of the (existing) test instances run into the debug assert that a literal used in a reason is unknown (it is known but not propagated yet). Depending on how these tests are executed, I'm not sure if this is an issue for the automated testing.
• I am currently running some experiments to determine the best default parameters for the internal difference logic settings.

Further, I have introduced a few global changes to review / discuss:

• to_solver has gained an extra argument, which is the model_trail (allows access to trailed values in the model for transformation)
• In from_fzn, I have given post_constraints access to the config
• Using advisors at model level, I found that they might not be triggered as they were only called at the end of propagate, but the first propagation might rely on the advisors getting triggered beforehand. I separated the propagate and notify_advisors methods in Model, and added a notify_advisors call before the first propagate call. This seems to work, but please check.
• I have made resolve_alias available via the SimplificationActions, as I would like to have only one node per underlying variable instead of duplicates for aliases.
• I have introduced assert_num_solutions to combine a solution checker with a solution count (as I sometimes had bugs where all returned solutions were correct, but not all correct solutions were returned).

[Dekker1]

I'm finally preparing the pull request for difference logic. In the difference logic component itself, there are a few points to consider:

* A few open TODOs, mostly regarding potential efficiency gains, future extension points or extra tests.

* Check documentation (and level of detail)

* Check logging (frequency and relevance)

Amazing work! In general, it looks great, so I'm looking forward to merging this. I'll add a full review, but I'd be happy to handle making some of the changes. Please let me know when you are happy for me to take over.

* I noticed that some of the (existing) test instances run into the debug assert that a literal used in a reason is unknown (it is known but not propagated yet). Depending on how these tests are executed, I'm not sure if this is an issue for the automated testing.

This would suggest that you are propagating in the wrong order. (The debug assert takes the order into account). Note that this would also suggest a problem for the SAT solver, since it means that the trailing order would be incorrect. The literal in the reason must be propagated before the literal that the reason implies.

* I am currently running some experiments to determine the best default parameters for the internal difference logic settings.

I'm looking forward to seeing the results. It would be great to reduce the number of options that we expose in the configuration and on the command line. For example, we haven't exposed any priority levels in the configuration before.

Further, I have introduced a few global changes to review / discuss:

* to_solver has gained an extra argument, which is the model_trail (allows access to trailed values in the model for transformation)

I think the capability that you've exposed is fine, but I might fine-tune it before we merge (or separately). Ideally, I would want to avoid having the extra argument as we fit all the other capabilities into the reformulation actions. However, this also seems like a good opportunity to investigate whether TrailedInt shouldn't be split between the Model and Solver layer, as you can currently request the value from somewhere where you didn't create it.

* In from_fzn, I have given post_constraints access to the config

I don't have a big issue with this, but it goes a little against the idea that a model is just a declaration of the decisions and constraints. Depending on what configuration options we are left with after parameter tuning, we might want to see whether this can be solved another way. Are the options relevant before we start solving?

* Using advisors at model level, I found that they might not be triggered as they were only called at the end of propagate, but the first propagation might rely on the advisors getting triggered beforehand. I separated the propagate and notify_advisors methods in Model, and added a notify_advisors call before the first propagate call. This seems to work, but please check.

I'll have a look! 👍

* I have made resolve_alias available via the SimplificationActions, as I would like to have only one node per underlying variable instead of duplicates for aliases.

This seems okay to me.

* I have introduced assert_num_solutions to combine a solution checker with a solution count (as I sometimes had bugs where all returned solutions were correct, but not all correct solutions were returned).

I'm not sure whether this is required. Are there that many solutions that expect_solutions doesn't work?

---

I've added some initial comments, but I probably need to inspect a little closer when I have some time. (That might take me a little while).

[Dekker1]

If we keep these options, then I would prefer to create descriptive enum types for their values, rather than using u8.

[kletzi]

Yes, we can reduce parameter options and make their values more explicit once we settle on the final parameters to expose or fix.

[Dekker1]

Similarly, I would prefer to use descriptive strings rather than numbers here. (Although I understand that this would be easy now for parameter tuning testing).

[Dekker1]

Unless required for some bit-fiddling. We should probably never store a PriorityLevel as a u8.

[Dekker1]

Instead of "start" and "stop" trace statements, this should use the span capability of tracing.

[kletzi]

Amazing work! In general, it looks great, so I'm looking forward to merging this. I'll add a full review, but I'd be happy to handle making some of the changes. Please let me know when you are happy for me to take over.

Thanks. I will have another look through my TODOs, documentation, logging, and some of the issues you mentioned, but feel free to start working on changes you would like to do, especially regarding the other solver parts that I touched. Our working times will not have a lot of overlap anyway.

* In from_fzn, I have given post_constraints access to the config

I don't have a big issue with this, but it goes a little against the idea that a model is just a declaration of the decisions and constraints. Depending on what configuration options we are left with after parameter tuning, we might want to see whether this can be solved another way. Are the options relevant before we start solving?

I think the main thing is that I collect all relevant constraints if difference logic is active, otherwise they are individually posted to the solver (so the on/off switch for difference logic as a whole)

* I have introduced assert_num_solutions to combine a solution checker with a solution count (as I sometimes had bugs where all returned solutions were correct, but not all correct solutions were returned).

I'm not sure whether this is required. Are there that many solutions that expect_solutions doesn't work?

Well I have a test with 85 solutions. Initially I just checked their validity, but during development I had bugs that cut off a few of them. I could also list all results or reduce the domains, but adding the count felt more convienent without restricting the test case.

[kletzi]

* I noticed that some of the (existing) test instances run into the debug assert that a literal used in a reason is unknown (it is known but not propagated yet). Depending on how these tests are executed, I'm not sure if this is an issue for the automated testing.

This would suggest that you are propagating in the wrong order. (The debug assert takes the order into account). Note that this would also suggest a problem for the SAT solver, since it means that the trailing order would be incorrect. The literal in the reason must be propagated before the literal that the reason implies.

I looked again at this one, and I'm not really sure what goes wrong:

0.692035300s TRACE propagate{level=1}:difference_logic_bounds: huub::constraints::difference_logic: Updating lower bound for i25 to 53
0.692137700s TRACE propagate{level=1}:difference_logic_bounds: huub::solver::solving_context: propagate lit="X_INTRODUCED_45_≥53" reason="X_INTRODUCED_40_≥46" prop=4
...  
0.696016000s TRACE propagate{level=1}:difference_logic_bounds: huub::constraints::difference_logic: Constraint DiffEdge { from: 25, to: 5, val: -5, bool_var: Some(89), bool_index: 0, out_index: 0, in_index: 11 } is falsified by bounds.
0.696073300s TRACE propagate{level=1}:difference_logic_bounds: huub::solver::solving_context: propagate lit="not X_INTRODUCED_201_" reason=lazy prop=4
...
0.700655700s DEBUG propagate{level=1}: huub::solver::engine: notify oracle lit="X_INTRODUCED_45_≥53"
0.700765500s DEBUG huub::solver::engine: assignments lits="X_INTRODUCED_45_≥53"
0.700877100s DEBUG huub::solver::engine: assignments lits="X_INTRODUCED_45_≥52, X_INTRODUCED_45_≥51, X_INTRODUCED_45_≥50, X_INTRODUCED_45_≥49, X_INTRODUCED_45_≥48, X_INTRODUCED_45_≥47, X_INTRODUCED_45_≥46, X_INTRODUCED_45_≥45, X_INTRODUCED_45_≥44"
...
0.708226300s DEBUG propagate{level=1}: huub::solver::engine: notify oracle lit="not X_INTRODUCED_201_"
0.708336700s TRACE propagate{level=1}: huub::solver::trail: undo to when literal was set len=3904 lit="not X_INTRODUCED_201_"
0.708450300s TRACE propagate{level=1}: huub::constraints::difference_logic: Explaining 18446744073709551482 with [BoolView(Lit(Lit(-3199))), BoolView(Lit(Lit(677)))]
0.708589500s ERROR propagate{level=1}: huub::solver::engine: invalid reason: not all antecedents are known true clause="X_INTRODUCED_45_<50 ∨ X_INTRODUCED_20_≥55 ∨ not X_INTRODUCED_201_" lit_explained="not X_INTRODUCED_201_" lit_invalid="X_INTRODUCED_45_≥50" invalid_val=None

• Difference logic updates the bound X_INTRODUCED_45>=53.
• The new bound causes the boolean to be set not X_INTRODUCED_201, reason lazy (with eager it does not trigger the error).
• The engine propagates the new bound for X_INTRODUCED_45 (and all missing lower bounds).
• However, when the lazy reason for X_INTRODUCED_201 is obtained, it fails. Is it because obtaining the lazy reason resets to the state where X_INTRODUCED_45>=53 did not yet propagate to X_INTRODUCED_45>=50? I'm obtaining the literals in the reason via lit_relaxed.

[Dekker1]

• Difference logic updates the bound X_INTRODUCED_45>=53.

• The new bound causes the boolean to be set not X_INTRODUCED_201, reason lazy (with eager it does not trigger the error).

• The engine propagates the new bound for X_INTRODUCED_45 (and all missing lower bounds).

• However, when the lazy reason for X_INTRODUCED_201 is obtained, it fails. Is it because obtaining the lazy reason resets to the state where X_INTRODUCED_45>=53 did not yet propagate to X_INTRODUCED_45>=50? I'm obtaining the literals in the reason via lit_relaxed.

But it looked that it doesn't happen in this order. What I glance from the log, is that first, not X_INTRODUCED_201_ is propagated, then something propagates X_INTRODUCED_45_≥53. It looks like the bound before this was X_INTRODUCED_45_≥43, so when we revert to before not X_INTRODUCED_201_ was set, X_INTRODUCED_45_≥50 is false. So with the requirement that the Reason is all known true (i.e. propagated) before the condition it implies, this does seem like an invalid reason.

Maybe I don't really understand how this is supposed to work. What is are the literals that you're requesting with lit_relaxed?

[AllenZzw]

Looking at the logs, my conjecture is that this is caused by an out-of-order propagation issue.

In the propagation algorithm, X_INTRODUCED_45 >= 53 is propagated first, and the algorithm assumes that X_INTRODUCED_45 >= 50 is already true. Based on the current lower bound of X_INTRODUCED_45, the propagator then infers not X_INTRODUCED_201.

Conceptually, the propagator “thinks” the trail (growing to the right) in the CP engine looks like:

... [X_INTRODUCED_45>=53], [X_INTRODUCED_45>=51], [X_INTRODUCED_45>=50], ... [X_INTRODUCED_45>=44], [not X_INTRODUCED_201]

However, in the actual implementation, the bound literals implied by X_INTRODUCED_45 >= 50 only become true after the literal X_INTRODUCED_45 >= 53 is notified to the SAT engine. As a result, not X_INTRODUCED_201 is placed immediately after X_INTRODUCED_45 >= 53.

So the real trail in the CP engine becomes:

... [X_INTRODUCED_45>=53], [not X_INTRODUCED_201], ... [X_INTRODUCED_45>=51], [X_INTRODUCED_45>=50], ... [X_INTRODUCED_45>=44]

When [not X_INTRODUCED_201] is propagated, debug_check_reason is triggered. To validate the reason, it resumes the trail using goto_assign_lit, resulting in:

... [X_INTRODUCED_45>=53], [not X_INTRODUCED_201]

This unassigns [X_INTRODUCED_45>=50], which is part of the reason clause for [not X_INTRODUCED_201]. Consequently, the reason check encounters an unassigned literal, leading to the invalid_val=None error.

As a hot fix, enabling eager explanation avoids resuming the trail in debug_check_reason, which prevents this inconsistency.

[kletzi]

Thanks for the details. [X_INTRODUCED_45>=53] is actually propagated first. [not X_INTRODUCED_201] is a consequence of [X_INTRODUCED_45>=53] and the other literal in the reason. Using [X_INTRODUCED_45>=50] is the lifted version of the reason.

It seems unexpected to me that when I give the same reason as an eager explanation the order is fine (oracle notify lit [X_INTRODUCED_45>=53] propagates [X_INTRODUCED_45>=50], then oracle notify lit [not X_INTRODUCED_201]), while with a lazy explanation it is reverted to the state before propagating the bound of 50 from the bound of 53, but I don't see how to realize this in the explain call. Requesting the bound of 50 via lit_relaxed causes no indication that this bound can't be used at this point.

Still, I can just activate eager mode in difference logic (this was one of the options for the experiments anyway). It also didn't seem to cause any follow-up issues when running in release mode where the assert is not triggered.

[Dekker1]

Okay, I now understand the problem. These issues with the channelling between the SAT and Engine stack remain annoying. I think it's just lit_relaxed by itself causes the problem, since some consequences might be out of order when checking, but would already be included in the reasons.

I'll have to think about a solution. We might be able to better maintain the order, but I might have to play around a little to find a solution that is performant.