ILP-based extractor that produces an optimal dag-cost extraction

[TrevorHansen]

I mentioned in #24 that I've made an updated ILP extractor that given enough time, will produce an optimal (least-cost) DAG-extaction. It's my preference to combine this and the work in #24, so we have a faster & simple ILP extractor that can produce optimal DAG extractions.

I now realise, either the bottom-up, or faster-bottom-up will produce an optimal tree-extraction. So with this ILP extractor we can now produce optimal dag or tree extractions.

I'm not sure if it's widely appreciated, but the current ILP extractor isn't good. Looking at the details below, you can see the the current/old extractor is about 95 times slower than the faster-greedy-dag extractor and produces extractions that are much worse than it. I can't see a reason to use the current/old ILP extractor.

cumulative time for faster-greedy-dag: 3146ms
cumulative dag cost for faster-greedy-dag: 77029

(10 second timeout)
cumulative time for ilp-cbc: 1039220ms
cumulative dag cost for ilp-cbc: 76100

cumulative time for ilp-cbc-old: 297838ms
cumulative dag cost for ilp-cbc-old: 118031

cumulative time for ilp-cbc: 1039220ms
cumulative time for ilp-cbc-old: 297838ms
cumulative tree cost for ilp-cbc: 32017750412190
cumulative tree cost for ilp-cbc-old: 35474620331874
cumulative dag cost for ilp-cbc: 76100
cumulative dag cost for ilp-cbc-old: 118031
ilp-cbc / ilp-cbc-old
geo mean
tree: 0.6204
dag: 0.6842
micros: 22.8171
quantiles
tree:   0.0229, 0.5030, 0.5840, 0.8510, 2.3333
dag:    0.0233, 0.5762, 0.6541, 0.8865, 1.1095
micros: 0.1439, 9.9892, 31.2070, 63.5396, 461.6565

The ILP solver in this PR is slow on some instances, with some taking >10 hours to optimise. So has a timeout, that if reached, will return the results from the faster-greedy-dag, which is fast and kinda-ok.

Here are the results at some timeouts for 260 test inputs.

2 second timeout, dag cost 77,011, 343 second cumulative, 125 unfinished
10 second timeout, dag cost  76,100, 1,039 second cumulative, 86 unfinished
30 second timeout, dag cost  75,894, 2,580 second cumulative, 71 unfinished
100 second timeout, dag cost 75,866, 6,509 second cumulative, 50 unfinished

[oflatt]

Does this already combine with #24?

[TrevorHansen]

Does this already combine with #24?

Not yet. Hopefully when they're combined, and this ILP extractor is using good_lp/highs instead of CBC solver the runtime will drop by 1/3 (like @averyanalex has demonstrated with the current ILP extractor).

Going forward, I'm imagining something like this:

• Merge the good_lp/highs ILP extractor (Add good_lp based (with highs solver) extractor #24) into main.
• Merge this ILP extractor (ILP-based extractor that produces an optimal dag-cost extraction #30) into main.
• Merge the better test code (Test code #31) into main.
• Using the better test code, confirm that the updated extractors(Add good_lp based (with highs solver) extractor #24, ILP-based extractor that produces an optimal dag-cost extraction #30) are sound.
• Change this extractor to use good_lp/highs

[oflatt]

Sounds like a good plan!

[oflatt]

Let me know if you are ever blocked on a review

[TrevorHansen]

Let me know if you are ever blocked on a review

Thanks @oflatt, I'm happy with this PR now, who should I ask to review it?

[averyanalex]

Does this already combine with #24?

Not yet. Hopefully when they're combined, and this ILP extractor is using good_lp/highs instead of CBC solver the runtime will drop by 1/3 (like @averyanalex has demonstrated with the current ILP extractor).

Going forward, I'm imagining something like this:

* Merge the good_lp/highs ILP extractor ([Add good_lp based (with highs solver) extractor #24](https://github.com/egraphs-good/extraction-gym/pull/24)) into main.

* Merge this ILP extractor ([ILP-based extractor that produces an optimal dag-cost extraction #30](https://github.com/egraphs-good/extraction-gym/pull/30)) into main.

* Merge the better test code ([Test code #31](https://github.com/egraphs-good/extraction-gym/pull/31)) into main.

* Using the better test code, confirm that the updated extractors([Add good_lp based (with highs solver) extractor #24](https://github.com/egraphs-good/extraction-gym/pull/24), [ILP-based extractor that produces an optimal dag-cost extraction #30](https://github.com/egraphs-good/extraction-gym/pull/30)) are sound.

* Change this extractor to use good_lp/highs

It might make sense to merge #30 first, and then I'll try to port the updated extractor to good_lp.

[mwillsey]

I like the overall plan, and I like the consolidation of extractor variants (too many makes it hard to compare). The problem with optimal ILP is cycle breaking, and I'm not 100% clear on how this approach works on that. Can you include a comment or something on how cycles are avoided? It seems like cycle avoidance strategies will be a major distinguishing factor for DAG-based extractors.

[TrevorHansen]

... The problem with optimal ILP is cycle breaking, and I'm not 100% clear on how this approach works on that. Can you include a comment or something on how cycles are avoided? It seems like cycle avoidance strategies will be a major distinguishing factor for DAG-based extractors.

Sure, I've added this description to the code:

To block cycles, we enforce that a topological ordering exists on the extraction.
Each class is mapped to an integer variable (called its level). Then for each node,
we add a constraint that if a node is active, then the level of the class the node
belongs to must be less than than the level of each of the node's children.

To create a cycle, the levels would need to decrease, so they're blocked. For example,
given a two class cycle: if class A, has level 'l', and class B has level 'm', then
'l' must be less than 'm', but because there is also an active node in class B that
has class A as a child, 'm' must be less than 'l', which is a contradiction.

[mwillsey]

is it being an integer variable important? Could it be a real-valued one? That might be easier for the solver.

[TrevorHansen]

is it being an integer variable important? Could it be a real-valued one? That might be easier for the solver.

Nicely spotted! Combined with some other changes it reduced the runtime by about 15%.