Recognizing when two arithmetic expressions are essentially the same

How would a therom prover like z3 handle this, out of interest? Isn't it the ideal domain for it?

I think the difficulty is in defining the relation, rather than proving it. The problems are so small that it probably doesn't matter how you actually prove equivalence, once you've defined it.

Within its domain, that's what the Oppen-Nelson simplifier did. Many provers since can do that.

Amusingly, Plato, the first on-line teaching system, had a solver for that. It was used to check student's answers to math problems. It worked by plugging in some random numeric values and evaluating. If many sets of random values evaluated the same as the desired answer, it was accepted as equivalent.

Thank you for sharing! A closely related puzzle was previously discussed at:

https://news.ycombinator.com/item?id=14400017

The present puzzle can be seen as a natural continuation of this earlier thread, and the declarative programming language Prolog is again well-suited for this puzzle.

For example, we can start with a short Prolog program that exhaustively generates all solutions:

    numbers_tree([N], leaf(N)).
    numbers_tree(Vs0, binary(Left, Right)) :-
            permutation(Vs0, Vs),
            append([L|Ls], [R|Rs], Vs),
            numbers_tree([L|Ls], Left),
            numbers_tree([R|Rs], Right).

    tree_op_expr_value(leaf(N), _, number(N), N).
    tree_op_expr_value(binary(Left0, Right0), Op, expr(Op,Left,Right), Value) :-
            tree_op_expr_value(Left0, _, Left, VL),
            tree_op_expr_value(Right0, _, Right, VR),
            op_values_value(Op, VL, VR, Value).

    op_values_value(+, A, B, V) :- V is A + B.
    op_values_value(-, A, B, V) :- V is A - B.
    op_values_value(×, A, B, V) :- V is A * B.
    op_values_value(÷, A, B, V) :- B =\= 0, V is A rdiv B.

We can query it like this:

    ?- numbers_tree([4,6,6,6], T),
       tree_op_expr_value(T, _, Expr, 24).

On backtracking, it generates all solutions, reported as abstract syntax trees Expr.

This is of course not yet the full task. And I won't solve the full task here, because I would like to give others a chance to also have a look. However, I post a hint towards an efficient solution:

In such cases where you want to detect whether something is "essentially the same", consider applying a notion from term rewriting: In term rewriting, we apply rewrite rules, and in strongly normalizing systems, each term has a so-called normal form, which is its canonical representation.

Thus, in the language of term rewriting, when trying to decide if two terms are "essentially the same", you can reduce both of them to their respective normal forms, and then compare the normal forms! The two original terms are the same iff their normal forms are the same.

Here is part of the term rewriting system I have come up with for this task, implemented in Prolog:

    commutative(+).
    commutative(×).

    expr_normal_form(number(N), number(N)).
    expr_normal_form(expr(Op,A0,B0), expr(Op,A,B)) :-
            commutative(Op),
            expr_comparison(A0, B0, Comp),
            smaller_first(Comp, A0, B0, A, B).
    expr_normal_form(expr(Op,A0,B0), expr(Op,A,B)) :-
            \+ commutative(Op),
            expr_normal_form(A0, A),
            expr_normal_form(B0, B).

    smaller_first(=, A0, B0, A, B) :-
            expr_normal_form(A0, A),
            expr_normal_form(B0, B).
    smaller_first(, A0, B0, A, B) :- smaller_first().
    expr_comparison(Expr, Expr, =).
    expr_comparison(expr(Op1, _, _), expr(Op2, _, _), C) :-
            dif(Op1, Op2),
            compare(C, Op1, Op2).
    expr_comparison(expr(Op,A0,B), expr(Op,A,B), C) :-
            dif(A0, A),
            expr_comparison(A0, A, C).
    expr_comparison(expr(Op,A,B0), expr(Op,A,B), C) :-
            dif(B0, B),
            expr_comparison(B0, B, C).

It works by imposing an order on terms, and recursively rewriting a single term to its normal form, which is smaller than or equal to the original term according to that (self-imposed) order.

We can now use an additional predicate like the following to collect all solutions, remove duplicates, then rewrite each solution to its respective normal form, and then remove duplicates again:

    all_expressions(Ls, Value, Exprs) :-
            findall(Expr, (numbers_tree(Ls, T),
                           tree_op_expr_value(T, _, Expr, Value)), Exprs0),
            sort(Exprs0, Exprs1),
            maplist(expr_normal_form, Exprs1, Exprs2),
            sort(Exprs2, Exprs).

For example, in the [4,6,7,9] = 24 case, this algorithm reduces the expressions to 5 solutions:

    ?- all_expressions([4,6,7,9], 24, Exprs),
       maplist(portray_clause, Exprs),
       length(Exprs, L).
    expr(×, number(6), expr(÷, expr(+, number(7), number(9)), number(4))).
    expr(×, expr(+, number(7), number(9)), expr(÷, number(6), number(4))).
    expr(÷, number(6), expr(÷, number(4), expr(+, number(7), number(9)))).
    expr(÷, expr(+, number(7), number(9)), expr(÷, number(4), number(6))).
    expr(÷, expr(×, number(6), expr(+, number(7), number(9))), number(4)).
    Exprs = [...],
    L = 5 .

I leave adding more rewrite rules as a challenge.

It's kindof funny zmonx, whenever there is a challenge that I think "oh I can do this with a SAT solver", you've already shown up and solved it with Prolog.

I think you've gone for the more 'expressive' variant here. If I were writing SMTLIB directly or using an API, I'd prove the assertion that any possible parenthization is eqv by enumerating & checking them individually :)