Где я могу найти метод преобразования произвольного логического выражения в конъюнктивную или дизъюнктивную нормальную форму?

Я написал небольшое приложение , которое анализирует выражения в абстрактные синтаксические деревья. Прямо сейчас я использую набор эвристик для выражения, чтобы решить, как лучше всего оценить запрос. К сожалению, есть примеры, которые сильно ухудшают план запроса.

Я нашел способ достоверно лучше догадываться о том, как следует оценивать запросы, но мне нужно сначала поместить свое выражение в CNF или DNF, чтобы получить доказуемо правильные ответы. Я знаю, что это может привести к потенциально экспоненциальному увеличению времени и пространства, но для типичных запросов, выполняемых моими пользователями, это не проблема.

Теперь преобразование в CNF или DNF - это то, что я все время делаю вручную, чтобы упростить сложные выражения. (Ну, может быть, не все время , но я знаю, как это делается, используя, например, законы Деморгана, законы распределения и т. Д.) Однако я не уверен, как начать переводить это в метод, который реализуемый как алгоритм. Я просмотрел статьи по оптимизации запросов, и некоторые из них начинаются со слов «сначала мы помещаем вещи в CNF» или «сначала мы помещаем вещи в DNF», и они, кажется, никогда не объясняют свой метод достижения этого.

С чего мне начать?