4551
правка
Бинарный граф решений: различия между версиями
Перейти к навигации
Перейти к поиску
→Экспериментальные результаты
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
| Строка 74: | Строка 74: | ||
== Экспериментальные результаты == | == Экспериментальные результаты == | ||
Брайант исследовал возможность проверки двух качественно различных схем для сложения. Ему удалось проверить эквивалентность двух 64-битных сумматоров на VAX 11/780 (компьютере с одним MIP) за 95,8 минут. При этом он использовал выведенное вручную упорядочение. | Брайант исследовал возможность проверки двух качественно различных схем для сложения. Ему удалось проверить эквивалентность двух 64-битных сумматоров на VAX 11/780 (компьютере с одним MIP) за 95,8 минут. При этом он использовал выведенное вручную упорядочение. | ||
Современные БДР-пакеты работают на два порядка величины быстрее, чем первая реализация Брайанта. Одним из источников усовершенствования было использование строгой канонической формы, в которой поддерживается глобальная база данных вершин БДР, и ни одна новая вершина не может быть добавлена без проверки, не существует ли уже в базе данных вершины с той же меткой и теми же 0-потомком и 1-потомком [3]. (Для этого требуется, чтобы потомки любой добавляемой вершины также находились в строгой канонической форме). Другими путями к повышению производительности были использование дополнительных указателей (если у указателя установлен наименьший значащий бит, он ссылается на дополнение функции), лучшее управление памятью (сборка мусора на базе счетчиков ссылок, хранение часто используемых вершин в памяти поблизости друг от друга), улучшенные хэш-функции и лучшая организация таблицы вычисленных результатов (в которой отслеживаются подзадачи, уже встреченные ранее) [16]. | |||
Современные БДР-пакеты работают на два порядка величины быстрее, чем первая реализация Брайанта. Одним из источников усовершенствования было использование [[строгая каноническая форма|строгой канонической формы]], в которой поддерживается глобальная база данных вершин БДР, и ни одна новая вершина не может быть добавлена без проверки, не существует ли уже в базе данных вершины с той же меткой и теми же 0-потомком и 1-потомком [3]. (Для этого требуется, чтобы потомки любой добавляемой вершины также находились в строгой канонической форме). Другими путями к повышению производительности были использование дополнительных указателей (если у указателя установлен наименьший значащий бит, он ссылается на дополнение функции), лучшее управление памятью (сборка мусора на базе счетчиков ссылок, хранение часто используемых вершин в памяти поблизости друг от друга), улучшенные хэш-функции и лучшая организация таблицы вычисленных результатов (в которой отслеживаются подзадачи, уже встреченные ранее) [16]. | |||
'''Наборы данных''' | '''Наборы данных''' | ||