Czym jest Problem spełnialności boolowskiej (Boolean satisfiability problem)?
Problem spełnialności boolowskiej, najczęściej skracany do SAT, polega na stwierdzeniu, czy dla danego wyrażenia logicznego zapisanego w algebrze Boole’a istnieje przypisanie wartości prawda–fałsz, które sprawi, że całe wyrażenie przyjmie wartość prawda. W praktyce sprowadza się to do pytania, czy formuła zawierająca operatory AND, OR i NOT jest wewnętrznie niesprzeczna. SAT to pierwsze zadanie, które w 1971 roku Stephen Cook z University of Toronto sklasyfikował jako NP-zupełne, a niezależnie od niego podobny wynik podał Leonid Levin. Oznacza to, że SAT stanowi punkt odniesienia dla całej klasy problemów, które dają się zweryfikować w czasie wielomianowym, lecz nie znamy dla nich algorytmu działającego w czasie wielomianowym w najgorszym przypadku.
Kontekst historyczny
Początków badania nad SAT należy szukać w pracach Claude’a Shannona nad przekształcaniem obwodów logicznych w latach 40., jednak dopiero dowód Cooka-Levina nadał mu fundamentalne znaczenie teoretyczne. Od lat 90. dynamiczny rozwój tzw. solverów SAT, wspierany przez konkursy SAT Competition, znacząco przyspieszył dzięki heurystykom opartym na uczeniu maszynowym oraz technikom propagacji jednostkowej.
Jak dokładnie działa Problem spełnialności boolowskiej (Boolean satisfiability problem)
Instancję SAT przedstawia się najczęściej w postaci klauzulowej, gdzie formułę zapisuje się jako koniunkcję klauzul, a każda klauzula jest alternatywą literałów. Popularny algorytm DPLL (Davis–Putnam–Logemann–Loveland) systematycznie wybiera zmienną, przypisuje jej wartość, propaguje narzucone tym faktem konsekwencje i w razie sprzeczności cofa się, aby spróbować innego przypisania. Nowoczesne rozwiązywacze SAT opierają się na rozszerzeniu DPLL zwanym Conflict-Driven Clause Learning, gdzie w chwili wykrycia sprzeczności powstaje nowa klauzula uniemożliwiająca powrót do tej samej ślepej uliczki. Dzięki temu przestrzeń przeszukiwania kurczy się szybciej niż przy klasycznym przeszukiwaniu w głąb.
Zastosowania w praktyce
W sztucznej inteligencji SAT pomaga przekształcać problemy planowania, wnioskowania i optymalizacji w formuły logiczne, które następnie rozwiązuje się za pomocą wyspecjalizowanych solverów. Przykładowo, przy automatycznym planowaniu ruchu robotów kolejność czynności przekłada się na formułę SAT, a rozwiązywacz weryfikuje, czy istnieje sekwencja kroków spełniająca wszystkie ograniczenia czasowe i przestrzenne. W erytmetyce formalnej SAT wspiera dowód twierdzeń poprzez redukcję formuł pierwszego rzędu, natomiast w weryfikacji układów scalonych minimalizuje ryzyko błędów produkcyjnych, wykazując, że dany obwód logiczny nie osiągnie niedozwolonego stanu.
Zalety i ograniczenia
Największą zaletą SAT jest jego uniwersalność: dowolny problem w klasie NP da się zredukować do postaci SAT, co czyni go wspólnym językiem dla rozmaitych technik AI. Zaawansowane heurystyki, clause learning i restarty umożliwiają praktyczne rozwiązywanie instancji obejmujących miliony zmiennych. Ograniczeniem pozostaje fakt, że w najgorszym przypadku czas obliczeń rośnie wykładniczo, a dobór heurystyk bywa wrażliwy na charakter danych wejściowych, co może prowadzić do nieprzewidywalnych czasów działania.
Na co uważać?
Redukując problem do SAT, warto zadbać o minimalizację liczby zmiennych i klauzul, ponieważ niepotrzebna redundancja znacząco obciąża solver. Istotne jest także monitorowanie zasobów pamięci, zwłaszcza przy clause learning, gdzie liczba wygenerowanych klauzul może rosnąć lawinowo. W projektach krytycznych czasowo zaleca się hybrydowe podejście: wstępne uproszczenie instancji metodami symbolicznego BDD lub programowania liniowego, a dopiero potem przekazanie do solvera SAT.
Dodatkowe źródła
Rozbudowane omówienie właściwości SAT oraz przykładów redukcji można znaleźć w podręczniku Handbook of Satisfiability. Dostępne jest również przystępne wprowadzenie na stronie Wikipedia. Aktualne publikacje konferencyjne i raporty badawcze można śledzić w serwisie arXiv.
