The implementation in mmj2 is here: https://github.com/digama0/mmj2/blob/master/src/mmj/lang/ScopeFrame.java#L154-L294
It does not use the same algorithm as mm-web-rs. I don't have any particular insights regarding the theoretical properties of the mmj2 algorithm. On Sun, Apr 2, 2023 at 9:59 PM Mario Carneiro <di.g...@gmail.com> wrote: > I recently implemented a variation on this algorithm for mm-web-rs: > https://github.com/digama0/mm-web-rs/blob/master/src/render.rs#L1026-L1077 > > As the function name suggests, the thing to google is "clique cover". It > is an NP hard problem, but there are some okay approximations. > > On Sun, Apr 2, 2023 at 1:39 PM Benoit <benoit.ju...@gmail.com> wrote: > >> Did you try searching things like "search complete subgraphs" ? >> >> Benoît >> >> On Sunday, April 2, 2023 at 1:44:45 PM UTC+2 Glauco wrote: >> >>> What's the algorithm used by mmj2 to represent $d pairs as $d sets ? >>> >>> For instance, for a given theorem, with yamma I'm producing >>> >>> $d ph x $. $d k x $. $d k ph $. $d j x $. $d j k $. >>> $d F x $. $d F k $. $d A x $. $d A k $. $d A j $. >>> >>> whereas mmj2 produces >>> >>> $d A j k x $. $d F k x $. $d k ph x $. >>> >>> (from 'visual' inspection, they actually represent the same relation) >>> >>> I've googled for 'compact representation of symmetric relations' and >>> stuff like that, but no luck, so far. >>> >>> Can anybody point me in the right direction. >>> >>> Thanks in advance >>> Glauco >>> >> -- >> You received this message because you are subscribed to the Google Groups >> "Metamath" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to metamath+unsubscr...@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/metamath/3692a051-5119-481c-b21a-250c13f99a3dn%40googlegroups.com >> <https://groups.google.com/d/msgid/metamath/3692a051-5119-481c-b21a-250c13f99a3dn%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsUqHxiC6FXLGhRW1CLGCmta7zXdaFnD_PAFXJH98_Ghg%40mail.gmail.com.
