3 ms·
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
by ZephyrP 9y ago
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 :)
- zmonx 9y agoThis may get out of hand: The task asks not only for all parenthesizations, but also other equivalence classes. The rewrite rules and Prolog in general let you express the equivalence classes reasonably concisely and efficiently. I'm still always interested also in other approaches, and greatly enjoy your SAT solutions!