search

gaperez64 / acacia-bonsai

A minimal implementation of reactive synthesis via universal co-Buchi automata using antichains
GNU General Public License v3.0
4 stars 3 forks source link

improve k-d tree structure and usage #37

Closed gaperez64 closed 1 year ago

gaperez64 commented 1 year ago

We should:

  1. Make sure to choose the median while constructing the tree instead of sorting ahead of time to get better worst-case complexity.
  2. Have two cutoffs: one for when building a tree starts to pay off (something like 10 probably) and then one for when building the tree becomes too much for union to scale (something like 2^{d/2} probably). In general, cleaning the data structure and making sure that the antichain-collection template using this is also cleaner.

Another point: Make sure the tests are still up to date.

gaperez64 commented 1 year ago
  1. is done now and a pull request is pending
  2. will have to wait, I have self-benchmark.sh running and that will possibly tell us how good/bad the new version of k-d trees works and whether this is important

I cleaned a bit the tests, in particular the antichains suite which was not working anymore. @michaelcadilhac , it work now for all kdtree_backed things that use no SIMD. For some reason even the simplest checks fail with using SIMD vectors, could you try it too?

gaperez64 commented 1 year ago

latest benchmarking logs for 3 configs including new kdtrees benchs.zip

gaperez64 commented 1 year ago

@michaelcadilhac did you have a script to get a cactus plot from these logs? I remember you had automated this for the CAV/TACAS submissions but I cannot find it

michaelcadilhac commented 1 year ago

Goddamit, never realized you were hyperactive on that project! I have so many issues to catch up to!

You can find the plotting instructions there:

https://github.com/gaperez64/acacia-bonsai/blob/master/doc/tacas23/etc/Readme.txt

gaperez64 commented 1 year ago

Thanks @michaelcadilhac , it seems kdtrees now do pay! plot.pdf