Turning off backwards rewrites in proof

[bet20ICL]

What would be the quickest way to turn off using backward rewrites to explain the equivalence between two expressions on an e-graph?

For context, I am investigating rewrite scheduling techniques to delay the exponential blowup of the e-graph. My strategy is to run a testcase using the SimpleScheduler for a large number of iterations, to get an empirically optimal solution. Then, I will run the testcase using an experimental scheduler, and try to reach an e-graph that is much smaller, but still contains the same optimal solution.

I want to get an understanding of the upper bound on the performance of any scheduler that applies all matches on a rewrite (does not rewrite only certain parts of the e-graph), by estimating the size of the minimum possible e-graph that still contains an optimal solution. To do this I am running the testcase with only the rewrites that appear in the proof of the optimal solution. However, due to the presence of backwards rewrites in the proof, I am rarely able to make an e-graph that contains the target solution (missing some crucial forward rewrites).

[mwillsey]

Cool!! I think @oflatt is the right person to answer this.

[oflatt]

Great question! Let me answer this in three parts.

backwards rewrites

Unfortunately, there's no way to turn off "backwards rewrites" in the egraph. At a high level, this is because the congruence closure algorithm treats all of the actual matches of rewrites as equalities with no direction. At a deeper level, it's very difficult to attempt to generate a proof with only forward rewrites due to proofs of congruence. Imagine we need a proof of congruence between f(a) and f(b) (the proof is that a = b) and a proof of congruence between g(b) and g(a) (the proof is that b = a). Now we need both directions in one proof! In fact, I'm guessing that finding a proof with just forward rewrites is NP-Hard. I've been thinking about this problem because it would be a really useful feature if possible.

egraphs / proofs of minimum size

In fact, finding the size of the minimum possible e-graph that has the solution is an NP-complete problem, since it's the same problem as finding a proof of optimal size (https://link.springer.com/article/10.1007/s10703-017-0283-x). So we can't actually figure out what the optimal schedule of rewrites would be to arrive at your solution. However, egg has a greedy algorithm that does it's best to minimize the proof size. It's not in the latest egg release yet, so you need to use the lastest main branch to use it. (We have a paper going to FMCAD22 all about it).

proofs as a baseline for rewrite scheduling

It's a really interesting idea to use proofs as a baseline for how good your scheduler is! We have thought about it too, but nobody has tried it yet. The proof is our best guess at the smallest egraph that contains the solution. So instead of using the size of your smaller egraph, I suggest using the number of unique equalities in the proof as your baseline (the smallest egraph we have discovered that contains your target equality) and compare to the number of equalities in the larger egraph.

[mwillsey]

Would there be a way to use set the proof "cost function" to minimize backwards edges?

[oflatt]

I don't think so, because an edge is only backwards with respect to a particular proof. One edge might be used either way depending on the path you take for proving two things are equal.

[oflatt]

Here's the arxiv for the paper!
https://arxiv.org/abs/2209.03398