Блог

Главная - Вопросы по программированию - Преобразование сложного логического выражения в CNF (без экспоненциального раздувания)

Преобразование сложного логического выражения в CNF (без экспоненциального раздувания)

#python #boolean #logical-operators #boolean-expression #sat

Вопрос:

В моей задаче логической логики у меня есть набор переменных (закодированных как целые числа) длиной более 10 000 (от 10 до 100 кб). Каждая переменная имеет свой набор ограничений, т. Е. Другие переменные из того же набора противоречат ей. Противоречия взаимны, т.е.

 (1 amp; -2) | (2 amp; -1)

Задача состоит в том, чтобы максимизировать количество взаимно удовлетворяющих переменных. В терминах SAT это должно быть сформулировано как:

 MAXIMIZE {
(1 amp; -2 amp; -3 ...) |
(2 amp; -1 amp; -4 ...) |
...
}

Это выражение интуитивно находится в формате DNF, но решатели SAT работают с выражениями CNF, поэтому преобразование необходимо.

Я хочу:

  • решите выражение с помощью решателя SAT (я использую инструментарий PySAT), что подразумевает перевод его в форму CNF, в то же время избегая экспоненциального увеличения предложений (необходимо применить преобразования Цейтина / ограничения мощности — но просто не знаю как);
  • максимизировать количество правдивых предложений в выражении, т.Е. Решить задачу «max-SAT» с максимальным количеством удовлетворяющих переменных

Пожалуйста, помогите мне сформулировать действительный CNF (ссылаясь на то, как это можно сделать в решателе Python SAT или просто в необработанном выражении).

Метки: