GMeet algorithms
October 2022. This document presents the implementation and tests ofGMeetStar
, GMeetMonoStar
, GMeetMonoLazy
and GMeetPlus
. Paper experiments:
Lattice sizes: [1,2,5,10,20,50,100,200,500]
Lattices per size: 12 (whenever possible)
Test functions per lattice: 500
Time limit: 1000 s
Lattices per size: 12 (whenever possible)
Test functions per lattice: 500
Time limit: 1000 s
GMeetStar | GMeetMonoStar | GMeetMonoLazy | GMeetPlus | DMeetPlus |
GMeetStar | GMeetMonoStar | GMeetMonoLazy | GMeetPlus | DMeetPlus |
GMeetStar | GMeetMonoStar | GMeetMonoLazy | GMeetPlus | DMeetPlus |
GMeetStar | GMeetMonoStar | GMeetMonoLazy | GMeetPlus | DMeetPlus |
Choose a lattice:
Number of elements: 8
Seed for presets: (re-click on a preset to apply)
(Running on the chosen lattice of 8 elements)
Algorithms:
Type of input function:
Algorithms:
- GMeetStar
- GMeetMonoStar
- GMeetMonoLazy
- GMeetPlus
- DMeetPlus
Type of input function:
Notation
Throughout this document we use the following notation. is a non-empty finite lattice with order and join and meet operators . The bottom element of is . The set of all endomorphisms (functions ) is denoted as , and it is a lattice with the order The join and meet operators in (i.e. and ) are the pointwise join and meet operators in . The endomorphisms that preserve least upper bounds and map to are called join-endomorphisms, and is the set of all join-endomorphisms, that is, The order for is defined as the restriction of to , and with this order, is also a lattice. The join operator coincides with (pointwise ), but the meet does not coincide with .Algorithms of reference
All the algorithms presented compute the maximal join-endomorphism below a given endomorphism.The implementations are based on the following abstract algorithms that do not indicate how to find the pairs .Implementations
Notation following variables that are used in the algorithms are present in the latticeL
and are assumed to be precomputed:
Notation:
n
is the number of nodes in the lattice.
m
is the number of edges in the Hasse diagram of the lattice.
lub[a][b]
is the join (least upper bound) of a
and b
.
glb[a][b]
is the meet (greatest lower bound).
leq[a][b]
is the boolean for .
geq[a][b]
is the boolean for .
lt[a][b]
is the boolean for .
gt[a][b]
is the boolean for .
children[b]
is the list of (direct) children of .
parents[a]
is the list of (direct) parents of . The implementation of the algorithms, including the counters is shown below. See the full code.