Модуль sympy + logi c: assert (is_cnf (to_cnf (expr, simpify = True))) завершается ошибкой - PullRequest
Новая
       83

Модуль sympy + logi c: assert (is_cnf (to_cnf (expr, simpify = True))) завершается ошибкой

0 голосов
/ 18 марта 2020

Я пытаюсь использовать sympy, чтобы помочь мне разобрать некоторые связанные с logi c текстовые файлы (после дополнительной обработки строк: например, генерация пронумерованных x-переменных как x0, x1...) и я не понимаю следующее поведение: 

in_ = '( ( x1 & x2 & x3 & x4 & x5 & x6 & x7 & x8 & x9 )  |  ( x1 & x2 & x3 & x4 & x5 & x6 & x7 & x10 & x9 )  |  ( x1 & x11 & x3 & x12 & x5 & x13 & x14 & x15 & x9 ) ) '

from sympy.parsing.sympy_parser import parse_expr
from sympy.logic.boolalg import to_cnf, is_cnf

parsed = parse_expr(in_, evaluate=False)
cnf_candidate = to_cnf(parsed, simplify=True)  # broken with simp=True; works with simp=False
cnf_status = is_cnf(cnf_candidate)

print(parsed)
print(cnf_candidate)
print(cnf_status)

assert cnf_status 

> (x1 & x10 & x2 & x3 & x4 & x5 & x6 & x7 & x9) | (x1 & x11 & x12 & x13 & x14 & x15 & x3 & x5 & x9) 
(x1 & x2 & x3 & x4 & x5 & x6 & x7 & x8 & x9)

> (x1 & x10 & x2 & x3 & x4 & x5 & x6 & x7 & x9) | (x1 & x11 & x12 & x13 & x14 & x15 & x3 & x5 & x9) | 
(x1 & x2 & x3 & x4 & x5 & x6 & x7 & x8 & x9)

> False
> AssertionError

Это выглядит очень плохо!

  • to_cnf на самом деле не производит cnf и не предупреждает меня об этом (с simplify=True).

Без упрощения:

  • работает и на выходе отображается ожидаемое экспоненциальное увеличение

Это выглядит несколько как «я никогда не смогу минимизировать это, поэтому я не пробую это» вещь, без обратной связи .

Я что-то пропустил? Является ли мое использование правильным (я предполагал, что синтаксический анализ sympys способен работать с моими пронумерованными переменными).

(Давайте пока проигнорируем более теоретическую сторону -> экспоненциальный рост; возможность упрощения)

1 Ответ

1 голос
/ 18 марта 2020

Функция to_cnf с simplify=True вызывает simplify_logic без прохождения установки флага force=True. Поскольку выражение имеет более 8 переменных, преобразование в cnf не предпринимается, и процедура не проверяет, находится ли упрощенный результат в форме cnf. Простой патч - 

diff --git a/sympy/logic/boolalg.py b/sympy/logic/boolalg.py
index dd734ce..d544ea7 100644
--- a/sympy/logic/boolalg.py
+++ b/sympy/logic/boolalg.py
@@ -1714,7 +1714,9 @@ def to_cnf(expr, simplify=False):
         return expr

     if simplify:
-        return simplify_logic(expr, 'cnf', True)
+        new = simplify_logic(expr, 'cnf', True)
+        if is_cnf(new):
+            return new

     # Don't convert unless we have to
     if is_cnf(expr):

Затем (если вы хотите попытаться упростить результат) вам нужно вызвать simplify_logic с force=True.

...