Zaspokojenie rogów

W logice formalnej spełnialność Horna lub HORNSAT to problem z podjęciem decyzji, czy dany zestaw zdaniowych klauzul Horna jest spełnialny, czy nie. Klauzule Horn-spełnialności i Horn są nazwane na cześć Alfreda Horna .

Podstawowe definicje i terminologia

Klauzula Horna to klauzula z co najwyżej jednym literałem dodatnim , zwanym głową klauzuli, oraz dowolną liczbą literałów ujemnych, tworzących treść klauzuli . Formuła Horna to formuła zdaniowa utworzona przez koniunkcję klauzul Horna.

Problem spełnialności Horna jest rozwiązywalny w czasie liniowym . Problem decydowania o prawdziwości skwantyfikowanych formuł Horna można również rozwiązać w czasie wielomianowym. Algorytm czasu wielomianowego dla spełnialności Horna jest oparty na zasadzie propagacji jednostek : jeśli formuła zawiera klauzulę złożoną z pojedynczego literału $l$ klauzula jednostkowa), to wszystkie klauzule zawierające $\ displaystyle l}$ (z wyjątkiem samej klauzuli jednostkowej) są usuwane, a wszystkie klauzule zawierające ${\ displaystyle \ neg l}$ usuń ten literał. Wynikiem drugiej reguły może być sama klauzula jednostkowa, która jest propagowana w ten sam sposób. Jeśli nie ma klauzul jednostkowych, formułę można spełnić, po prostu ustawiając wszystkie pozostałe zmienne jako ujemne. $,$ jeśli ta transformacja generuje parę przeciwstawnych $jednostkowych$ i . Spełnialność Horna jest w rzeczywistości jednym z „najtrudniejszych” lub „najbardziej wyrazistych” problemów, o których wiadomo, że można je obliczyć w czasie wielomianowym, w tym sensie, że jest to P - zupełne problem.

Algorytm ten umożliwia również określenie prawdziwości spełnialnych formuł Horna: wszystkie zmienne zawarte w klauzuli jednostkowej są ustawiane na wartość spełniającą tę klauzulę jednostkową; wszystkie inne literały mają wartość false. Otrzymane przypisanie jest minimalnym modelem formuły Horna, to znaczy przypisaniem posiadającym minimalny zbiór zmiennych przypisanych do wartości true, gdzie porównania dokonuje się za pomocą zawierania zestawów.

Wykorzystując algorytm liniowy do propagacji jednostek, algorytm jest liniowy pod względem wielkości formuły.

Uogólnieniem klasy formuł Horna są formuły Horna, które można zmienić, czyli zestaw formuł, które można umieścić w postaci Horna, zastępując niektóre zmienne ich odpowiednimi negacjami. Sprawdzenie istnienia takiej zamiany można przeprowadzić w czasie liniowym; dlatego spełnialność takich formuł jest w P, ponieważ można ją rozwiązać, najpierw wykonując to zastąpienie, a następnie sprawdzając spełnialność wynikowej formuły Horna. Spełnialność Horna i możliwość zmiany nazwy Spełnialność Horna zapewnia jedną z dwóch ważnych podklas spełnialności, które można rozwiązać w czasie wielomianowym; drugą taką podklasą jest 2-spełnialność .

Problem spełnialności Horna można również zadać dla zdaniowych logik wielowartościowych . Algorytmy zwykle nie są liniowe, ale niektóre są wielomianowe; patrz Hähnle (2001 lub 2003), aby zapoznać się z ankietą.

Podwójny głośnik SAT

Podwójnym wariantem Horn SAT jest Dual-Horn SAT , w którym każda klauzula ma co najwyżej jeden ujemny literał. Zanegowanie wszystkich zmiennych przekształca instancję Dual-Horn SAT w Horn SAT. W 1951 roku Horn udowodnił, że Dual-Horn SAT jest w P . ^{[ potrzebne źródło ]}

Zobacz też

