Проект по дискретной математике.

Постановка задачи: Прочесть булеву формулу, преобразовать её в КНФ и проверить формулу на выполнимость.

Программа принимает булеву формулу, которая содержит

1. Переменные.
2. Операторы \/, /\, <->, ->, ~
3. Скобки.

Переменные могут задаваться произвольной строкой латинского алфавита. Программа поддерживает не более 31 различных переменных в одном выражении.

Задача выполняется следующими шагами.

1. С помощью конечного автомата выражение разбивается на токены.
2. С помощью автомата с магазинной памятью выражение проверяется, является ли набор токенов формулой. Например, строка "(((" пройдет первый шаг, потому что строка состоит из правильных токенов, но не пройдет второй, потому что строка не является формулой.
3. Формула приводится к обратной польской нотации (постфиксной нотации)
4. По формуле строится дерево выражения.
5. В дерево выражения подставляются все возможные значение переменных, строится таблица истинности и по ней строится СКНФ. С помощью таблицы истинности происходит проверка на выполнимость.