Главная       Библиотека      Перечень ссылок      Диссертация       Отчет о поиске

Диссертация

Поляков Андрей Николаевич

по теме "Исследование параллельных методов символического моделирования и верификации"


Бинарная алгебра представляет собой краеугольный камень компьютерной науки и разработки цифровых систем. Большинство проблем в разработке и тестировании цифровой логики, искусственного интеллекта, и комбинаторики могут быть выражены как последовательность операций с бинарными функциями. Использование этих методов является эффективным алгоритмом для представления и манипуляции бинарными функциями символически. К сожалению, многие задачи, которые хотелось бы представить в виде бинарной функции, являются NP-сложными задачами. Следовательно, все известные подходы для представления этих операций потребуют, в худшем случае, машинного времени, величина которого растет экспоненциально в зависимости от размера задачи. В этом и состоит сложность оценки эффективности различных методов представления и манипуляции Бинарных функций. В худшем случае, все известные подходы представления также малоэффективны как и простой подход представления функции с помощью таблиц истинности. На практике, использование более эффективные представления и манипуляционные алгоритмы, мы можем избежать экспоненциальных расчетов.

Множество методов были разработаны для представления и манипуляции бинарными функциями. Основанные на классическом представлении с помощью таблиц истинности: карты Карно, или каноническая форма sum-of-product являются довольно непрактичными, т.к. каждая функция n аргументов требует размерность представления 2n или более. Более практично использовать представления которые, по крайней мере для многих функций, не имеют экспоненциальную сложность. Пример такого представления включает в себя пониженную сумму продуктов (элементов) (или эквивалентную множеству простых кубов) и приведен к виду однородной функции. Но у этих методов есть и ряд недостатков. Во-первых, остаются все же функции которые требуют экспоненциальную сложность представления. Например, функции «четность» и «нечетность» являются худшим примером во всех этих представлениях. Второе, в то время как некоторые функции имеют смысл в таком представлении, производя простые операции такие как комплементация могут произвести функцию с экспоненциальной сложностью представления. В конце концов, ни одно из этих представлений не дает каноническую форму, т.е., исходная функция может иметь несколько представлений. Следовательно, тестирования на эквивалентность и выполнимость могут быть довольно трудоемкими.

В результате этих характеристик, большинство программ работающих с последовательностью операций с бинарными функциями имеют скорее хаотичное поведение. Они движутся с нормальным шагом, но в конце концов «взрываются», толи выходят за пределы области расчета или невозможность продолжения просчета с соизмеримыми затратами времени.

В этой статье мы представляем новый класс алгоритмов для манипуляции с бинарными функциями представленными в виде направленного нецикличного графа. Это преставление похоже на бинарную диаграмму решений представленную Лии и в дальнейшем описанной Акерсом. Тем не менее, мы положили дальнейшее ограничение на расположение результативных переменных – вертикально. Эти ограничения позволяют более эффективно разрабатывать алгоритмы манипуляции представлений.

Наши представления имеют ряд преимуществ по сравнению с предыдущими подходами манипуляции с бинарными функциями. Во-первых, большинство общих встречающихся функций имеют приемлемое представление. Например, все симметричные функции (включая «четность» и «нечетность») представлены графами где количество узлов равно квадрату количества аргументов. Во-вторых, представление программы основанной на наших алгоритмах, когда обработка последовательности операций ухудшается медленно, если вообще. Временная сложность любой простой операции ограничена размером графа для функции с которой мы работаем. Например, вычисление функции требует время пропорциональное размеру графа, в то время как комбинирование двух бинарных функций (такие как конъюнкция, вычитание, и импликация – это отдельные случаи) требует времени пропорционально двум размерам графа. Наконец, наше представление является канонической формой упрощенного графа, т.е. каждая функция имеет уникальное представление. Отсюда, …

К сожалению наше представление не имеет своего множества нежелательных характеристик. Прежде всего мы должны определится с порядком единых входных параметров в качестве аргументов для всех представляемых функций. Для некоторых функций размер графа представляющего функцию очень чувствителен к этому порядку. Проблема вычисления порядка минимизации графа является NP-сложной задачей. Наш опыт, тем не менее, показывает, что человек понимающий проблему, может выбрать подходящий метод без такой большой сложности. Похоже что использование маленького множества эвристик может привести к тому, что программа сама сможет выбрать адекватный метод. Более того, есть несколько функций, которые могут быть представлены бинарными выражениями или логическими сетями разумного размера, но для всех входных последовательностей представление в виде функционального графа слишком большое для использование на практике. Например, мы доказали в приложении, что функции описывающие результат целочисленного умножения представляются графом, размер которого растет экспоненциально независимо от входных последовательностей. Если не рассматривать целочисленное умножение, наш опыт показывает, что такие функции редко появляются в приложениях. Для других классов проблем, особенно в комбинаторике, наши методы практичны только в ограниченных условиях.

Многообразие графического представления дискретных функций в настоящий момент интенсивно исследуется. Ряд литературы по этому разделы представлен сайтами Морета, содержащими более 100 ссылок, но ни одна не описывает алгоритм для составления программы управления бинарными функциями. К счастью, Гопкрофт и Шмидт изучили свойства графов используя ограничения похожие на наши, и показали что два графа могут быть проверены на функциональную эквивалентность за полиномиальное время, и что некоторые функции потребуют граф большего размера при таких ограничениях, чем при более мягких ограничениях. Пейн описал технику похожую на нашу….


Главная       Библиотека      Перечень ссылок      Диссертация