Бинарный граф решений: различия между версиями

Перейти к навигации Перейти к поиску
Строка 46: Строка 46:


Определение изоморфизма напрямую дает нам рекурсивный алгоритм проверки на изоморфизм. Однако он имеет экспоненциальную по отношению к числу узлов сложность; это можно проиллюстрировать, в частности, при помощи проверки изоморфизма БДР для функции четности относительно ее самой. Экспоненциальная сложность связана с постоянно возникающими проверками на изоморфизм между парами вершин; решение может быть найдено в динамическом программировании. Кэширование проверок на изоморфизм снижает сложность этих проверок до O(|F| <math>\cdot </math> |G|), где |B| обозначает количество вершин в БДР B.
Определение изоморфизма напрямую дает нам рекурсивный алгоритм проверки на изоморфизм. Однако он имеет экспоненциальную по отношению к числу узлов сложность; это можно проиллюстрировать, в частности, при помощи проверки изоморфизма БДР для функции четности относительно ее самой. Экспоненциальная сложность связана с постоянно возникающими проверками на изоморфизм между парами вершин; решение может быть найдено в динамическом программировании. Кэширование проверок на изоморфизм снижает сложность этих проверок до O(|F| <math>\cdot </math> |G|), где |B| обозначает количество вершин в БДР B.


'''Операции с БДР'''
'''Операции с БДР'''


Многие логические операции при использовании БДР могут быть реализованы за полиномиальное время: их примерами являются bdd_and, которая вычисляет БДР, представляющую логическое сложение AND функций, представленных двумя БДР, bdd_or и bdd_not определяются аналогичным образом для OR и NOT; bdd_compose принимает БДР, представляющие функции f и g, и переменную v и возвращает БДР для f, в которой v заменена на g.
Многие логические операции при использовании БДР могут быть реализованы за полиномиальное время: их примерами являются bdd_and, которая вычисляет БДР, представляющую логическое сложение AND функций, представленных двумя БДР, bdd_or и bdd_not определяются аналогичным образом для OR и NOT; bdd_compose принимает БДР, представляющие функции f и g, и переменную v и возвращает БДР для f, в которой v заменена на g.
Пример bdd_and был выбран не случайно: он основан на тождестве f g = x (fx • gx) + x’ • (fx’ • gx’). Рекурсия может быть реализована напрямую: основными являются ситуации, когда либо f, либо g равны 0, и когда одно или оба значения равны 1. Рекурсивный процесс выбирает переменную v, являющуюся меткой корня БДР либо для f, либо для g, в зависимости от того, что из них идет раньше по порядку переменных, и, рекурсивно вычисляет БДР для fv • gv и fv' • gv'; если они изоморфны, выполняется их слияние. Пусть дана БДР F для f. Если v – переменная, служащая меткой корня F, то БДР для fv’ и fv представляют собой просто 0-потомка и 1-потомка корня F, соответственно.
 
Пример bdd_and был выбран не случайно: он основан на тождестве <math>f \cdot g = x \cdot (f_x \cdot g_x) + x' \cdot (f_{x'} \cdot g_{x'})</math>. Рекурсия может быть реализована напрямую: основными являются ситуации, когда либо f, либо g равны 0, и когда одно или оба значения равны 1. Рекурсивный процесс выбирает переменную v, являющуюся меткой корня БДР либо для f, либо для g, в зависимости от того, что из них идет раньше по порядку переменных, и, рекурсивно вычисляет БДР для <math>f_v \cdot g_v</math> и <math>f_{v'} \cdot g_{v'}</math>; если они изоморфны, выполняется их слияние. Пусть дана БДР F для f. Если v – переменная, служащая меткой корня F, то БДР для <math>f_{v'} \, </math> и <math>f_v \, </math> представляют собой просто 0-потомка и 1-потомка корня F, соответственно.
 
Реализация bdd_and вышеописанным способом имеет экспоненциальную сложность из-за постоянного возникновения новых подзадач. Динамическое программирование вновь может стать вариантом решения этой проблемы: кэширование промежуточных результатов bdd_and снижает сложность до O(|F| • |G|).
Реализация bdd_and вышеописанным способом имеет экспоненциальную сложность из-за постоянного возникновения новых подзадач. Динамическое программирование вновь может стать вариантом решения этой проблемы: кэширование промежуточных результатов bdd_and снижает сложность до O(|F| • |G|).


'''Упорядочение переменных'''
'''Упорядочение переменных'''
4551

правка

Навигация