SAT jest NP-zupełny, a mimo to solvery rozwiązują ogromne instancje
NP-zupełność opisuje najgorszy przypadek całej klasy instancji, nie gwarantuje, że każda rzeczywista formuła SAT będzie trudna. Nowoczesne solvery konfliktowe, zwłaszcza CDCL, nie przeglądają po prostu wszystkich 2^n przypisań. Uczą się z konfliktów, dodając nowe klauzule blokujące całe rodziny błędnych decyzji, korzystają z dynamicznych heurystyk wyboru zmiennych, restartów i usuwania mniej użytecznych klauzul. Dzięki temu potrafią rozwiązywać bardzo duże ustrukturyzowane problemy z weryfikacji sprzętu, planowania czy model checking. Nie przeczy to NP-zupełności: nadal mogą istnieć instancje wymagające ogromnej pracy i nie znamy wielomianowej gwarancji dla wszystkich przypadków.
Najgorszy przypadek nie jest opisem każdego przypadku
Stwierdzenie „SAT jest NP-zupełny” dotyczy rodziny wszystkich instancji i relacji redukcji. Nie mówi, że formuła z milionem zmiennych musi być trudniejsza od formuły z tysiącem. Struktura może sprawić, że w ogromnym problemie szybko pojawi się sprzeczność albo że decyzje propagują się niemal automatycznie. Z kolei mała, specjalnie skonstruowana instancja może być nieprzyjemna dla konkretnego solvera.
Uczenie się na konflikcie
CDCL, czyli conflict-driven clause learning, rozwija klasyczne przeszukiwanie DPLL. Gdy częściowe przypisanie prowadzi do sprzeczności, solver analizuje graf implikacji i wyprowadza klauzulę opisującą przyczynę konfliktu. Dodanie jej do bazy sprawia, że program nie musi ponownie przechodzić przez tę samą rodzinę błędnych wyborów. Jest to rodzaj pamięci: porażka w jednej gałęzi staje się wiedzą użyteczną później.
Heurystyki, restarty i zarządzanie wiedzą
Współczesne solvery wybierają zmienne na podstawie historii konfliktów, okresowo restartują wyszukiwanie i usuwają część wyuczonych klauzul. Restarty nie oznaczają utraty całego postępu, bo zachowana wiedza może sprawić, że kolejne przejście przez przestrzeń jest zupełnie inne. Literatura o CDCL podkreśla właśnie współdziałanie konflikt analysis, heurystyk, lazy data structures, restartów i polityk kasowania klauzul.
Dlaczego zastosowania przemysłowe są możliwe
Formuły powstające z obwodów, programów, planów czy konfiguracji mają często dużo więcej struktury niż losowy zbiór klauzul. Powtarzalne podukłady i silne zależności dają solverom materiał do propagacji i uczenia się. To jedna z przyczyn, dla których SAT stał się praktycznym silnikiem rozwiązywania problemów daleko poza logiką podręcznikową.
Nie należy odwracać wniosku
Sukces solverów nie jest dowodem P=NP. Algorytm może być fenomenalny dla ogromnej części instancji spotykanych w praktyce, a mimo to nie mieć wielomianowej granicy czasu dla wszystkich wejść. To rozróżnienie między teorią najgorszego przypadku a inżynierią algorytmów jest kluczowe: obie mówią prawdę, ale odpowiadają na inne pytania.
Najgorszy przypadek i typowe instancje to inne pytania
Klasa złożoności opisuje gwarancję dla całej rodziny wejść. Solver SAT może więc znakomicie działać na tysiącach czy milionach zmiennych w wielu zastosowaniach i jednocześnie nie mieć wielomianowej gwarancji dla wszystkich możliwych formuł. W praktyce znaczenie ma struktura: powtarzające się motywy, ograniczone zależności, wymuszone wartości i konflikty pojawiające się wcześnie. CDCL zamienia konflikty w nowe klauzule, które blokują całe grupy przyszłych błędnych decyzji, dzięki czemu nie musi bezmyślnie przechodzić drzewa 2^n przypisań. To przykład ogólniejszej lekcji: wynik NP-zupełności wyznacza granicę gwarancji, ale nie przewiduje czasu dla konkretnego rozkładu danych z przemysłu.
Praktyczny sukces nie rozstrzyga P kontra NP
Fakt, że współczesny solver potrafi błyskawicznie rozwiązać bardzo duży przypadek SAT, nie jest dowodem na P=NP. Aby taki wniosek był uzasadniony, potrzebny byłby algorytm z wielomianową gwarancją dla wszystkich instancji. Rekordowe wyniki solverów pokazują coś innego: teoria najgorszego przypadku i praktyczna wydajność na ustrukturyzowanych danych odpowiadają na różne pytania i mogą jednocześnie być prawdziwe.