Czy istnieje czasem skuteczny algorytm do rozwiązania #SAT?

Niech będzie formułą logiczną składającą się ze zwykłych operatorów AND, OR i NOT oraz niektórych zmiennych. Chciałbym policzyć liczbę spełniającą zadania dla . To znaczy, chcę znaleźć liczbę różnych przypisań wartości prawdy do zmiennych dla których przyjmuje wartość prawdziwą. Na przykład formuła ma trzy zadowalające przypisania; ma cztery. To jest problem #SAT . $B$ $B$ $B$ $B$ $a\lor b$ $(a\lor b)\land(c\lor\lnot b)$

Oczywiście wydajne rozwiązanie tego problemu oznaczałoby wydajne rozwiązanie SAT, co jest mało prawdopodobne, aw rzeczywistości ten problem jest # P-kompletny, a zatem może być znacznie trudniejszy niż SAT. Więc nie oczekuję rozwiązania gwarantującego skuteczność.

Ale dobrze wiadomo, że jest stosunkowo niewiele naprawdę trudnych przypadków samej SAT. (Patrz na przykład Cheeseman 1991, „Gdzie są naprawdę trudne problemy” ). Zwykłe przycinane wyszukiwanie, choć w najgorszym przypadku ma charakter wykładniczy, może skutecznie rozwiązać wiele przypadków; metody rozwiązywania problemów, chociaż w najgorszym przypadku mają charakter wykładniczy, są w praktyce jeszcze bardziej skuteczne.

Moje pytanie brzmi:

Czy znane są jakieś algorytmy, które mogą szybko policzyć liczbę spełniających przypisania typowej formuły boolowskiej, nawet jeśli takie algorytmy wymagają czasu wykładniczego w ogólnym przypadku? Czy jest coś zauważalnie lepszego niż wyliczenie każdego możliwego zadania?

complexity-theory reference-request satisfiability

— Mark Dominus
źródło

Próbowałem dodać tag dla # p-kompletności, ale oprogramowanie Stack Exchange nie lubi znaku #.

— Mark Dominus

Byłbym ostrożny z twierdzeniem, że „jest stosunkowo niewiele naprawdę trudnych przypadków samej SAT”. Uważam, że link, który łączysz, mówi o losowym SAT. Ponadto zjawisko przejścia fazowego dotyczy tylko przypadkowych przypadków. Istnieje wiele naprawdę trudnych ręcznych, przemysłowych itp. Przypadków SAT.

k

$k$

— Juho

Dzięki. Czy uważasz, że to sprawia, że moje pytanie jest mniej jasne? Czy rozumiesz o co proszę?

— Mark Dominus

To dla mnie jasne. Ważne jest tylko, aby pamiętać, które przypadki wykazują przejście fazowe :)

— Juho

Odpowiedzi:

Liczenie w ogólnym przypadku

Problem, który Cię interesuje, znany jest jako #SAT lub liczenie modeli. W pewnym sensie jest to klasyczny problem # P-zupełny. Liczenie modeli jest trudne, nawet dla SAT! Nic dziwnego, że dokładne metody mogą obsługiwać tylko instancje z około setkami zmiennych. Istnieją również przybliżone metody, które mogą być w stanie obsłużyć instancje z około 1000 zmiennych. $2$

Dokładne metody liczenia często opierają się na wyczerpującym wyszukiwaniu w stylu DPLL lub kompilacji wiedzy. Metody przybliżone są zwykle klasyfikowane jako metody, które dają szybkie oszacowania bez żadnych gwarancji i metody, które zapewniają dolne lub górne granice z gwarancją poprawności. Istnieją również inne metody, które mogą nie pasować do kategorii, takie jak wykrywanie tylnych drzwi lub metody, które domagają się pewnych właściwości strukturalnych, które mają zachować formuły (lub ich wykres ograniczeń).

Istnieją praktyczne wdrożenia. Niektóre dokładne liczniki modeli to CDP, Relsat, Cachet, sharpSAT i c2d. Rodzaje głównych technik używanych przez dokładne solwery to częściowe zliczanie, analiza składników (wykresu niewystarczającego ograniczenia), buforowanie formuł i składników oraz inteligentne wnioskowanie w każdym węźle. Inna metoda oparta na kompilacji wiedzy przekształca wejściową formułę CNF w inną formę logiczną. Z tej formy można łatwo wydedukować liczbę modeli (czas wielomianowy w wielkości nowo wytworzonej formuły). Na przykład można przekonwertować formułę na binarny diagram decyzyjny (BDD). Następnie można przejść BDD z liścia „1” z powrotem do korzenia. Lub w innym przykładzie, c2d wykorzystuje kompilator, który przekształca formuły CNF w deterministyczną rozkładalną negację normalną formę (d-DNNF).

$\phi$ $\phi$

