Pomiar trudności wystąpień SAT

Biorąc pod uwagę instancję SAT, chciałbym móc oszacować, jak trudno będzie rozwiązać instancję.

Jednym ze sposobów jest uruchamianie istniejących solverów, ale ten rodzaj pokonuje cel oszacowania trudności. Drugi sposób może polegać na szukaniu stosunku klauzul do zmiennych, jak ma to miejsce w przypadku przejść fazowych w losowo-SAT, ale jestem pewien, że istnieją lepsze metody.

Biorąc pod uwagę przykład SAT, czy są jakieś szybkie heurystyki do zmierzenia trudności? Jedynym warunkiem jest to, aby te heurystyki były szybsze niż faktyczne uruchamianie istniejących solverów SAT w instancji.

Powiązane pytanie

Które problemy z SAT są łatwe? na cstheory.SE. To pytanie dotyczy możliwych do wykonania zestawów instancji. To podobne pytanie, ale nie do końca takie samo. Naprawdę interesuje mnie heurystyka, która biorąc pod uwagę jedną instancję, w jakiś sposób na wpół inteligentna zgaduje, czy instancja będzie trudna do rozwiązania.

Ogólnie jest to bardzo istotne i interesujące pytanie badawcze. „Jednym ze sposobów jest uruchamianie istniejących solverów ...” i co by to nam dokładnie powiedziało? Widzieliśmy empirycznie, że wystąpienie wydaje się trudne dla konkretnego rozwiązania lub konkretnego algorytmu / heurystyki, ale co tak naprawdę mówi o twardości wystąpienia?

Jednym ze sposobów jest identyfikacja różnych właściwości strukturalnych instancji, które prowadzą do wydajnych algorytmów. Te właściwości są rzeczywiście preferowane, aby można je było „łatwo” zidentyfikować. Przykładem jest topologia bazowego wykresu ograniczenia, mierzona przy użyciu różnych parametrów szerokości wykresu. Na przykład wiadomo, że instancja jest rozwiązywalna w czasie wielomianowym, jeśli szerokość podstawowego wykresu ograniczenia jest ograniczona stałą.

Inne podejście koncentruje się na roli ukrytej struktury instancji. Jednym z przykładów jest zestaw backdoor , co oznacza zestaw zmiennych, tak że gdy są one tworzone, pozostały problem upraszcza się do klasy możliwej do wyleczenia. Na przykład Williams i in., 2003 [1] pokazują, że nawet biorąc pod uwagę koszt poszukiwania zmiennych typu backdoor, nadal można uzyskać ogólną przewagę obliczeniową, skupiając się na zestawie backdoor, pod warunkiem, że zestaw jest wystarczająco mały. Ponadto Dilkina i in., 2007 [2] zauważają, że solver o nazwie Satz-Rand jest wyjątkowo dobry w znajdowaniu małych silnych tylnych drzwi w szeregu domen eksperymentalnych.

Niedawno Ansotegui i in., 2008 [3] proponują użycie drzewiastej złożoności przestrzeni jako miary dla solverów opartych na DPLL. Dowodzą one, że również przestrzeń o stałym ograniczeniu implikuje istnienie algorytmu wielomianowej decyzji w czasie, gdzie przestrzeń jest stopniem wielomianu (Twierdzenie 6 w pracy). Co więcej, pokazują, że przestrzeń jest mniejsza niż rozmiar zestawów cyklicznych. W rzeczywistości, przy pewnych założeniach, przestrzeń jest również mniejsza niż wielkość tylnych drzwi.

Formalizują także to, o czym myślę, że szukasz:

Znajdź miarę , a algorytm, który dał formułę decyduje o spełnieniu w czasie . Im mniejsza miara, tym lepiej charakteryzuje ona twardość formuły .$\psi$$\Gamma$$O(n^{\psi ( \Gamma )})$

[1] Williams, Ryan, Carla P. Gomes i Bart Selman. „Backdoors do typowej złożoności sprawy”. Międzynarodowa wspólna konferencja na temat sztucznej inteligencji. Vol. 18, 2003.

