Данный солвер строит граф ROBDD по логическому выражению. Решение выдается в требуемом для курса формате.

Поддерживаемые операторы приведены в таблице ниже в порядке возрастания приоритета.

Оператор	Импликация	Исключающее ИЛИ	Дизъюнкция	Конъюнкция	Отрицание
Запись	->	+	|	&	!

В качестве имени переменной можно использовать любую комбинацию латинских букв и цифр, за исключением букв X, F, G, U, W, R.

Можно использовать любые скобки в выражении - фигурные, квадратные и круглые. Выражения в скобках вычисляются с наивысшим приоритетом.

Пример формулы: (x2 & !y2) | (!(x2 + y2) & ((x1 & !y1) | (!(x1 + y1) & (x0 & !y0)))).

Для построения ROBDD необходимо указать порядок переменных, по которому будет производится подстановка значений. В случае, если порядок не указан, им будет порядок появления переменных в формуле.

В случае, если в условии формула задана косвенно (например: старший бит трехбитного сложения x₂x₁x₀ + y₂y₁y₀), то булеву формулу для него можно взять из выпадающего списка в окне ввода формулы.