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

Question

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

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

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

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

Answer 1

Посмотрите на https://github.com/bastikr/boolean.py Пример:

def test(self):
    expr = parse("a*(b+~c*d)")
    print(expr)

    dnf_expr = normalize(boolean.OR, expr)
    print(list(map(str, dnf_expr)))

    cnf_expr = normalize(boolean.AND, expr)
    print(list(map(str, cnf_expr)))

Вывод:

a*(b+(~c*d))
['a*b', 'a*~c*d']
['a', 'b+~c', 'b+d']

ОБНОВЛЕНИЕ : Теперь я предпочитаю это sympyлогический пакет :

>>> from sympy.logic.boolalg import to_dnf
>>> from sympy.abc import A, B, C
>>> to_dnf(B & (A | C))
Or(And(A, B), And(B, C))
>>> to_dnf((A & B) | (A & ~B) | (B & C) | (~B & C), True)
Or(A, C)

Answer 2

Наивный ванильный алгоритм для формул без квантификаторов:

• для CNF, преобразование в нормальную форму отрицания с законами де Моргана, затем распределение ИЛИ по И
• для DNF, конвертируйте в нормальную форму отрицания с законами Де Моргана, затем распределите И по ИЛИ

Мне неясно, количественно ли определены ваши формулы.Но даже если это не так, кажется, конец статей в Википедии о конъюнктивной нормальной форме , и ее - примерно эквивалент в мире автоматизированных доказательств теорма - клаузальной нормальной форме альтер эгообрисовать в общих чертах используемый алгоритм (и указать ссылки, если вы хотите сделать это преобразование немного более умным).Если вам нужно больше, пожалуйста, расскажите нам больше о том, где вы столкнулись с трудностями.

Answer 3

Я сталкивался с этой страницей: Как преобразовать формулу в CNF .Он показывает алгоритм для преобразования логического выражения в CNF в псевдокоде.Помог мне начать работу в этой теме.