Zwiększanie konkurencyjności solverów SAT dzięki wyspecjalizowanym algorytmom

11

Jakie są przeszkody w konkurowaniu solverów SAT ze specjalistycznymi algorytmami graficznymi? Innymi słowy, czy jest możliwe oczekiwanie od solverów SAT, które mogą zastąpić rolę projektanta algorytmów - tj. Być w stanie automatycznie rozpoznać strukturę problemu, a następnie rozwiązać go tak szybko, jak specjalistyczny algorytm?

Oto kilka przykładów, które moim zdaniem stanowią wyzwanie dla dzisiejszych solverów SAT:

  • Zliczanie niezależnych zestawów wielkości . Kodowanie „x jest niezależnym zestawem wielkości k” daje dużą formułę, którą trudno rozwiązać. Idealny solver SAT rozpoznałby, że ten problem jest łatwy na ograniczonym wykresie szerokości drzewa z dodatkiem dodatkowej zmiennej „count” dla worków.k

  • Znalezienie minimalnego drzewa Steiner. Ponownie, „drzewo Steinera” ma globalne ograniczenie, jednak wyspecjalizowany algorytm (jak tutaj ) ułatwia zadanie, dodając dodatkową zmienną

  • Każdy problem, który sprowadza się do idealnych dopasowań planarnych.

Jarosław Bułatow
źródło
czy to się już nie dzieje? Popularną sztuczką jest zredukowanie problemu do SAT, a następnie uruchomienie solvera.
Suresh Venkat
Tak, ale czy są konkurencyjne? Zastanawiam się, czy istnieje jakiś solver SAT, który mógłby wziąć prosty zestaw ograniczeń opisujących Eulerian podgraph wykresu płaskiego i wykonać #SAT w czasie wielomianowym
Jarosław Bułatow

Odpowiedzi:

7

Jest ładny papier, który pomaga zwizualizować wewnętrzną strukturę instancji SAT. Zobacz Wizualizacja wystąpień i uruchomień algorytmu DPLL autorstwa Carstena Sienza (pojawiła się w SAT 2004). Zasadniczo rysuje wykres, który autor nazywa „grafem zmiennych interakcji” (zgodnie z niektórymi zasadami) w celu wizualizacji relacji między spełnionymi klauzulami. Autor pokazuje to przez kilka częściowych uruchomień DPLL.

Głównym twierdzeniem jest to, że te techniki wizualizacji można wykorzystać do wykrywania struktury i zaprojektowania odpowiedniego algorytmu. Jednak nadal nie jest jasne, w jaki sposób możemy skutecznie wykrywać struktury takie jak te przedstawione w artykule. Dobrze wiadomo, że algorytmy SAT dla jednego konkretnego problemu źle zachowują się w innych problemach. Jest więc „lunch bez posiłków”, chociaż o ile wiem, nie można formalnie stwierdzić tego twierdzenia.

Marcos Villagra
źródło
Wydaje mi się, że stosownym twierdzeniem „nie ma obiadu za darmo” jest „nie ma obiadu bez wyszukiwania” no-free-lunch.org . Zasadniczo nie możemy sobie pozwolić na wyszukiwanie wszystkich możliwych struktur problemowych i musimy popchnąć nasze wyszukiwanie w kierunku określonych struktur. Myślę, że to w porządku, ponieważ projektanci algorytmów ludzkich już to robią
Jarosław Bułatow