Solver SMT to solver SAT + procedura decyzyjna
Solver SAT to rozwiązanie problemu decyzyjnego: problem SAT to problem decyzyjny. Ponadto ten problem decyzyjny jest „samowystarczalny”:
Problem SAT jest samowystarczalny, to znaczy każdy algorytm, który poprawnie odpowiada, jeśli wystąpienie SAT jest możliwe do rozwiązania, może zostać użyty do znalezienia zadowalającego przypisania
- ( wikipedia )
Oznacza to, że solwery SAT mogą również dać satysfakcjonujące zadanie, oprócz rozstrzygnięcia problemu.
Solvery TL; DR SMT rozwiązują problem uogólnienia SAT w zależności od typów / ograniczeń dozwolonych w teorii. Co więcej, umożliwiają także kodowanie relacji typu wyższego poziomu niż pozwalają kodowania SAT.
Solver SAT zwykle zajmuje się wieloma pojedynczymi zmiennymi boolowskimi, które są powiązane tylko przez klauzule / ograniczenia CNF . Teoria SMF QF_BV (bitvector bez kwantyfikatora) to w zasadzie solver SAT + więcej informacji na temat relacji. Na przykład solver QF_BV SMT można zredukować do SAT 1 . Po co więc korzystać z solvera QF_BF SMT? Główną zaletą jest to, że w SAT liczba całkowita jest reprezentowana przez różne zmienne, które na pierwszy rzut oka mogą wydawać się niepowiązane. Solver SAT spędziłby dużo czasu na uczeniu się prostych relacji, takich jak na poziomie liczb całkowitych(A=B)∧(B=C)⟹(A=C) , podczas gdy solver SMT wie, że poszczególne bity są od samego początku powiązane w ten sposób, ponieważ język SMF QF_BV jest na poziomie liczb całkowitych (stała szerokość bitów). Zatem solver QF_BV SMT może argumentować na poziomie liczby całkowitej, oprócz poziomu bitów.
- Zobacz Solver Beaver SMT, który może nawet wygenerować równoważny problem SAT, który musiałby zostać rozwiązany.
Podczas gdy solver QF_BV SMT ma tę przewagę nad solverem SAT, nie sądzę, że jest to zaleta złożoności: oba są zasadniczo równoważne i zajmują wykładniczy czas na rozwiązanie ich najgorszych problemów. Ale praktycznie, solver QF_BV SMT może być znacznie szybszy z powodu tej dodatkowej wiedzy. Zobacz moją odpowiedź na temat limitów solverów SMT , na przykład czegoś, co uważane jest za „twarde”, które (obecne) solwery SMT QF_BV i solwery SAT mogłyby się zakrztusić.
Istnieją również solwery SMT, które próbują rozwiązać nawet trudniejsze problemy niż Boolean Satisfiable (na przykład dopuszczając typy i ograniczenia na liczbach rzeczywistych lub dopuszczając kwantyfikatory); oczywiście są one teoretycznie co najmniej tak wolne jak solver SAT. Te solwery SMT są rozwiązaniem uogólnienia problemu SAT; zamiast używać zmiennych binarnych, każda „teoria” dopuszcza relacje / ograniczenia w różnych domenach, takie jak realia lub ograniczenia ilościowe (dla wszystkich).
Przysłowie twierdzące
Zautomatyzowany twierdzenie Prover jest solver, że biorąc pod jakiś system dowód niektórych założeń oraz celu udowodnienia, będzie „wypełnić luki” pomiędzy założeniami i bramki. Będzie też miał jakiś weryfikator do sprawdzania dowodów (który działa szybko). Potwierdzacz twierdzeń może polegać na rozwiązaniu SAT, aby wypełnić puste pola; w rzeczywistości, jeśli i istnieje praktyczny algorytm do rozwiązywania problemów związanych z NP-zupełnym, można potencjalnie udowodnić prawie wszystkie przydatne rzeczy możliwe do udowodnienia (w rozsądnym czasie):P=NP
Ale takie zmiany mogą blednąć w porównaniu z rewolucją, którą skuteczna metoda rozwiązywania problemów NP-zupełnych spowodowałaby w samej matematyce. Według Stephena Cooka [19]
... przekształciłoby matematykę, pozwalając komputerowi znaleźć formalny dowód dowolnego twierdzenia, które ma dowód o rozsądnej długości, ponieważ dowody formalne można łatwo rozpoznać w czasie wielomianowym. Przykładowe problemy mogą obejmować wszystkie problemy z nagrodami CMI.
- ( wikipedia )
[19]: Cook, Stephen (kwiecień 2000). Problem P a NP. Clay Mathematics Institute (PDF) .
Powodem tego byłoby to, że „weryfikatory formalne można łatwo rozpoznać w czasie wielomianowym” za pomocą weryfikatora, a oznaczałoby, że na problemy, które można zweryfikować w czasie wielomianowym, można również odpowiedzieć w czasie wielomianowym.P=NP
Ale na razie automatyczne twierdzenie głównie dowodzi, że korzysta z algorytmów heurystycznych lub wykładniczych algorytmów czasu (ale nadal są pomocne).
Solver ograniczeń
Są to zwykle przeformułowania solverów SAT / SMT na inne języki. Jeśli kiedykolwiek użyłeś jakiegoś solwera SAT / SMT do rozwiązania problemu, naprawdę możesz pokochać niedeterministyczną zdolność solverów. Oznacza to, że zamiast mówić komputerowi, jak coś zrobić, mówisz mu, co chcesz , tj. jakie właściwości mają mieć dane wyjściowe, a solver SAT / SMT w niedeterministyczny sposób „wypełni je”, nie zawracając sobie głowy szczegółami implementacji. Ten rodzaj paradygmatu programistycznego jest bardzo atrakcyjny i nazywa się programowaniem ograniczeń , a do działania musi używać solvera ograniczającego (który może używać solwera SAT / SMT w backendie, w zależności od typów i ograniczeń, które pozwala na użycie) .
Ale widzę ludzi nazywających Z3 twierdzeniem twierdzącym. Więc nie wiem, jak wymazać te warunki.
AFAIK, Z3 to zestaw wielu narzędzi, w tym solver SMT, kilka języków dowodzenia / sprawdzania modeli i wiele innych.
A jaki jest najbardziej ogólny termin dla nich wszystkich?
Myślę, że uogólnieniem problemu satysfakcji są Teorie Modulo Satisfiable , a zatem „solver SMT” byłby najbardziej ogólny z nich wszystkich. Jednak nie wszystkie rzeczywiste implementacje solvera SMT rozwiązują wszystkie teorie, więc nie oznacza to, że wszystkie solvery SMT są jednakowo ogólne.