Minimize both AstSize and number of rewrites?

[AlienKevin]

I'm trying to use egg for boolean algebra simplification. The goal is to show the theorem applied in each step and explain to students how the boolean expression can be simplified. Ideally, I want to show the easiest simplification process with the least number of steps. For my implementation, I followed the tutorial and used the default AstSize extractor. It successfuly finds the simplest boolean expressions for all of my tests. However, some simple expressions took a long time and applied unnecessary rewrites. For example, here's an example where an unnecessary commutativity rule is applied when an involution is enough.

(| a (~ (~ b)))
(Rewrite=> commutativity' (| (~ (~ b)) a))  // Unnecessary
(| (Rewrite=> involution b) a)

Minimal simplification process:
(| a (~ (~ b)))
(| a (Rewrite=> involution b))

A more complicated example with an unnecessary commutativity rule:

(| (~ a) (& a b))
(| (~ a) (Rewrite=> commutativity (& b a)))  // Unnecessary
(Rewrite=> distributivity'-rev (& (| (~ a) b) (| (~ a) a)))
(& (| (~ a) b) (| (~ a) (Rewrite=> involution-rev (~ (~ a)))))
(& (| (~ a) b) (Rewrite=> complements' 1))
(Rewrite<= identity-rev (| (~ a) b))

Minimal simplification process:
(| (~ a) (& a b))
(Rewrite=> distributivity'-rev (& (| (~ a) a) (| (~ a) b)))
(& (| (~ a) (Rewrite=> involution-rev (~ (~ a)))) (| (~ a) b))
(& (Rewrite=> complements' 1) (| (~ a) b))
(Rewrite<= identity-rev (| (~ a) b))

I understand that the AstSize cost function cannot guarantee minimal rewrites. So is there a way to write a custom function that minimize both AstSize and number of rewrites? Thanks.

Below is the important part of my implementation

pub fn simplify_sexp(expr: &str) -> (RecExpr<SymbolLang>, String) {
    let rules: &[Rewrite<SymbolLang, ()>] = &[
        // Boolean theorems of one variable (Table 2.2 pg 62)
        rw!("identity"; "(& ?b 1)" <=> "?b"),
        rw!("identity'"; "(| ?b 0)" <=> "?b"),
        vec![rw!("null-element"; "(& ?b 0)" => "0")],
        vec![rw!("null-element'"; "(| ?b 1)" => "1")],
        rw!("idempotency"; "(& ?b ?b)" <=> "?b"),
        rw!("idempotency'"; "(| ?b ?b)" <=> "?b"),
        rw!("involution"; "(~ (~ ?b))" <=> "?b"),
        vec![rw!("complements"; "(& ?b (~ ?b))" => "0")],
        vec![rw!("complements'"; "(| ?b (~ ?b))" => "1")],
        // Boolean theorems of several variables (Table 2.3 pg 63)
        rw!("commutativity"; "(& ?b ?c)" <=> "(& ?c ?b)"),
        rw!("commutativity'"; "(| ?b ?c)" <=> "(| ?c ?b)"),
        rw!("associativity"; "(&(& ?b ?c) ?d)" <=> "(& ?b (& ?c ?d))"),
        rw!("associativity'"; "(|(| ?b ?c) ?d)" <=> "(| ?b (| ?c ?d))"),
        rw!("distributivity"; "(| (& ?b ?c) (& ?b ?d))" <=> "(& ?b (| ?c ?d))"),
        rw!("distributivity'"; "(& (| ?b ?c) (| ?b ?d))" <=> "(| ?b (& ?c ?d))"),
        vec![rw!("covering"; "(& ?b (| ?b ?c))" => "?b")],
        vec![rw!("covering'"; "(| ?b (& ?b ?c))" => "?b")],
        vec![rw!("combining"; "(| (& ?b ?c) (& ?b (~ ?c)))" => "?b")],
        vec![rw!("combining'"; "(& (| ?b ?c) (| ?b (~ ?c)))" => "?b")],
        rw!("consensus"; "(| (| (& ?b ?c) (& (~ ?b) ?d)) (& ?c ?d))" <=> "(| (& ?b ?c) (& (~ ?b) ?d))"),
        rw!("consensus'"; "(& (& (| ?b ?c) (| (~ ?b) ?d)) (| ?c ?d))" <=> "(& (| ?b ?c) (| (~ ?b) ?d))"),
        rw!("de-morgan"; "(~ (& ?b ?c))" <=> "(| (~ ?b) (~ ?c))"),
        rw!("de-morgan'"; "(~ (| ?b ?c))" <=> "(& (~ ?b) (~ ?c))"),
    ]
    .concat();

    let start = expr.parse().unwrap();
    let mut runner = Runner::default()
        .with_explanations_enabled()
        .with_expr(&start)
        .run(rules);
    let extractor = Extractor::new(&runner.egraph, AstSize);
    let (_min_cost, min_expr) = extractor.find_best(runner.roots[0]);
    let explanation = runner
        .explain_equivalence(&start, &min_expr)
        .get_flat_string();
    (min_expr, explanation)
}

[AlienKevin]

I later found a more complex example where the boolean expression is not minimized. Does this mean that I need to configure the scheduler so egg can explore more possibilities?

input expression:
(a & b & c) | (~a & b) | (~a & ~b & ~c)

minimal expression obtained through Karnaugh map:
(~a & ~c) | (b & c)

egg simplification process:
(| (| (& (& a b) c) (& (~ a) b)) (& (& (~ a) (~ b)) (~ c)))
(Rewrite=> associativity' (| (& (& a b) c) (| (& (~ a) b) (& (& (~ a) (~ b)) (~ c)))))
(| (& (& a b) c) (Rewrite=> distributivity'-rev (& (| (& (~ a) b) (& (~ a) (~ b))) (| (& (~ a) b) (~ c)))))
(| (& (& a b) c) (& (Rewrite=> combining (~ a)) (| (& (~ a) b) (~ c))))
(| (& (& a b) c) (& (~ a) (Rewrite=> involution-rev (~ (~ (| (& (~ a) b) (~ c)))))))
(| (& (& a b) c) (Rewrite<= de-morgan' (~ (| a (~ (| (& (~ a) b) (~ c)))))))
(| (& (& a b) c) (~ (| a (Rewrite=> de-morgan' (& (~ (& (~ a) b)) (~ (~ c)))))))
(| (& (& a b) c) (~ (| a (& (~ (& (~ a) b)) (Rewrite<= involution-rev c)))))
(| (& (& a b) c) (~ (| a (Rewrite=> commutativity (& c (~ (& (~ a) b)))))))
(| (& (& a b) c) (~ (| a (& c (Rewrite=> de-morgan (| (~ (~ a)) (~ b)))))))
(| (& (& a b) c) (~ (| a (& c (| (Rewrite<= involution-rev a) (~ b))))))

[oflatt]

Hi @AlienKevin
I think you have some confusion about extraction cost functions and proofs.
The extraction cost function has no influence on how many steps a proof has. Egg has a built-in algorithm for trying to minimize the number of steps in a proof using a greedy strategy, so it just tries it's best. It's an NP-hard problem to find the smallest proof.
So once you call explain_equivalence, it tries to find the smallest proof for the two terms you give it.

Also, make sure you are using the most recent version of egg (:

[AlienKevin]

@oflatt Thanks for your explanation, I got it now. However, when I tried to run explain_equivalence on a more complex example, it panicked at 'Tried to explain equivalence between non-equal terms RecExpr ...'. Though I know that they are equivalent expressions because they produce identical truth tables.

input expression:
(a & b & c) | (~a & b) | (~a & ~b & ~c)

equivalent but smaller expression:
(~a & ~c) | (b & c)

In this case, do I need to tweak the scheduler somehow to allow for a deeper search?

[oflatt]

Right, so those expressions haven't been found to be equal in the e-graph (even though you know they are). One way you can tell is if you add them both to the egraph and compare their resulting Ids.
Either you need to run your rules for longer, or you need to alter your ruleset/analysis to find they are equal more quickly.

Hope that helped

[AlienKevin]

Got it, thanks.