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

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.

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.