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

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

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

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

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


query-optimization algorithm boolean-expression
person Billy ONeal    schedule 03.11.2011    source источник

Ответы (3)


arrow_upward
9
arrow_downward

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

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

person Francois G    schedule 03.11.2011
comment
Этого достаточно, чтобы начать. Спасибо :) - person Billy ONeal; 04.11.2011
comment
Любые указатели на способ распределения ИЛИ по И, когда терминов больше нескольких (например, несколько уровней вложенных И и ИЛИ и много переменных)? - person jamie; 29.12.2011
comment
@Jamie: Вам нужно рекурсивно генерировать умножение для каждой пары. Это ничем не отличается от FOILing :). В худшем случае это занимает экспоненциальное время. (Преобразование в CNF или DNF лежит в основе исходной проблемы NP Complete, выполнимости) - person Billy ONeal; 24.10.2013

arrow_upward
10
arrow_downward

Посмотрите на 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)
person Ayrat    schedule 24.10.2013

arrow_upward
4
arrow_downward

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

person Dejan    schedule 18.10.2016
comment
Сайт удален, это архив: https://web.archive.org/web/20160609111815/http://cs.jhu.edu/~jason/tutorials/convert-to-CNF - person Crouching Kitten; 08.12.2020