Minimalna niezadowalająca formuła 3-CNF

Obecnie jestem zainteresowany pozyskiwaniem (lub konstruowaniem) i badaniem formuł 3-CNF, które są niezadowalające i mają minimalny rozmiar. Oznacza to, że muszą składać się z jak najmniejszej liczby klauzul (najlepiej m = 8) i możliwie jak najmniejszej liczby odrębnych zmiennych (n = 4 lub więcej), tak że usunięcie co najmniej jednej klauzuli sprawi, że formuła będzie zadowalająca.

Bardziej formalnie, każda kwalifikująca się formuła 3-CNF musi spełniać następujące warunki:

F jest niezadowalający
F ma minimalną ilość (4+) różnych zmiennych (lub ich negację)
F ma minimalną liczbę klauzul (8+)
każdy właściwy podzbiór F jest satysfakcjonujący (umożliwiając usunięcie dowolnej arbitralnej klauzuli lub klauzul).
F nie ma 2 klauzul, które można zredukować do klauzuli 2-CNF, np. (i, j, k) & (i, j, ~k)NIE jest dozwolone (redukują do (i,j))

Na przykład przy n = 4 istnieje wiele minimalnych 8-klauzulowych wzorów 3-CNF, które są niezadowalające. Po pierwsze, patrząc na 4-hipersześcian i próbując pokryć go krawędziami (2-ścianami), można skonstruować następującą niezadowalającą formułę:

1. (~A,  B,  D)
2. (~B,  C,  D)
3. ( A, ~C   D)
4. ( A, ~B, ~D)
5. ( B, ~C, ~D)
6. (~A,  C, ~D)
7. ( A,  B,  C)
8. (~A, ~B, ~C)

Kwalifikuje się to jako minimalnie niezadowalająca formuła 3-CNF, ponieważ:

Jest niezadowalający:
- Punkty 1-3 są równoważne z: D or A=B=C
- Punkty 4-6 są równoważne z: ~D or A=B=C
- Sugerują A=B=C, ale w klauzulach 7 i 8 jest to sprzeczność.
Istnieją tylko 4 różne zmienne.
Jest tylko 8 klauzul.
Usunięcie dowolnej klauzuli czyni ją satysfakcjonującą.
Żadne 2 klauzule nie są „redukowalne” do klauzuli 2-CNF.

Sądzę więc, że moje ogólne pytania są w kolejności według mnie:

