mmj2 compact representation for $d statements

[Glauco]

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

[Benoit]

Did you try searching things like "search complete subgraphs" ?

Benoît

[Mario Carneiro]

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.

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3692a051-5119-481c-b21a-250c13f99a3dn%40googlegroups.com.

[Mario Carneiro]

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.

[Glauco]

Thanks Benoit and Mario,

it looks like we've plenty of algorithms to chose from. I'm going to do some research and pick one.

Glauco