Biblioteka efektywnych typów danych i algorytmów

Library of Efficient Data types and Algorithms ( LEDA ) to licencjonowana biblioteka oprogramowania zawierająca implementacje C++ szerokiej gamy algorytmów dla teorii grafów i geometrii obliczeniowej . Pierwotnie został opracowany przez Instytut Informatyki im. Maxa Plancka w Saarbrücken . Od 2001 roku LEDA jest dalej rozwijana i dystrybuowana przez firmę Algorithmic Solutions Software GmbH.

LEDA jest dostępna w wersji bezpłatnej, badawczej i profesjonalnej. Bezpłatna edycja jest bezpłatna , z możliwością zakupu kodu źródłowego. Wersje Research i Professional wymagają uiszczenia opłat licencyjnych za dowolne użycie. Od października 2017 r. algorytmy graficzne LEDA są również dostępne dla środowiska programistycznego Java .

Szczegóły techniczne

Typy danych

Reprezentacje numeryczne

LEDA zapewnia cztery dodatkowe reprezentacje numeryczne obok tych wbudowanych w C++: integer , racjonalne , bigfloat i real :

  • całkowity LEDA oferuje ulepszenie w stosunku do wbudowanego typu danych int , eliminując problem przepełnienia kosztem nieograniczonego wykorzystania pamięci dla coraz większych liczb.
  • wymierny LEDA ma taką samą odporność na przepełnienie, ponieważ opiera się bezpośrednio na matematycznej definicji wymiernego jako ilorazu dwóch liczb całkowitych s.
  • bigfloat udoskonala typy zmiennoprzecinkowe C++, umożliwiając ustawienie mantysy na dowolny poziom precyzji zamiast przestrzegania standardu IEEE .
  • rzeczywisty LEDA pozwala na precyzyjną reprezentację liczb rzeczywistych i może być użyty do obliczenia znaku radykalnego wyrażenia.

Sprawdzanie błędów

LEDA korzysta z algorytmów certyfikujących , aby wykazać, że wyniki funkcji są matematycznie poprawne. Oprócz danych wejściowych i wyjściowych funkcji, LEDA oblicza trzecią wartość „świadka”, której można użyć jako danych wejściowych do programów sprawdzających w celu sprawdzenia poprawności danych wyjściowych funkcji. imperatywnym języku programowania Simpl i zweryfikowane przy użyciu programu Isabelle/HOL , służącego do sprawdzania poprawności dowodów matematycznych.

Charakter wartości świadka często zależy od rodzaju wykonywanych obliczeń matematycznych. W przypadku funkcji testowania planarności LEDA, jeśli wykres jest planarny , jako świadek tworzone jest osadzanie kombinatoryczne . Jeśli nie, zwracany jest podgraf Kuratowskiego . Wartości te można następnie przekazać bezpośrednio do funkcji sprawdzających, aby potwierdzić ich poprawność. Deweloper musi tylko zrozumieć wewnętrzne działanie tych funkcji sprawdzających, aby mieć pewność, że wynik jest poprawny, co znacznie skraca krzywą uczenia się w porównaniu do pełnego zrozumienia algorytmu testowania planarności LEDA.

Przypadków użycia

LEDA jest przydatna w dziedzinie geometrii obliczeniowej ze względu na obsługę dokładnej reprezentacji liczb rzeczywistych za pomocą typu danych leda_real . Zapewnia to przewagę dokładności nad arytmetyką zmiennoprzecinkową . Na przykład obliczenia obejmujące pierwiastki są znacznie dokładniejsze, gdy są obliczane przy użyciu leda_real . Algorytmy, takie jak wyszukiwanie parametryczne , technika rozwiązywania podzbioru problemów optymalizacyjnych i inne w rzeczywistej pamięci RAM model obliczeniowy opiera się na parametrach liczb rzeczywistych w celu uzyskania dokładnych wyników.

Alternatywy

Boost i LEMON to potencjalne alternatywne biblioteki z pewnymi korzyściami w zakresie wydajności dzięki różnym implementacjom podstawowych algorytmów i struktur danych. Jednak żaden z nich nie stosuje podobnego zestawu sprawdzania poprawności, szczególnie w przypadku arytmetyki zmiennoprzecinkowej.

Linki zewnętrzne


Pobrano z „ https://en.wikipedia.org/w/index.php?title=Library_of_Efficient_Data_types_and_Algorithms&oldid=1103353644 ”