Jakie są inne małe minimalne formuły, które spełniają powyższe warunki? (tj. powiedzmy 4,5,6 zmiennych i 8,9,10 klauzul)
Czy istnieje jakaś baza danych lub „atlas” takich minimalnych formuł?
Jakie nielosowe algorytmy istnieją, by je skonstruować wprost, jeśli w ogóle?
Jakie są wgląd w cechy tych formuł? Czy można je policzyć lub oszacować, biorąc pod uwagę n (# zmiennych) im (# klauzul)?

Z góry dziękuję za odpowiedzi. Czekam na każdą odpowiedź lub komentarz.

cc.complexity-theory sat

— MAF
źródło

Każda klauzula 3-CNF nie zezwala na 1/8 możliwych rozwiązań. Tak wyraźnie, że zawsze potrzebujesz co najmniej 8 klauzul lub więcej, jeśli zestawy niedozwolonych rozwiązań nakładają się. Od stanu 5 zabrania zakaz nakładających zestawy niedozwolonych rozwiązań dla n = 3, trzeba więcej niż 8 klauzule w tym przypadku: Należy pamiętać, że przykład nie warunek posłuszni 5.

— András Salamon

Tak, masz rację we wszystkich punktach András. 8 klauzul jest wymaganym minimum dla niezadowalającej formuły 3-CNF, dlatego warunek 5 może być zbyt restrykcyjny dla moich celów w poszukiwaniu / konstruowaniu formuł kwalifikujących. Zdaję sobie sprawę, że dla n = 3 warunek 5 musi być koniecznie naruszony, ale został uwzględniony wyłącznie w celach ilustracyjnych. Jestem ściśle zainteresowany formułami kwalifikacyjnymi o rozmiarze n = 4 + (tj. 4 lub więcej zmiennych, ale nie za dużo więcej). Być może zarysuję warunek 5.

— MAF

Myślę, że twój „przykład” z n = 3 jest raczej mylący niż ilustracyjny, ponieważ (jak zauważył András w swoim komentarzu) tak naprawdę nie jest to przykład tego, o co pytasz w tym pytaniu. Przykład z n = 4 jest doskonale w porządku i ilustrujący. Dlaczego po prostu nie usuniesz przykładu z n = 3?

— Tsuyoshi Ito,

Dobra uwaga, Tsuyoshi. Gotowy.

— MAF

{x}

$\{x\}$

{x^{'}}

$\{x'\}$

C

$C$

C \cup {v}

$C \cup \{v\}$

C \cup {v^{'}}

$C \cup \{v'\}$

v

$v$

Odpowiedzi:

$\lnot A \lor \lnot B \lor \lnot C$ $2$

$\lnot A \lor \lnot B \lor \lnot E$
$\lnot B \lor \lnot C \lor E$

$n=5$ $m=9$

$l_1 \lor l_2 \lor l_3$ $2$

$l_1 \lor l_2 \lor v$
$l_2 \lor l_3 \lor \lnot v$

$v$ $n$ $m$ $1$ $r=\frac{m}{n}$ $1$ $n$ $r=1$

— Giorgio Camerani
źródło

Dzięki za odpowiedź, Walter. Opisana procedura jest rzeczywiście bardzo pomocna w generowaniu jeszcze nieco większych, mniejszych formuł „Unatat” o „podobnej” strukturze, to znaczy, gdy już znajdziesz zestaw rdzenia, który znajdziesz, ma interesujące właściwości.

— MAF

@MAF: Nie ma za co. Dziękujemy za zamieszczenie tak interesującego pytania.

— Giorgio Camerani

Uważam, że warunek nr 5 tak naprawdę nie jest spełniony w twoim przykładzie i nie może być spełniony nigdy.
Niech następujące klauzule będą równoważne:

( p, q) = (~A,B,D)(A,~B,~D)

Co pozwoli nam zmapować zdania A, B, C i D na nowe zmienne p, q, r i s, jak w poniższej tabeli prawdy:

A B C D | p q r s
-----------------
0 0 0 0 | 0 1 0 0
0 0 0 1 | 0 1 0 1
0 0 1 0 | 0 1 1 0
0 0 1 1 | 0 1 1 1
-----------------
0 1 0 0 | 1 0 0 0
0 1 0 1 | 0 0 0 0
0 1 1 0 | 1 0 0 1
0 1 1 1 | 0 0 0 1
-----------------
1 0 0 0 | 0 0 1 0
1 0 0 1 | 1 0 1 0
1 0 1 0 | 0 0 1 1
1 0 1 1 | 1 0 1 1
-----------------
1 1 0 0 | 1 1 0 0
1 1 0 1 | 1 1 0 1
1 1 1 0 | 1 1 1 0
1 1 1 1 | 1 1 1 1
-----------------

A teraz możemy wyrazić zdania A, B, C i D w kategoriach p, q, r i s:

1. (~A,  B,  D) = ( p, q,~r, s)( p, q,~r,~s)
2. (~B,  C,  D) = (~p, q, r, s)(~p,~q, r, s)
3. ( A, ~C   D) = ( p,~q,~r, s)(~p, q, r,~s)
4. ( A, ~B, ~D) = ( p, q, r, s)( p, q, r,~s)
5. ( B, ~C, ~D) = ( p,~q,~r,~s)(~p, q,~r,~s)
6. (~A,  C, ~D) = (~p, q,~r, s)(~p,~q, r,~s)
7. ( A,  B,  C) = ( p,~q, r, s)( p,~q, r,~s)
8. (~A, ~B, ~C) = (~p,~q,~r, s)(~p,~q,~r,~s)

Ponieważ wszystkie klauzule są pokazane i powiązane z klauzulami A, B, C i D. Następnie możemy twierdzić, że klauzule p, q, r i s można sprowadzić do:

( p, q, r)
( p, q,~r)
( p,~q, r)
( p,~q,~r)
(~p, q, r)
(~p, q,~r)
(~p,~q, r)
(~p,~q,~r)

Co oczywiście narusza warunek nr 5.

Chciałbym zwrócić uwagę, że nawet ten przykład nie pokazuje wyraźnie, że istnieją 2 klauzule, które można zredukować do 2-CNF, ale domyślnie tak jest (np. (~ A, B, D) i (A, ~ B, ~ D)), możesz nie być w stanie wyrazić 2-CNF za pomocą podanych zmiennych, ale kiedy wprowadzisz inne odwzorowanie dla problemu, będziesz w stanie je wyrazić.

— Khazam Alhamdan
źródło