Algorytmy SAT nie oparte na DPLL

Odpowiedzi:

21

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.

Optować
źródło
9
Wykazano, że DPLL z uczeniem się klauzul (lub uczeniem się nogood, jak to nazywasz) i restartuje się jako równoważne ogólnej rozdzielczości.
Jan Johannsen
1
@JanJohannsen, czy to jest artykuł, do którego się odwołujesz? arxiv.org/abs/1107.0044
Radu GRIGore 24.11.11
5
Tak, poprawa nastąpiła również w następującym artykule: Knot Pipatsrisawat i Adnan Darwiche. O sile uczenia się klauzul solverów SAT jako silników rozdzielczości. Artificial Intelligence 175 (2), 2011, ss. 512–525. dx.doi.org/10.1016/j.artint.2010.10.002
Jan Johannsen
3
Podczas gdy praca Beame i in. połączone przez Radu Grigore pokazuje, że ogólna rozdzielczość jest symulowana p przez algorytm DPLL ze szczególną, sztuczną strategią uczenia się, powyższy artykuł pokazuje to dla faktycznie wykorzystywanych strategii uczenia się naturalnego.
Jan Johannsen
12

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.

Timothy Chow
źródło
10

Istnieją solwery SAT oparte na wyszukiwaniu lokalnym. Zobacz na przykład ten artykuł do prezentacji.

ilyaraz
źródło
7

Można również powiedzieć, że wszystkie solwery CSP są również solverami SAT. I o ile mi wiadomo, dwie metody stosowane w CSP:

  • Wyczerpujący system plików DFS z przycinaniem przestrzeni wyszukiwania i sprawdzaniem spójności łuku, ewentualnie za pomocą golenia, aby zapewnić zachowanie spójności tak szybko, jak to możliwe.
  • Metody lokalne (wyszukiwanie tabu, symulowane wyżarzanie)
malejpavouk
źródło
4

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.

[1] Previti, Alessandro, Raghuram Ramanujan, Marco Schaerf i Bart Selman. „Poszukiwanie UCT w stylu Monte-Carlo dla logicznej satysfakcji”. W AI * IA 2011: Artificial Intelligence Around Man and Beyond, s. 177-188. Springer Berlin Heidelberg, 2011.

Juho
źródło
-4

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

vzn
źródło
4
Czy rozumiesz, że poprosiłem o algorytmy nieoparte na DPLL ?
Anonimowy
2
Czy rozumiesz, co oznacza „oparty” ? Powiedziałem : nie używaj moich pytań do komentowania wszystkiego, co chcesz skomentować!
Anonimowy
7
sam twierdzisz, że są oparte na DPLL. wydaje mi się, że to tak, jakby powiedzieć, że różne reguły przestawne dla simpleks dają ci algorytm, który nie jest algorytmem simpleksowym
Sasho Nikolov
7
Zgadzam się z Sasho. Ponadto badania nad heurystykami o zmiennej kolejności zdecydowanie nie są na wczesnym etapie. Znaczenie zostało uświadomione dawno temu (wyobraź sobie konsekwencje doskonałej wyroczni) i wiele czasu poświęcono na ich analizę. Heurystyka porządkowania wartości stała się bardziej interesująca w solverach CSP iz jakiegoś powodu nie sądzę, aby badania nad nimi były tak dynamiczne jak w przypadku porządkowania zmiennych.
Juho
4
Mówiąc ściślej, wstępne badania nad heurystykami o zmiennej kolejności sięgają lat 70. Jeśli jesteś zainteresowany, mogę wykopać odpowiednie referencje dla ciebie.
Juho