Gogate i Dechter [3] używają techniki liczenia modeli znanej jako SampleMinisat. Opiera się na próbkowaniu z wolnej od wstecznej przestrzeni wyszukiwania formuły boolowskiej. Technika ta opiera się na zasadzie ważnego ponownego próbkowania, wykorzystując solwery SAT oparte na DPLL do budowy przestrzeni wyszukiwania wolnej od powrotów. Można to zrobić całkowicie lub w przybliżeniu. Możliwe jest również pobieranie próbek do oszacowań z gwarancjami. Opierając się na [2], Gomes i in. [4] wykazał, że stosując próbkowanie ze zmodyfikowaną randomizowaną strategią, można uzyskać możliwe do udowodnienia dolne granice całkowitej liczby modeli z wysokimi gwarancjami poprawności probabilistycznej.

Istnieje również praca oparta na propagowaniu przekonań (BP). Patrz Kroc i in. [5] i BPCount, które wprowadzają. W tym samym artykule autorzy podają drugą metodę o nazwie MiniCount, służącą do ustalenia górnych granic liczby modeli. Istnieją również ramy statystyczne, które pozwalają obliczyć górne granice przy określonych założeniach statystycznych.

Algorytmy dla # 2-SAT i # 3-SAT

$O(1.3247^n)$ $O(1.6894^n)$ $O(1.6423^n)$

Podobnie jak w naturze problemu, jeśli chcesz rozwiązać przypadki w praktyce, wiele zależy od wielkości i struktury twoich wystąpień. Im więcej wiesz, tym bardziej jesteś w stanie wybrać właściwą metodę.

[1] Vilhelm Dahllöf, Peter Jonsson i Magnus Wahlström. Liczenie satysfakcjonujących zadań w 2-SAT i 3-SAT. W materiałach z 8. dorocznej międzynarodowej konferencji Computing and Combinatorics (COCOON-2002), 535-543, 2002.

[2] W. Wei i B. Selman. Nowe podejście do liczenia modeli. W materiałach z SAT05: 8. Międzynarodowa konferencja na temat teorii i zastosowań testów satysfakcji, tom 3569 notatek z wykładów z informatyki, 324-339, 2005.

[3] R. Gogate i R. Dechter. Przybliżone liczenie poprzez próbkowanie przestrzeni wyszukiwania wolnej od cofania. In Proceedings of AAAI-07: 22th National Conference on Artificial Intelligence, 198–203, Vancouver, 2007.

[4] CP Gomes, J. Hoffmann, A. Sabharwal i B. Selman. Od próbkowania do zliczania modeli. In Proceedings of IJCAI-07: 20th International Joint Conference on Artificial Intelligence, 2293–2299, 2007.

[5] L. Kroc, A. Sabharwal i B. Selman. Wykorzystanie propagowania przekonań, wyszukiwania wstecznego i statystyk zliczania modeli. W CPAIOR-08: Piąta międzynarodowa konferencja nt. Integracji technik AI i OR w programowaniu ograniczeń, tom 5015 notatek z wykładów z informatyki, 127–141, 2008.

[6] K. Kutzkov. Nowa górna granica dla problemu nr 3-SAT. Information Processing Letters 105 (1), 1-5, 2007.

— Juho
źródło

Oprócz artykułów wymienionych przez Juho, oto kilka innych, które opisują prace na ten temat, szczególnie w zakresie przybliżania liczby rozwiązań:

Liczenie modeli . Carla P. Gomes, Ashish Sabharwal, Bart Selman Handbook of Satisfiable, IOS Press. Redakcja: Armin Biere, Marijn Heule, Hans van Maaren i Toby Walsh. Rozdział 20, s. 633–654, 2009.
- Jest to ładny przegląd tematu i wprowadzenie do wielu technik.
Prawie jednolite próbkowanie przestrzeni kombinatorycznych przy użyciu ograniczeń XOR . Carla P. Gomes, Ashish Sabharwal, Bart Selman. NIPS-06. 20. doroczna konferencja nt. Systemów przetwarzania informacji neuronowych, str. 481–488, Vancouver, BC, Kanada, grudzień 2006.
Krótkie XOR do zliczania modeli: od teorii do praktyki . Carla P. Gomes, Joerg Hoffmann, Ashish Sabharwal, Bart Selman SAT-07. 10. Międzynarodowa konferencja na temat teorii i zastosowań testów satysfakcji, LNCS tom 4501, str. 100-106, Lizbona, Portugalia, maj 2007.
Wykorzystanie propagowania przekonań, wyszukiwania wstecznego i statystyk zliczania modeli . Lukas Kroc, Ashish Sabharwal, Bart Selman ANOR-2011. Annals of Operations Research, tom 184, nr 1, s. 209–231, 2011.
Heurystyka dla szybkiego dokładnego zliczania modeli . Tian Sang, Paul Beame i Henry Kautz. Teoria i zastosowania testów satysfakcji (SAT 2005), s. 226–240.

— DW
źródło