Pomiar trudności wystąpień SAT

28

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.

Artem Kaznatcheev
źródło
Czy potrafisz wyjaśnić, dlaczego przemiana fazowa wr „gęstości” nie jest tym, czego potrzebujesz?
Raphael
@Raphael to całkiem niezła metoda i wspominam o tym w moim pytaniu. Mam jednak wrażenie, że istnieje jeszcze lepsza heurystyka. Przejście fazowe przeszkadza mi, ponieważ wydaje się to tak łatwe do oszukania (wystarczy dołączyć łatwo spełniające się klauzule lub instancję do tej, którą próbujesz ukryć)
Artem Kaznatcheev
Przepraszam, przegapiłem tę część twojego pytania. Racja, jak zauważają komentatorzy, przejście fazowe wydaje się być wrażliwe na formuły nieprzypadkowe.
Raphael
2
Możesz reprezentować formułę SAT (w CNF) jako wykres dwudzielny, z wierzchołkami dla każdej formuły i klauzuli oraz krawędziami reprezentującymi wystąpienia. Jeśli ten wykres można łatwo podzielić, problem można rozłożyć na podzielone na partycje podgrupy. Może to może być użytecznym środkiem? Nie mam pojęcia (dlatego jest to komentarz, a nie odpowiedź).
Alex ten Brink
Może się to przydać: ece.uwaterloo.ca/~vganesh/QPaper/paper.pdf
użytkownik

Odpowiedzi:

22

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 .ψΓO(nψ(Γ))


[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.

Juho
źródło
Podoba mi się formalizacja, którą cytujesz. Przydałoby się również doprecyzować, aby wyraźnie stwierdzić, że jest wydajnie obliczalny. Dziękuję za odpowiedź! Czy znasz mniej formalne środki, które ludzie mogą zastosować „w praktyce”? ψ(Γ)
Artem Kaznatcheev
@ArtemKaznatcheev Myślę, że zestaw backdoor jest prawdopodobnie jedynym naprawdę używanym. Podczas uruchamiania solwera tak naprawdę nie dbamy o twardość formuły; instancja musi jednak zostać rozwiązana. Pomiar musi dać nam przewagę obliczeniową, a może możemy go użyć do wybrania odpowiedniej heurystyki. Poza tym wydaje mi się, że pomiary twardości są wciąż dość eksperymentalne.
Juho,
1

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||¬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.v1,v2,v3{v1,v2,...},{v2,v3,...},{v1,v3,...}

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

Kosiarz umyslów
źródło
0

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.

Pseudonim
źródło
1
„za pomocą ich systemu dynamicznego można rozwiązać problemy SAT w czasie wielomianowym na komputerze analogowym, co samo w sobie jest niezwykłym wynikiem”. Nie zgadzam się, że jest to niezwykłe. Jak zauważasz: wymaga wykładniczej precyzji. Jest to w rzeczywistości standardowa sztuczka, która prowadzi bezpośrednio do definicji NP. Jeśli możesz zmierzyć wykładniczo dokładność, możesz po prostu spróbować oszacować liczbę akceptowalnych ścieżek (lub wyświetlić jako losowy spacer dyn sys) i sprawdzić, czy jest to dokładnie zero, czy też kilka (oczywiście wymagałoby to wykładniczo dokładnego pomiaru, tak samo jak w przypadku systemu dynamicznego).
Artem Kaznatcheev
Dziękuję za to. Nie znam zbyt wielu teoretycznych wyników dotyczących obliczeń analogowych.
pseudonim