Hi jagra, starting from an uncompressed proof, you can compress it in several different ways, depending on how you order the labels. There's not a spec for how you order the labels. Yamma's configuration allows you to choose between three ordering algorithms: fifo mostReferencedFirst mostReferencedFirstAndNiceFormatting
it may be fifo is the most "natural": it keeps the order of the uncompressed proof (but it leads to much longer proofs, w.r.t. the other "optimized" options) by default, yamma uses mostReferencedFirstAndNiceFormatting it produces proofs that have the EXACT same LENGTH as those produced by mmj2 (I can't prove it, but I've checked it on the longest proofs in set.mm) The proofs produced by mmj2 are not exactly the same, because (in my opinion) mmj2 has a small bug in the knapsack algorithm Since the knapsack is only applied on subgroups of labels which are referred by "numbers" (capital letter strings) of the same length, a different order in these subgroups does not affect the overall length of the compressed proof. Thus, yamma and mmj2 produce proofs of the same length (yamma's proofs could sometimes have a better formatting) You can find the code for this specific algorithm in this file https://github.com/glacode/yamma/blob/master/server/src/mmp/proofCompression/MmpSortedByReferenceWithKnapsackLabelMapCreator.ts IMHO, metamath.exe and mmj2 don't produce the same compressed proofs (I've shown several examples, in the past) -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f687d4b6-412f-4be0-92b8-4d92dd893277n%40googlegroups.com.
