Odpowiedzi:
Wyszukiwanie rozdzielczości (po prostu zastosowanie reguły rozdzielczości z pewną dobrą heurystyką) to kolejna możliwa strategia dla solverów SAT. Teoretycznie jest on wykładniczo silniejszy (tzn. Istnieją problemy, dla których ma wykładnicze, krótsze dowody) niż DPLL (który robi tylko rozpoznawanie drzew, chociaż można go rozszerzyć o naukę nogood, aby zwiększyć jego moc - czy to czyni go tak potężnym, jak ogólna rozdzielczość jest nadal o ile mi wiadomo), ale nie znam rzeczywistej implementacji, która działałaby lepiej.
Jeśli nie ograniczasz się do pełnego wyszukiwania, to WalkSat jest lokalnym narzędziem do wyszukiwania, które może być wykorzystane do znalezienia satysfakcjonujących rozwiązań i w wielu przypadkach przewyższa wyszukiwanie oparte na DPLL. Nie można go jednak użyć do udowodnienia niezadowolenia, chyba że buforuje się wszystkie zadania, które się nie powiodły, co oznaczałoby wykładnicze wymagania dotyczące pamięci.
Edycja: Zapomniałem dodać - można również użyć płaszczyzn cięcia (redukując SAT do programu liczb całkowitych). W szczególności cięcia Gomory wystarczą, aby optymalnie rozwiązać dowolny program liczb całkowitych. Ponownie w najgorszym przypadku może być potrzebna liczba wykładnicza. Myślę, że książka Arora & Barak Computational Complexity zawiera jeszcze kilka przykładów systemów dowodowych, które teoretycznie można by wykorzystać do rozwiązywania problemów takich jak SAT. Znów nie widziałem szybkiej implementacji czegokolwiek oprócz metod opartych na DPLL lub lokalnych metodach wyszukiwania.
Propagacja ankiety to kolejny algorytm, który z powodzeniem zastosowano w przypadku niektórych rodzajów problemów SAT, zwłaszcza przypadkowych instancji SAT. Podobnie jak WalkSAT, nie można go wykorzystać do udowodnienia niezadowolenia, ale opiera się on na bardzo różnych pomysłach (algorytmach przekazywania wiadomości) od WalkSAT.
Istnieją solwery SAT oparte na wyszukiwaniu lokalnym. Zobacz na przykład ten artykuł do prezentacji.
Można również powiedzieć, że wszystkie solwery CSP są również solverami SAT. I o ile mi wiadomo, dwie metody stosowane w CSP:
Wyszukiwarka drzew Monte Carlo (MCTS) osiągnęła ostatnio imponujące wyniki w grach takich jak Go. Podstawową ideą jest przeplatanie losowej symulacji z wyszukiwaniem drzewa. Jest lekki i łatwy do wdrożenia, strona centrum badań, do której się odnalazłem, zawiera również wiele przykładów, dokumentów i trochę kodu.
Previti i in. [1] przeprowadził wstępne dochodzenie w sprawie MCTS w odniesieniu do SAT. Nazywają one oparty na MCTS algorytm wyszukiwania UCTSAT („górne granice ufności stosowane do drzew SAT”, jeśli wolisz). Porównali wydajność DPLL i UCTSAT w instancjach z repozytorium SATLIB, aby sprawdzić, czy UCTSAT wygeneruje znacznie mniejsze drzewa wyszukiwania niż DPLL.
W przypadku jednolitych przypadkowych kolorystyk 3-SAT i płaskich wykresów o różnych rozmiarach nie było istotnych różnic. Jednak UCTSAT działał lepiej w rzeczywistych instancjach. Średnie rozmiary drzew (pod względem liczby węzłów) dla czterech różnych instancji analizy uszkodzeń obwodu SSA były w kilku tysiącach dla DPLL, a zawsze mniejsze niż 200 dla UCTSAT.
DPLL nie określa ściśle kolejności wyświetlania zmiennych i istnieje wiele interesujących badań dotyczących optymalnych strategii atakowania zmiennych. niektóre z nich są uwzględnione w logice wyboru zmiennych w algorytmach SAT. w pewnym sensie niektóre z tych badań są wstępne, ponieważ pokazują, że różne zmienne kolejność ataków prowadzą do różnych ograniczeń sekwencyjnych (co jest silnie skorelowane z twardością instancji), a opracowanie najbardziej skutecznej heurystyki lub strategii wykorzystania tej pozornie kluczowej wiedzy wydaje się być na wczesnych etapach badań.