^ Dowling, William F.; Gallier, Jean H. (1984), „Algorytmy czasu liniowego do testowania spełnialności zdaniowych formuł Horna”, Journal of Logic Programming , 1 (3): 267–284, doi : 10.1016 / 0743-1066 (84) 90014- 1 , MR 0770156
Bibliografia _ Karpiński, Marek; Flogel, A. (1995). „Rozdzielczość dla ilościowych formuł logicznych” . Informacja i obliczenia . Elsevier. 117 (1): 12–18. doi : 10.1006/inco.1995.1025 .
Bibliografia _ Phuong Nguyen (2010). Logiczne podstawy złożoności dowodu . Wydawnictwo Uniwersytetu Cambridge. P. 224. ISBN 978-0-521-51729-4 .
^ Lewis, Harry R. (1978). „Zmiana nazwy zestawu klauzul na zestaw Horna”. Dziennik ACM . 25 (1): 134–135. doi : 10.1145/322047.322059 . MR 0468315 . .
^ Aspvall, Bengt (1980). „Rozpoznawanie ukrytych przypadków NR (1) problemu spełnialności”. Dziennik algorytmów . 1 (1): 97–103. doi : 10.1016/0196-6774(80)90007-3 . MR 0578079 .
^ Hebrard, Jean-Jacques (1994). „Algorytm liniowy do zmiany nazwy zestawu klauzul na zestaw Horna” . Informatyka teoretyczna . 124 (2): 343–350. doi : 10.1016/0304-3975(94)90015-9 . MR 1260003 . .
^ Chandru, Widźaja; Collette R. Coullard ; Petera L. Hammera; Miguel Montañez; Xiaorong Sun (2005). „O zmienianych nazwach Horn i uogólnionych funkcjach Horn”. Roczniki matematyki i sztucznej inteligencji . 1 (1–4): 33–47. doi : 10.1007/BF01531069 .
Bibliografia _ „Zaawansowane logiki wielowartościowe”. W Dov M. Gabbay, Franz Günthner (red.). Podręcznik logiki filozoficznej . Tom. 2 (wyd. 2). Skoczek. P. 373. ISBN 978-0-7923-7126-7 .
Bibliografia _ „Złożoność logiki wielowartościowej”. W Melvin Fitting, Ewa Orłowska (red.). Poza dwoma: teoria i zastosowania logiki wielowartościowej . Skoczek. ISBN 978-3-7908-1541-2 .

Dalsza lektura

Gradel, Erich; Kolaitis, Phokion G.; Libkin, Leonid; Maarten, Marks; Spencer, Joel ; Vardi, Mosze Y .; Venema, Yde; Weinstein, Scott (2007). Teoria modeli skończonych i jej zastosowania . Teksty z informatyki teoretycznej . Seria EATCS. Berlin: Springer-Verlag . ISBN 978-3-540-00428-8 . Zbl 1133.03001 .

[1] Dowling, William F.; Gallier, Jean H. (1984), „Algorytmy czasu liniowego do testowania spełnialności zdaniowych formuł Horna”, Journal of Logic Programming , 1 (3): 267–284, doi : 10.1016 / 0743-1066 (84) 90014- 1 , MR 0770156

[buningkarpinski-2] Bibliografia _ Karpiński, Marek; Flogel, A. (1995). „Rozdzielczość dla ilościowych formuł logicznych” . Informacja i obliczenia . Elsevier. 117 (1): 12–18. doi : 10.1006/inco.1995.1025 .

[CookNguyen2010-3] Bibliografia _ Phuong Nguyen (2010). Logiczne podstawy złożoności dowodu . Wydawnictwo Uniwersytetu Cambridge. P. 224. ISBN 978-0-521-51729-4 .

[4] Lewis, Harry R. (1978). „Zmiana nazwy zestawu klauzul na zestaw Horna”. Dziennik ACM . 25 (1): 134–135. doi : 10.1145/322047.322059 . MR 0468315 . .

[5] Aspvall, Bengt (1980). „Rozpoznawanie ukrytych przypadków NR (1) problemu spełnialności”. Dziennik algorytmów . 1 (1): 97–103. doi : 10.1016/0196-6774(80)90007-3 . MR 0578079 .

[6] Hebrard, Jean-Jacques (1994). „Algorytm liniowy do zmiany nazwy zestawu klauzul na zestaw Horna” . Informatyka teoretyczna . 124 (2): 343–350. doi : 10.1016/0304-3975(94)90015-9 . MR 1260003 . .

[7] Chandru, Widźaja; Collette R. Coullard ; Petera L. Hammera; Miguel Montañez; Xiaorong Sun (2005). „O zmienianych nazwach Horn i uogólnionych funkcjach Horn”. Roczniki matematyki i sztucznej inteligencji . 1 (1–4): 33–47. doi : 10.1007/BF01531069 .

[8] Bibliografia _ „Zaawansowane logiki wielowartościowe”. W Dov M. Gabbay, Franz Günthner (red.). Podręcznik logiki filozoficznej . Tom. 2 (wyd. 2). Skoczek. P. 373. ISBN 978-0-7923-7126-7 .

[FittingOrlowska2003-9] Bibliografia _ „Złożoność logiki wielowartościowej”. W Melvin Fitting, Ewa Orłowska (red.). Poza dwoma: teoria i zastosowania logiki wielowartościowej . Skoczek. ISBN 978-3-7908-1541-2 .