Библиотека эффективных типов данных и алгоритмов
Библиотека эффективных типов данных и алгоритмов ( LEDA ) — это с собственной лицензией, библиотека программного обеспечения обеспечивающая реализации на C++ широкого спектра алгоритмов теории графов и вычислительной геометрии . [1] Первоначально он был разработан Институтом информатики Макса Планка в Саарбрюкене . [2] С 2001 года LEDA развивается и распространяется компанией Algorithmic Solutions Software GmbH.
LEDA доступна в бесплатной, исследовательской и профессиональной версиях. Бесплатная версия является бесплатной , с доступом к исходному коду, который можно приобрести. Редакции Research и Professional требуют уплаты лицензионных сборов за любое использование. С октября 2017 года графовые алгоритмы LEDA доступны и для среды разработки Java .
Технические детали
[ редактировать ]Типы данных
[ редактировать ]Числовые представления
[ редактировать ]LEDA предоставляет четыре дополнительных числовых представления помимо встроенных в C++: integer
, rational
, bigfloat
, и real
:
- светодиоды
integer
type предлагает улучшение по сравнению со встроеннымint
datatype, устраняя проблему переполнения за счет неограниченного использования памяти для все более больших чисел. - Отсюда следует, что компания LEDA
rational
тип имеет такую же устойчивость к переполнению, поскольку он основан непосредственно на математическом определении рационального как отношения двухinteger
с. - The
bigfloat
type улучшает типы с плавающей запятой в C++, позволяя устанавливать мантиссу (также обычно называемую мантиссой) с произвольным уровнем точности вместо того, чтобы следовать стандарту IEEE . - светодиоды
real
type позволяет точно представлять действительные числа и может использоваться для вычисления знака радикального выражения. [1]
Проверка ошибок
[ редактировать ]LEDA использует алгоритмы сертификации , чтобы продемонстрировать, что результаты функции математически верны. В дополнение к входным и выходным данным функции, LEDA вычисляет третье значение «свидетеля», которое можно использовать в качестве входных данных для программ проверки для проверки выходных данных функции. Программы проверки LEDA были разработаны на Simpl, императивном языке программирования , и проверены с использованием Isabelle/HOL , программного инструмента для проверки правильности математических доказательств. [3]
Характер значения свидетеля часто зависит от типа выполняемых математических вычислений. Для функции проверки планарности LEDA, если граф планарный комбинаторное вложение , в качестве свидетеля создается . Если нет, подграф Куратовского возвращается . Эти значения затем можно передать непосредственно функциям проверки для подтверждения их достоверности. Разработчику нужно только понять внутреннюю работу этих функций проверки, чтобы быть уверенным в правильности результата, что значительно сокращает кривую обучения по сравнению с получением полного понимания алгоритма тестирования планарности LEDA. [4]
Варианты использования
[ редактировать ]LEDA полезна в области вычислительной геометрии благодаря поддержке точного представления действительных чисел с помощью leda_real
тип данных. Это обеспечивает преимущество в точности по сравнению с арифметикой с плавающей запятой . Например, расчеты с участием радикалов становятся значительно более точными, если их вычислять с использованием leda_real
. Алгоритмы, такие как параметрический поиск , метод решения подмножества задач оптимизации и другие, в рамках модели вычислений с реальной оперативной памятью, полагаются на параметры действительных чисел для получения точных результатов. [5]
Альтернативы
[ редактировать ]Boost и LEMON — потенциальные альтернативные библиотеки с некоторыми преимуществами в эффективности за счет различных реализаций фундаментальных алгоритмов и структур данных. Однако ни один из них не использует аналогичный набор проверок правильности, особенно при работе с арифметикой с плавающей запятой. [3]
Ссылки
[ редактировать ]- ^ Перейти обратно: а б Мельхорн, Курт; Нэхер, Стефан (1999), LEDA: платформа для комбинаторных и геометрических вычислений , издательство Кембриджского университета, ISBN 978-0-521-56329-1 .
- ^ «LEDA — Библиотека эффективных типов данных и алгоритмов» . Университет Стоуни-Брук . Проверено 21 февраля 2019 г.
- ^ Перейти обратно: а б Абдулазиз, Мохаммед; Мельхорн, Курт; Нипков, Тобиас (2019). «Надежные графовые алгоритмы». В Россманите, Питер; Хеггернес, Пинар; Катоен, Йост-Питер (ред.). 44-й Международный симпозиум по математическим основам информатики, MFCS 2019, 26-30 августа 2019 г., Ахен, Германия . ЛИПики. Том 138. Замок Дагштуль - Центр информатики Лейбница. стр. 1:1–1:22. arXiv : 1907.04065 . doi : 10.4230/LIPIcs.MFCS.2019.1 .
- ^ Мельхорн, Курт; Нэхер, Стефан (1998), Брим, Любош; Грушка, Йозеф; Златушка, Иржи (ред.), «От алгоритмов к рабочим программам: об использовании проверки программ в LEDA» , Математические основы информатики, 1998 , том. 1450, Springer Berlin Heidelberg, стр. 84–93 , doi : 10.1007/bfb0055759 , ISBN 978-3-540-64827-7 , получено 22 ноября 2019 г.
- ^ Мельхорн, Курт; Ширра, Стефан (2001). «Точные вычисления с помощьюleda_real — приложения теории и геометрии» (PDF) . Символьные алгебраические методы и методы проверки . Вена: Springer Verlag. стр. 163–172. дои : 10.1007/978-3-7091-6280-4_16 . ISBN 978-3-211-83593-7 .