Najkrótsza równoważna formuła CNF

Niech będzie zadowalającą formułą CNF z zmiennymi i klauzulami . Niech będzie przestrzenią rozwiązań .$F_1$m S F 1 F $n$$m$$S_{F_1}$$F_1$

Rozważ problem z określeniem, biorąc pod uwagę , innej formuły CNF z tym samym zestawem zmiennych co , z (ta sama przestrzeń rozwiązania co ), ale z możliwie jak najmniejszą liczbą klauzul (jedyne celem jest zminimalizowanie liczby klauzul, więc liczba literałów w każdej klauzuli nie ma znaczenia).F 2 F 1 S F 2 = S F 1 F $F_1$$F_2$$F_1$$S_{F_2} = S_{F_1}$$F_1$

Pytanie

Czy ktoś już zbadał ten problem? Czy w literaturze są jakieś wyniki?

Jako przykład rozważmy następującą formułę CNF (każdy wiersz jest klauzulą): $F_1$

x 2 ∨ x 3 ∨ x 4 ¬ x 1 ∨ x 2 ∨ x 4 ¬ x 1 ∨ x 2 ∨ ¬ x 3 ¬ x 1 ∨ x 3 ∨ x 5 ¬ x 1 ∨ x 2 ∨ ¬ x $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$

oraz następujący wzór : $F_2$

$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$

oba mają tę samą przestrzeń rozwiązania, ale podczas gdy $F_1$ ma $6$ klauzul, $F_2$ ma tylko $4$ .

Na koniec rozważ następującą formułę $F_3$ :

$x_2 \lor x_3$
$\lnot x_1 \lor x_3 \lor x_5$
$\lnot x_1 \lor x_2$

Przestrzeń rozwiązania jest znowu taka sama, ale zawiera tylko klauzule.$3$

Problem ustalenia, czy istnieje równoważna formuła CNF z co najwyżej określoną liczbą literałów, to . Wersja minimalizująca liczbę klauzul jest w granicach wielkości formuły, gdzie jest liczbą zmiennych. Sekcja 6:$\Pi_2^p$$n$$n$

• Christopher Umans, The Minimum Equivalent DNF Problem and Shortest Implicants , JCSS 63 (4), 597–611, 2001. doi: 10.1006 / jcss.2001.1775 ( preprint )

Ostatni wynik pokazuje, że obliczenie określonej dolnej granicy dla wielkości najkrótszej równoważnej formuły CNF (mierzonej liczbą klauzul, jak określasz) jest NP-zakończone. Ten artykuł stwierdza również, że twój problem zminimalizowania liczby klauzul jest również -kompletny, cytując powyższy artykuł Umansa, chociaż dlaczego nie wynika to od razu.$\Pi^p_2$

• Ondřej Čepek, Petr Kučera i Petr Savický, Boolean działa z prostym certyfikatem złożoności CNF , DAM 160 (4–5), 365–382, 2012. doi: 10.1016 / j.dam.2011.05.013

Problemem minization obwód jest trudny (patrz komentarz poniżej). Wydaje mi się również, że być może zainteresuje Cię technika, którą stosują niektóre solwery SAT (przynajmniej w pewnym stopniu), która nazywa się wstępnym przetwarzaniem SAT. Na przykład dobrze znany solver MiniSAT wykorzystuje minimalizator CNF SatELite do wstępnego przetworzenia instancji. Google Scholar daje również wiele wyników dla „sat preprocessing”.

głównym standardowym / znanym rozwiązaniem minimalizacji CNF w EE jest algorytm Quine-McCluskey, którego jest wiele implementacji, niektóre są własnością publiczną. jednakże rozumiem, że (nie wspomniane w bieżącym artykule na Wikipedii) większość powraca do heurystyki i chciwych algorytmów, aby znaleźć rozwiązania szczególnie dla dużych formuł, tzn. nie jest to konieczne. znajdź optymalne rozwiązanie esp. dla dużych instancji wejściowych.

Quine-MCluskey to uogólnienie pracy z mapami Karnough, które diagramy mogą odnieść sukces w małych instancjach.

i zauważ, że może istnieć wiele optymalnych rozwiązań pod względem równoważnych formuł o tej samej (minimalnej) wielkości klauzuli, zostanie to wskazane w dobrym odnośniku na temat subj. znajdowanie minimum najwyraźniej sprowadza się do wyszczególnienia wszystkich pierwotnych implikacji, które mogą wiązać się z ogromnym wykładniczym powiększeniem pamięci / „przestrzeni” w porównaniu do rozmiaru oryginalnej formuły.