Кратчайший эквивалент формулы CNF

Пусть $F_1$ - выполнимая формула CNF с $n$ переменными и $m$ предложениями. Пусть $S_{F_1}$ - пространство решений $F_1$ .

Рассмотрим проблему определения для данной $F_1$ другой формулы CNF $F_2$с тем же набором переменных, что и для $F_1$ , с $S_{F_2} = S_{F_1}$ (то же пространство решений, что и для $F_1$ ), но с как можно меньшим количеством предложений ( единственная цель состоит в том, чтобы минимизировать количество предложений, поэтому количество литералов в каждом предложении не имеет значения).

Вопрос

Кто-нибудь уже исследовал эту проблему? Есть ли какие-либо результаты в литературе по этому поводу?

В качестве примера рассмотрим следующую формулу CNF (каждая строка является предложением): $F_1$

х 2 ∨ х 3 ∨ х 4 ¬ х 1 ∨ х 2 ∨ х 4 ¬ х 1 ∨ х 2 ∨ ¬ х 3 ¬ х 1 ∨ х 3 ∨ х 5 ¬ х 1 ∨ х 2 ∨ $x_1 \lor x_2 \lor x_3$
$x_2 \lor x_3 \lor x_4$
$\lnot x_1 \lor x_2 \lor x_4$
$\lnot x_1 \lor x_2 \lor \lnot x_3$
$\lnot x_1 \lor x_3 \lor x_5$
$\lnot x_1 \lor x_2 \lor \lnot x_5$

и следующая формула : $F_2$

х 2 ∨ х 3 ∨ х 4 ¬ х 1 ∨ х 3 ∨ х 5 ¬ х 1 ∨ х $x_1 \lor x_2 \lor x_3$
$x_2 \lor x_3 \lor x_4$
$\lnot x_1 \lor x_3 \lor x_5$
$\lnot x_1 \lor x_2$

оба имеют одинаковое пространство решений, но в то время как имеет 6 предложений, F 2 имеет только 4 . $F_1$$6$$F_2$$4$

Наконец, рассмотрим следующую формулу : $F_3$

¬ х 1 ∨ х 3 ∨ х 5 ¬ х 1$x_2 \lor x_3$
$\lnot x_1 \lor x_3 \lor x_5$
$\lnot x_1 \lor x_2$

Пространство решений опять то же самое, но только с предложениями.$3$

Задача определения того , существует ли эквивалентная формула КНФА с не более заданным числом литералов -полный. Версия, минимизирующая количество предложений, находится в пределах коэффициента n от размера формулы, где $\Pi_2^p$$n$$n$ - количество переменных. Смотрите раздел 6 из:

• Кристофер Уманс, Минимально эквивалентная проблема DNF и кратчайшие импликанты , JCSS 63 (4), 597–611, 2001. doi: 10.1006 / jcss.2001.1775 ( препринт )

Недавний результат показывает, что вычисление конкретной нижней границы для размера самой короткой эквивалентной формулы CNF (измеряемой количеством предложений, как вы указываете) является NP-полным. В этой статье также говорится, что ваша задача минимизации количества предложений $\Pi^p_2$ -полной, ссылаясь на статью Уманса, приведенную выше, хотя почему это не сразу понятно для меня.

• Ондржей Чепек, Петр Кучера и Петр Савицкий, Булевы функции с простым сертификатом сложности CNF , DAM 160 (4–5), 365–382, 2012. doi: 10.1016 / j.dam.2011.05.013

Проблема минимизации схемы неразрешима (см. Комментарии ниже). Кроме того, я думаю, что вас может заинтересовать метод, используемый некоторыми решателями SAT (по крайней мере, в некоторой степени), который называется предварительной обработкой SAT. Например, хорошо известный решатель MiniSAT использует минимизатор CNF SatELite для предварительной обработки экземпляра. Google Scholar также дает много результатов для "предварительной обработки".

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

Quine-MCluskey - это обобщение работы с картами Карно, диаграммы которых могут быть успешными для небольших случаев.

и обратите внимание, что может быть несколько оптимальных решений в терминах эквивалентных формул с одинаковым (минимальным) размером предложения, это будет указано в хорошей ссылке на subj. нахождение минимума, по-видимому, сводится к перечислению всех простых импликатов, что может привести к значительному экспоненциальному взрыву в памяти / «пространстве» по сравнению с размером исходной формулы.