[2] Dilkina, Bistra, Carla Gomes i Ashish Sabharwal. „Kompromisy w złożoności wykrywania backdoorów”. Zasady i praktyka programowania ograniczeń (CP 2007), s. 256–270, 2007.

[3] Ansótegui, Carlos, Maria Luisa Bonet, Jordi Levy i Felip Manya. „Pomiar twardości instancji SAT”. W materiałach z 23. krajowej konferencji na temat sztucznej inteligencji (AAAI'08), s. 222–228, 2008.

Ponieważ wiesz o przejściu fazowym, pozwól mi wspomnieć o kilku innych prostych kontrolach, o których wiem (które prawdopodobnie są uwzględnione w analizie grafu ograniczeń):

• Niektóre wczesne losowe generatory SAT nieumyślnie stworzyły głównie proste formuły, ponieważ stosowały „stałą gęstość”, co oznacza mniej więcej taką samą proporcję wszystkich długości klauzul. Były to w większości łatwe, ponieważ 2-klauzule i jednostki znacznie upraszczają problem, jak można się spodziewać, a naprawdę długie klauzule albo nie dodają zbyt wiele rozgałęzień, albo jeszcze bardziej ułatwiają hiperrozdzielczość. Wydaje się więc, że lepiej trzymać się klauzul o stałej długości i zmieniać inne parametry.
• Podobnie, potężną zasadą uproszczenia jest Czysta Dosłowna Eliminacja. Oczywiście, formuła jest tak trudna, jak liczba nieczystych literałów. Ponieważ Resolution tworzy nowe klauzule numerujące(co oznacza iloczyn występowania i jego negacji), liczba rezolwentów jest zmaksymalizowana, gdy dla każdej zmiennej jest taka sama liczba literałów dodatnich i ujemnych. Stąd zrównoważone generatory SAT.$|x|*|\lnot x|$$x$
• Istnieje również technika o nazwie „No Triangle SAT”, która wydaje się dość świeża [1], która jest rodzajem generatora o twardej instancji, który zabrania „trójkątów”. Trójkąt jest zbiorem klauzul zawierających 3 zmienne które występują parami we wszystkich kombinacjach w pewnym zestawie klauzul (tj. ). Najwyraźniej trójkąty ułatwiają formułę znanym rozwiązującym.$v_1, v_2, v_3$$\{v_1, v_2, ...\}, \{v_2, v_3, ...\}, \{v_1, v_3, ...\}$

[1] https://arxiv.org/pdf/1903.03592.pdf

Oprócz doskonałej odpowiedzi Juho, oto inne podejście:

Ercsey-Ravasz & Toroczkai, Twardość optymalizacji jako przejściowy chaos w analogicznym podejściu do satysfakcji z ograniczeń , Nature Physics tom 7, strony 966–970 (2011).

Podejście to polega na przepisaniu problemu SAT na układ dynamiczny, w którym dowolny atraktor systemu jest rozwiązaniem problemu SAT. Baseny przyciągania systemu są bardziej fraktalne, gdy problem staje się trudniejszy, a zatem „trudność” instancji SAT można zmierzyć, badając stopień chaosu stanów nieustalonych, zanim system zbiegnie się.

W praktyce oznacza to uruchomienie grupy solverów z różnych pozycji początkowych i zbadanie szybkości, z jaką solwery uciekają od chaotycznych stanów nieustalonych, zanim dotrą do atraktora.

Nie jest trudno wymyślić dynamiczny system, w którym „rozwiązania” są rozwiązaniami dla danego problemu SAT, ale nieco trudniej jest upewnić się, że wszystkie rozwiązania są atraktorami, a nie repelentami. Ich rozwiązaniem jest wprowadzenie zmiennych energetycznych (podobnych do mnożników Lagrange'a), aby pokazać, jak poważnie naruszane jest ograniczenie, i spróbuj zmusić system do zminimalizowania energii układu.

Co ciekawe, za pomocą ich układu dynamicznego można rozwiązać problemy SAT w czasie wielomianowym na komputerze analogowym, co samo w sobie jest niezwykłym wynikiem. Jest w tym jakiś haczyk; reprezentowanie zmiennych energii może wymagać wykładniczo dużych napięć, więc niestety nie można tego zrealizować na sprzęcie fizycznym.