Które problemy z SAT są łatwe?

Jakie są „łatwe regiony” dla satysfakcji? Innymi słowy, wystarczające warunki, aby niektóre solver SAT mógł znaleźć zadowalające zadanie, pod warunkiem, że istnieje.

Jednym z przykładów jest sytuacja, w której każda klauzula dzieli zmienne z kilkoma innymi klauzulami, ze względu na konstruktywny dowód LLL, czy są jakieś inne wyniki w tym zakresie?

Istnieje spora literatura na temat łatwych regionów dla propagowania przekonań, czy jest coś podobnego do satysfakcji?

Chyba znasz klasyczny wynik Schaefera ze STOC'78, ale na wszelki wypadek.

10.1145 / 800133.804350

Schaefer udowodnił, że jeśli SAT jest parametryzowany przez zestaw relacji dozwolonych w każdym przypadku, to istnieje tylko 6 możliwych do prześledzenia przypadków: 2-SAT (tj. Każda klauzula jest binarna), Horn-SAT, dual-Horn-SAT, affine-SAT ( rozwiązania równań liniowych w GF (2), 0-poprawne (relacje spełnione przez przypisanie all-0) i 1-poprawne (relacje spełnione przez przypisanie all-1).

Nie jestem pewien, czy tego właśnie szukasz, ale istnieje spora literatura na temat przejścia fazowego 3-SAT.

Monasson, Zecchina, Kirkpatrcik, Selman i Troyansky mieli w naturze artykuł, który mówi o przejściu fazowym losowego k-SAT. Zastosowali parametryzację stosunku klauzul do zmiennych. W przypadku losowego 3-SAT ustalili liczbowo, że punkt przejścia wynosi około 4,3. Powyżej tego punktu losowe instancje 3-SAT są nadmiernie ograniczone i prawie na pewno nie można ich usatysfakcjonować, a poniżej tego punktu problemy są ograniczone i zadowalające (z dużym prawdopodobieństwem). Mertens, Mezard i Zecchina stosują procedury wnękowe do oszacowania punktu przejścia fazowego z wyższym stopniem dokładności.

Daleko od punktu krytycznego, „głupie” algorytmy działają dobrze w zadowalających przypadkach (walk sat itp.). Z tego, co rozumiem, deterministyczne czasy działania solvera rosną wykładniczo na przejściu fazowym lub w jego pobliżu (zobacz tutaj więcej dyskusji?).

Bliski kuzyn propagacji przekonań, Braunstein, Mezard i Zecchina wprowadzili propagację badań, która, jak się uważa, rozwiązuje zadowalające przypadki 3-SAT w milionach zmiennych, nawet bardzo blisko przejścia fazowego. Mezard ma wykład tu na szklanki typu spin (teoria, którą wykorzystał w analizie losowych NP-complete przejść fazowych) i Maneva ma wykład tutaj na propagację badań.

Z drugiej strony nadal wygląda na to, że nasze najlepsze solwery potrzebują wykładniczej ilości czasu na udowodnienie niezadowolenia. Zobacz tutaj , tutaj i tutaj, aby znaleźć dowody / dyskusje na temat wykładniczego charakteru niektórych powszechnych metod dowodzenia niezadowolenia (procedury Davisa-Putnama i metody rozwiązywania).

Trzeba uważać na „łatwość” lub „twardość” przypadkowych problemów z NP-Complete. Wyświetlanie problemu z NP-Complete, przejście fazowe nie daje żadnej gwarancji, gdzie są trudne problemy, a nawet czy w ogóle występują. Na przykład problem cyklu Hamiltoniain na losowych wykresach Erdosa-Renyi jest łatwo możliwy nawet w krytycznym punkcie przejścia lub w jego pobliżu. Problem partycji liczbowej nie wydaje się mieć żadnych algorytmów, które rozwiązywałyby go dobrze w zakresie prawdopodobieństwa 1 lub 0, nie mówiąc już o progu krytycznym. Z tego, co rozumiem, losowe problemy 3-SAT mają algorytmy, które działają dobrze w zadowalających przypadkach prawie na poziomie progu krytycznego lub poniżej niego (propagacja ankiety, spacer, itd.), Ale nie ma wydajnych algorytmów powyżej progu krytycznego, aby udowodnić niezadowolenie.

Istnieje wiele wystarczających warunków. W pewnym sensie znaczna część teoretycznej CS została poświęcona gromadzeniu tych warunków - stała zdolność do pomiaru parametrów, 2-SAT, losowa 3-SAT o różnych gęstościach itp.

jak dotąd w literaturze nie ma szerokiego rozpoznania tej koncepcji, ale wykres klauzulowy problemu SAT (wykres z jednym węzłem na klauzulę i węzły są połączone, jeśli klauzule dzielą zmienne), a także inne powiązane wykresy reprezentacji SAT wydaje się mieć wiele podstawowych wskazówek co do tego, jak średnio będzie trudna instancja.

wykres klauzulowy może być analizowany za pomocą wszelkiego rodzaju algorytmów graficznych, jest pozornie naturalną miarą „struktury” i ma silne powiązania z pomiarem / oszacowaniem twardości, i wydaje się, że badania tej struktury i jej implikacji są wciąż na bardzo wczesnym etapie gradacja. nie jest wykluczone, że badania punktu przejściowego, tradycyjny / dobrze zbadany sposób podejścia do tego pytania, mogą ostatecznie zostać połączone w strukturę grafu klauzulowego (do pewnego stopnia już to ma). innymi słowy, punkt przejściowy w SAT może występować „z powodu” struktury grafu klauzulowego.

oto jedno doskonałe odniesienie w tym zakresie, praca doktorska Herwiga, jest wiele innych.

[1] Rozkładanie problemów związanych z satysfakcją lub Korzystanie z wykresów w celu uzyskania lepszego wglądu w problemy dotyczące satysfakcji , Herwig 2006 (83pp)

Łatwo jest przenieść wszystkie wystąpienia w pobliżu punktu „przejścia” tak daleko od punktu „przejścia”, jak się chce. Ruch obejmuje wielomianowy wysiłek czasu / przestrzeni.

Jeśli instancje daleko od punktu „przejścia” są łatwiejsze do rozwiązania, to te w pobliżu punktu przejścia muszą być równie łatwe do rozwiązania. (Transformacje wielomianowe i wszystko.)

ten ważny artykuł [1] Toby'ego Walsha dotyczy przejścia SAT, mierzonego w stosunku klauzula / zmienna. jednak idzie dalej w pomiarze właściwość o nazwie constrainedness , . jest to szorstka, a może naturalna miara twardości, tak że problemy z ograniczeniami lub ograniczeniami są łatwiejsze niż ograniczenia w krytycznym punkcie pośrednim.$\kappa$

znajduje pozorną fraktalną strukturę samopodobieństwa twardych instancji w parametrze ograniczenia, tak że jako solver DP (LL) podczas wyszukiwania ma tendencję do znajdowania podproblemów z tym samym ograniczeniem krytycznym bez względu na to, która zmienna zostanie wybrana obok gałęzi. istnieje dalsza analiza struktury fraktalnej w instancjach SAT (takich jak wymiar Hausdorffa wzorów SAT i związek z twardością) np. [2,3]

inną nieco ze sobą powiązaną linią dochodzenia tutaj jest związek małych wykresów światowych ze (twardą) strukturą SAT np. [4,5]

oczywiście standardowy punkt w tym obszarze dotyczy tego, że bardzo ostateczna odpowiedź na to pytanie byłaby z natury bliska P NP$\stackrel{?}{=}$ , lub że taki dowód byłby (będzie?) najlepszy / bliski - ostateczna odpowiedź na pytanie.

[1] Ostrze noża ograniczającego autorstwa Toby'ego Walsha 1998

[2] SAMODPOWIEDNOŚĆ ZADOWOLONYCH EKSPRESÓW BOOLEJSKICH ODszyfrowanych w kategoriach UKŁADOWYCH SYSTEMÓW FUNKCJI BEZPOŚREDNICH WYKRESU Ni i Wen

[3] Wizualizacja wewnętrznej struktury instancji SAT (raport wstępny) Sinz

[4] Szukaj w małym świecie według Walsha 1999

[5] Modelowanie bardziej realistycznych problemów SAT przez Slater 2002