Dekker1
commented
1 year ago Thank you for your in-depth diagnosis of the problem. Hopefully we can resolve it.
Considering the fact you submitted a PR for the last problem you reported, please let me know if you are working on fixing the problem. Either way, your contributions are much appreciated.
Samclou
When solving the minimisation problem problem_steiner.txt, the solver finds a solution of cost 12 and reports it as optimal. This problem relates to finding a Steiner tree of minimal cost that is a sub-graph of the graph illustrated here
, with nodes 1, 3, and 6 being the terminal nodes. We can see that this problem has a solution of cost 11, highlighted in red in the previous illustration. This solution can be found by modifying the search heuristic.
When inspecting the lower bounds found for the cost by IncrementalMinimumWTreePropagator and their explanations, we can find that during the problematic search, the state [All nodes fixed to true except 2 which is false, and edges (1, 5) and (3, 5) fixed to true and edges (1, 6), (1,7), (2, 5) and (2, 6) fixed to false] is reached. This leads to a lower bound of 13 being found and explained by the edges (1, 5) and (3, 5) being true. Since it happens after the solution of cost 12 was found, it causes a conflict. Should all mandatory nodes (nodes that are fixed to true at that time in the search tree) be terminal nodes, this lower bound with this explanation would be completely valid. However, we are not in that case and this explanation seems to be removing the optimal solution.
I have not looked specifically at how the explanations are created in the code, but I hypothesize that the cause of the problem is that the logic in section 3.3.6.1 and 3.3.6.3 from De Uña's thesis should make a distinction between mandatory nodes and terminal nodes. For example, the fact that nodes 4 and 7 are mandatory in the problematic state (lifting the lower bound found by 3), but are not part of the explanation could be a problem. Also, perhaps the spR set is not full enough. For exemple, (2, 5) and (2, 6) were false and are a shortest path between 5 and 6, but were not used in the explanation.
Important notes: IncrementalMinimumWTreePropagator in itself seems to have other issues. When running it in debug, there is sometimes an infinite loop at the end of the short_dijkstra method because its priority_queue may be popped while empty, which somehow breaks its destructor into looping on itself. Also, the assertion of line 673 sometimes fails on this instance. I do not understand the meaning of this assertion; a splb of 1 seems reasonable to me.