Konwertowanie problemów matematycznych na instancje SAT

Chcę zmienić problem matematyczny, który mam, w logiczny problem satysfakcji (SAT), a następnie rozwiązać go za pomocą SAT Solvera. Zastanawiam się, czy ktoś zna instrukcję, przewodnik lub cokolwiek, co pomoże mi przekonwertować mój problem na instancję SAT.

Chcę też rozwiązać ten problem w czasie lepszym niż wykładniczy. Mam nadzieję, że Solver SAT mi pomoże.

Rozdział 2 Podręcznika SAT (autorstwa Stevena Prestwicha) omawia, jak dogłębnie przekształcić dyskretne problemy decyzyjne w CNF. (Niestety nie sądzę, że jest dostępna wersja robocza online - prawdopodobnie najlepiej skonsultować się z lokalną biblioteką.) Kilka innych odniesień cytowanych w dziwacznym przeglądzie Magnusa Björka Przydatne są również skuteczne techniki kodowania SAT .

Jeśli twoje problemy są ciągłe lub szczególnie interesują cię systemy nierówności, wówczas bardziej prawdopodobne są inne rodzaje rozwiązań. Jak podkreśla Kyle , solwery SMT (takie jak Z3 , Yices lub OpenSMT ) mogą być przydatne, chociaż tradycyjnie teorie SMT koncentrują się głównie na weryfikacji oprogramowania komputerowego, więc solwery SMT zwykle świetnie wspierają takie rzeczy, jak wyrażenia obejmujące przedziały liczb całkowitych , ale może źle działać w przypadku ograniczeń iniekcji. W przypadku problemów, które są naturalnie wyrażane jako systemy nierówności, należy pokonać CPLEX (był dostępny do użytku akademickiego za darmo i nadal może być). W przypadku niektórych problemów decyzyjnych kombinatorycznych (takich jak znalezieniepakiety prostokątów w kwadrat ), rozwiązania ograniczające, takie jak stwory, przewyższają rozwiązania SAT i często są łatwiejsze w użyciu.

O ile nie przekładasz problemów matematycznych na instancje SAT jako ćwiczenie edukacyjne, Twój czas będzie znacznie bardziej owocnie spędzony na poznawaniu teorii modulo satysfakcji . SMT pozwoli ci wyrażać równania i inne ograniczenia znacznie bardziej naturalnie niż jako instancje Boolean SAT. Niektóre solwery SMT obsługują egzystencjalne i uniwersalne kwantyfikatory, pozwalając wyjść poza NP i wyrażać problemy PSPACE.

Oprócz tego, że są bardziej ekspresyjne, solwery SMT są szybsze. Nie P = NP szybciej, ale bardziej wydajnie, ponieważ dobry solver SMT nie odrzuca specyficznych dla teorii informacji strukturalnych, które pomagają poprowadzić solver przez przestrzeń poszukiwań. Wykonanie redukcji Karp bezpośrednio do instancji SAT zmusza solver SAT do ponownego uczenia się całej tej struktury, często kosztem wykładniczym. Na przykład fakt, że dodawanie jest przemienne, jest tracony zarówno w rozwiązaniach SAT opartych na DPLL, jak i na wyszukiwaniu lokalnym; solver nie zdaje sobie sprawy, że ma do czynienia z liczbami! Aby uniknąć wypróbowania wszystkich permutacji x + y + z = 10, solver SAT potrzebuje kodu łamiącego symetrię, który wymaga wykrycia automorfizmu grafów. Najlepsze obecne algorytmy rozpoznawania grafów automorfizmu wymagają wykładniczego czasu w stosunku do liczby wierzchołków w najgorszym przypadku,

Dwa narzędzia konwertujące języki wysokiego poziomu na SMT lub CNF.

CVC Składnia jest zbliżona do CAS.

CBMC Konwertuje program C na CNF, pozwalając na stwierdzenia. Asercje są albo zawsze prawdziwe, albo w przypadku fałszu znaleziono dane wejściowe z kontrprzykładem. CBMC rozwija pętle, więc niektóre programy C mają wykładniczo duże CNF / SMT.