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

— Giorgio Camerani
źródło

@ tsuyoshi Myślę, że chce uzyskać formułę cnf, która składa się z minimalnej liczby klauzul z tym samym miejscem rozwiązania

— Tayfun Pay

@TsuyoshiIto: Tak, chcę zminimalizować liczbę klauzul. Nie nakładam żadnych ograniczeń na liczbę literałów, które każda klauzula może zawierać.

— Giorgio Camerani

W przypadku każdej rozsądnej definicji „małego” problem jest NP-trudny. Receptura A CNF jest spe tylko wtedy, gdy jest to nie równoważny wzorowi „false”, który ma zerowe klauzul.

— Jeffε

Rozdział 6 citeseerx.ist.psu.edu/viewdoc/… wspomina, że problem z ustaleniem, czy istnieje równoważna formuła CNF z co najwyżej określoną liczbą literałów, jest . Nie jestem pewien, czy rozumiem, dlaczego twoja wersja minimalizująca liczbę klauzul jest interesująca, ponieważ mieści się w współczynniku wielkości formuły, gdzie jest liczbą zmiennych.

Π_{2}^{p}

$\Pi_2^p$

n

$n$

n

$n$

— András Salamon

Istotny

— András Salamon

Odpowiedzi:

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

— András Salamon
źródło

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”.

— Juho
źródło

Myślałem, że Buchfuhrer i Umans w 2008 roku rozwiązali problem minimalizacji obwodu jako

-kompletny, w ramach redukcji Turinga?

Π_{2}^{p}

$\Pi^p_2$

— András Salamon,

Umans wykazał już w 1998 r., Że znalezienie minimalnej równoważnej formuły CNF to

twardy ( dx.doi.org/10.1006/jcss.2001.1775 ). Artykuł, o którym wspomina András, uogólnia to na obwody o większej głębokości.

Σ_{2}^{P}

$\Sigma^P_2$

— Jan Johannsen

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.

— vzn
źródło