Monotoniczna formuła CNF z m terminami na n zmiennych ( ) jest formułą postaci , gdzie każdy jest OR pewnego podzbioru zmiennych i i wynosi od 1 do m . f ( x 1 , … , x n ) = ⋀ C i C i x 1 , … , x n i 1 m
Na przykład to monotoniczna formuła CNF z 2 terminami na 4 zmiennych.
Szukam najkrótszej formuły (niekoniecznie monotonicznej, niekoniecznie CNF, każda formuła wystarczy!) Na tym samym zestawie zmiennych, która reprezentuje tę samą funkcję, co dana monotoniczna formuła CNF na n zmiennych z n terminami. (Pamiętaj, że liczba terminów i zmiennych jest taka sama).
Jednym oczywistym sposobem skonstruowania formuły jest rozszerzenie danej definicji CNF, która da nam formułę o rozmiarze . (Zdefiniujmy rozmiar formuły, która będzie długością formuły zapisywanej jako ciąg znaków). Chcę wiedzieć, czy jest to najbardziej wydajna ogólna konstrukcja, czy też dla każdej n-terminowej monotonicznej CNF istnieje formuła o wielkości .
Chcę tylko wiedzieć, czy jest to możliwe, tak naprawdę nie interesuje mnie algorytm. Jeśli nie jest to możliwe, funkcja, która służy jako kontrprzykład, byłaby świetna. Doceniane są również wskaźniki, w których można znaleźć odpowiedź w literaturze.
EDYCJA: Dodaję przykład, aby rozjaśnić cienkie.
Powiedzmy, że formuła wejściowa to . Jest to monotoniczna formuła CNF. Krótsza formuła reprezentująca tę samą funkcję jest następująca: .
źródło
Weź pod uwagę, że dla dowolnego CNF można obliczyć zbiór implikacji pierwotnych (z których każde minimum musi być podzbiorem), przyjmując zamknięcie w ramach rozdzielczości i stosując eliminację sumy.
Jednak w przypadku monotonicznego CNF , zamknięcie rozdzielczości F jest F (ponieważ nie ma literałów ujemnych, nie ma możliwości rozdzielczości). Dlatego minimalna wartość CNF to zbiór implikacji liczb pierwszych, czyli dokładnie taka formuła, którą już masz.fa fa fa
Oczywiście zakładam, że nie chcesz wprowadzać nowych zmiennych.
Jeśli chcesz się upewnić, że masz jakąś formułę zawierającą terminów, to jak sugerujesz, jedynym sposobem na uzyskanie tego jest rozszerzenie niektórych klauzul poprzez dodanie brakujących zmiennych. Każdy taki CNF powinien mieć taką samą liczbę literałów (miara wielkości, którą sugeruję, uważam) dla stałej f i n .n fa n
źródło