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

Бинарная диаграмма решений (БДР) представляет собой бесконтурный орграф с выдеренной вершиной и не более чем двумя стоками, один из которых имеет метку 0, а другой – метку 1. Вершины, не являющиеся стоками, помечены переменными. Каждая вершина, не являющаяся стоком, имеет две исходящих дуги; одна из них имеет метку 1 и ведет к 1-потомку, другая имеет метку 0 и ведет к 0-потомку. Переменные должны быть упорядочены; иначе говоря, если переменная-метка xi появляется раньше метки xj на некотором пути из вершины к стоку, тогда метка xj не может встречаться до xi ни на одном пути из вершины к стоку. Две вершины являются изоморфными, если обе являются стоками с одинаковой меткой либо представляют собой вершины, не являющиеся стоками, с одной и той же переменной-меткой, причем их 0-потомки и 1-потомки изоморфны. Чтобы бесконтурный орграф был допустимой БДР, необходимо, чтобы в нем не было изоморфных вершин и чтобы никакие вершины не имели одинаковых 0-потомков и 1-потомков.

Основной результат теории БДР заключается в следующем: если дано фиксированное упорядочение переменных, то представление является уникальным с точностью до изоморфизма. Иначе говоря, если F и G являются БДР, представляющими f: {0, 1}<math>^n</math> <math>\mapsto</math> {0, 1} с порядком переменных x1 <math>\prec</math> x2 <math>\prec</math> ... xn, то F и G являются изоформными.

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