9, Саратов, Россия, 410012 Булевы базисы Грёбнера проявили свою практическую применимость для ряда задач, таких как HFE (Hidden Field Equations) в криптографии, моделирование квантовых вычислений и к задаче «Выполнимость» для конъюнктивной нормальной формы. <...> Алгоритмы построения базисов Грёбнера имеют экспоненциальную сложность построения как по времени выполнения, так и по требуемой памяти. <...> Для более компактного хранения булевых многочленов было предложено использовать ZDD-диаграммы. <...> Показана связь ZDD-диаграмм с специальным видом рекурсивным представлением многочленов, которое отождествляет ZDD-диаграмму с некоторым набором равенств. <...> Доказана лемма дающая число вершин в ZDD-диаграмме для представления булевого многочлена, состоящего из всех мономов до степени d включительно. <...> В состав пакета входят собственная реализация красно-чёрных деревьев, списков и менеджера памяти. <...> Пакет разрабатывался для использования как внутреннее представление булевых многочленов, в ней реализованы операции сложения и умножение двух многочленов, а также умножение на переменную, которое используются при построении инволютивных базисов Грёбнера. <...> Ключевые слова: булевы многочлены, бинарная диаграмма решений, базис Грёбнера, задача «Выполнимость». <...> Введение Двоичные диаграммы решений (Binary Decision Diagram, BDD) [1] являются удобным инструментом представления и оперирования булевыми функциями и широко используются в различных областях, например для формальной верификации программных и аппаратных систем. <...> Двоичные диаграммы решений — это направленный ацикличный граф с двумя терминальными узлами {0, 1}, которые соответствуют значениям представляемой булевой функции. <...> Все остальные вершины имеют выходную степень 2 и называются узлами решений. <...> Одна вершина имеет входную степень, равную 0, эта вершина является корнем. <...> Рёбра, выходящие из узлов решений, соответствуют значению 0 (0-ребро, else-ребро) или 1 (1-ребро, then-ребро) для соответствующей <...>