Problem satysfakcji z ograniczeń (CSP) vs. teoria modulo satysfakcji (SMT); z kodą na temat programowania ograniczeń

Czy ktoś odważy się wyjaśnić, jaki jest związek tych kierunków studiów, czy może nawet bardziej konkretną odpowiedź na poziomie problemów? Który obejmuje, który obejmuje niektóre powszechnie akceptowane formulacje. Jeśli dobrze to zrozumiałem, przechodząc z SAT do SMT, po prostu wchodzisz w pole CSP; i na odwrót, jeśli ograniczysz CSP do boolanów, zasadniczo mówisz o SAT i może kilku powiązanych problemach, takich jak #SAT. Myślę, że to wszystko jest jasne (np. Rozdział Kolaitisa i Vardiego „Logiczne podejście do spełnienia ograniczenia” w teorii modeli skończonych i jej zastosowaniachGrädel i in.), ale dla mnie mniej jasne jest, kiedy ograniczenia są „modulo teorią”, a kiedy nie? Czy SMT zawsze implikuje, że teoria używa tylko równości, a ograniczenia nierówności są zawsze w szerszym obszarze CSP? O ile mi wiadomo, często można wprowadzić zmienne luźne , więc rozróżnienie [jeśli istnieje] jest mniej niż oczywiste.

Stosunkowo nowy „Podręcznik satysfakcji” (IOP Press 2009) gromadzi zarówno problemy SMT, jak i CSP pod szerokim parasolem „satysfakcji”, ale biorąc pod uwagę sposób jego struktury (rozdziały napisane przez różnych autorów) tak naprawdę nie pomaga mi to rozgryźć .

Mam nadzieję, że terminologia stanie się mniej myląca, kiedy mówimy o programowaniu ograniczeń , które (analogicznie do terminu „programowanie matematyczne”), mam nadzieję, obejmuje minimalizowanie / maksymalizowanie niektórych funkcji obiektywnych. Artykuł w Wikipedii na temat programowania ograniczeń jest niestety tak niejasny, że nie mogę powiedzieć, czy tak się dzieje. To, co mogę zebrać z Essentials of Constraint Programming Frühwirtha i Abdennadhera (s. 56), to to, że „solver ograniczenia” zwykle zapewnia coś więcej niż tylko sprawdzanie satysfakcji, a uproszczenie itp. Jest ważne w praktyce.

Chociaż nie jest to właściwie pytanie badawcze teorii CS, nie oczekuję dobrych odpowiedzi na to pytanie na stronie licencjackiej CS.SE, biorąc pod uwagę to, co widziałem na https://cs.stackexchange.com/questions/14946/distinguish- decyzja-procedura-vs-smt-solver-vs-twierdzenie-prover-vs-ograniczenie-zol (który zawiera wiele słów, ale nie to, co uważałbym za prawdziwą odpowiedź, niestety).

SAT, CP, SMT, (większość) ASP radzą sobie z tym samym zestawem kombinatorycznych problemów optymalizacji. Pojawiają się jednak przy tych problemach pod różnymi kątami i przy różnych zestawach narzędzi. Różnice te dotyczą głównie sposobu, w jaki każde podejście konstruuje informacje o eksploracji przestrzeni poszukiwań. Moja działająca analogia jest taka, że ​​SAT jest kodem maszynowym, podczas gdy inne są językami wyższego poziomu.

Opierając się na mojej pracy magisterskiej na temat strukturalnej teorii CSP , doszedłem do wniosku, że pojęcie „struktury klauzulowej” jest niezbędne do ujednolicenia wszystkich tych paradygmatów i zrozumienia, jak się różnią. Każda klauzula instancji SAT reprezentuje zabronione częściowe przypisanie; klauzula taka jak zabrania częściowego przypisania który jednocześnie ustawia i na false, a na prawdziwe. Struktura klauzulowa kombinatorycznego problemu optymalizacji to jego reprezentacja jako instancja SAT, z wykorzystaniem odpowiedniego kodowania. Jednak struktura klauzuli obejmuje wszystkie$x_1 \lor \overline{x_2} \lor x_3$$\{(x_1,0),(x_2,1),(x_3,0)\}$$x_1$$x_3$$x_2$zakazane częściowe zadania, nie tylko te podane na początku. Struktura klauzuli jest zatem zwykle zbyt duża, aby manipulować bezpośrednio: zazwyczaj ma ona co najmniej wykładniczy rozmiar w liczbie zmiennych i może być nieskończona. Dlatego też struktura klauzuli musi być aproksymowana przy ograniczonej ilości miejsca. SAT / CP / SMT / ASP utrzymuje i aktualizuje mniej lub bardziej niejawną reprezentację podstawowej struktury klauzuli. Jest to możliwe, ponieważ jeśli wiadomo, że jedno częściowe przypisanie znajduje się w strukturze klauzuli, oznacza to, że istnieje również wiele innych klauzul. Na przykład powyższa klauzula SAT zabrania również częściowego przypisywania, które zawiera ją jako podzbiór, więc klauzule takie jak i$x_1 \lor \overline{x_2} \lor x_3 \lor x_4$$x_1 \lor \overline{x_2} \lor x_3 \lor \overline{x_4} \lor x_5$ są w strukturze klauzulowej tego wystąpienia.

Zachowane jest przybliżenie struktury klauzuli, aby zawęzić zestaw rozwiązań i pomóc ustalić, czy ten zestaw jest pusty. Podczas wyszukiwania niektóre przydziały częściowe mogą się nie zawierać w żadnym rozwiązaniu (nawet jeśli indywidualnie spełniają każde z ograniczeń w instancji). Są to tak zwane nogoods , termin wprowadzony przez („GNU”) Stallmana i Sussmana. Klauzula nogood znajduje się zatem w strukturze klauzuli i może być zawarta w przybliżeniu struktury klauzuli, jako zwarta reprezentacja wielu klauzul, które można przyciąć w poszukiwaniu rozwiązań. Dodanie nogoods do przybliżonej struktury klauzuli zachowuje wszystkie rozwiązania, ale lepiej przybliża te rozwiązania. Przybliżona struktura klauzul zwykle zmienia się w miarę postępu wyszukiwania. Ponadto sposób modelowania problemu w jednym z kombinatorycznych podejść do optymalizacji wpływa na strukturę klauzuli, często dość znacząco. Na przykład zmienne zdań mogą reprezentować przedziały, takie jak lub punkty, takie jakx = $x \le 5$$x = 5$. Stąd nie istnieje jedna ogólna struktura klauzuli, ale jedna związana z każdym wyborem reprezentacji, w zależności od tego, co reprezentują singletony (literały) struktury klauzuli.

Programowanie ograniczeń (CP) było tradycyjnie dyscypliną sztucznej inteligencji, skupiającą się na planowaniu, harmonogramie i problemach kombinatorycznych, a zatem odgrywa kluczową rolę w przypadku zmiennych, które mogą przyjąć więcej niż dwie wartości (ale zwykle tylko bardzo wiele). CP kładzie nacisk na wydajne wyszukiwanie i motywowany tradycyjnymi aplikacjami nadał centralną rolę ograniczeniu all-different(iniekcyjności), ale opracował również skuteczne propagatory wielu innych rodzajów ograniczeń. Formalne definicje CP istnieją już od co najmniej papierowej sieci ograniczeń Montanari z 1974 roku, z prekursorami wracającymi jeszcze wcześniej. Ta waga historii mogła przyczynić się do tego, że CP pozostawał w tyle za innymi podejściami do surowych wyników w ciągu ostatniej dekady. CP klasycznie utrzymuje przybliżenie dopełnienia struktury klauzuli, poprzez zestaw aktywnych domen dla zmiennych. Celem jest wyeliminowanie wartości z domen aktywnych, zbadanie struktury klauzul, próba przypisania wartości kandydujących do zmiennych i wycofanie, jeśli to konieczne.

Teorie modulo satysfakcji (SMT) wyszły ze społeczności weryfikacyjnej. Każda teoria w rozwiązaniu SMT tworzy domyślną reprezentację potencjalnie nieskończenie wielu klauzul SAT. Teorie zastosowane w SMT i ograniczenia zastosowane w CP odzwierciedlają ich różne zastosowania historyczne. Większość teorii rozważanych przez SMT ma związek z tablicami indeksowanymi liczbami całkowitymi, prawdziwie zamkniętymi polami, rzędami liniowymi i tym podobnymi; wynikają one ze statycznej analizy programów (w weryfikacji wspomaganej komputerowo) lub podczas formalizowania dowodów matematycznych (w automatycznym rozumowaniu). Natomiast w harmonogramowaniu i planowaniu ograniczenie iniekcji ma kluczowe znaczenie i chociaż standardowy język SMTLIB ma ograniczenie iniekcji od momentu jego powstania w 2003 r.distinctsymbol), do 2010 r. solwery SMT zaimplementowane tylko distinctza pomocą naiwnego algorytmu. Na tym etapie przeniesiono technikę dopasowania ze standardowego propagatora CP dla all-different, co przyniosło wielki efekt, gdy zastosowano ją do dużych list zmiennych; zobacz Alldifferent solver constraint w SMT autorstwa Banković i Marić, SMT 2010. Ponadto większość propagatorów CP jest zaprojektowana do rozwiązywania problemów z domenami skończonymi, podczas gdy standardowe teorie SMT radzą sobie z nieskończonymi domenami (liczbami całkowitymi, a ostatnio rzeczywistymi) od razu po wyjęciu z pudełka. SMT używa instancji SAT jako aproksymacji struktury klauzuli, odpowiednio wyodrębniając klauzule nogood z teorii. Dobry przegląd to Teorie modulo satysfakcji: Wprowadzenie i zastosowania De Moura i Bjørner, doi: 10.1145 / 1995376.1995394.

Programowanie zestawu odpowiedzi (ASP) wyszło z programowania logicznego. Ze względu na koncentrację na rozwiązywaniu bardziej ogólnego problemu znalezienia stabilnego modelu, a także dlatego, że umożliwia on zarówno kwantyfikację uniwersalną, jak i egzystencjalną, ASP przez wiele lat nie konkurowała z CP ani SMT.

Formalnie, SAT to CSP w domenach boolowskich, ale koncentracja w SAT na uczeniu się klauzul, dobrej heurystyce do wykrywania konfliktów i szybkich sposobach cofania się jest zupełnie inna niż tradycyjna koncentracja CSP na propagatorach, ustanawianie spójności i heurystyki dla porządkowania zmiennych. SAT jest zwykle wyjątkowo wydajny, ale w przypadku wielu problemów należy w pierwszej kolejności wyrazić problem jako instancję SAT. Użycie paradygmatu wyższego poziomu, takiego jak CP, może pozwolić na bardziej naturalne wyrażenie problemu, a następnie albo instancja CP może zostać przetłumaczona ręcznie na SAT, albo narzędzie może zająć się tłumaczeniem. Miły przegląd nakrętek i śrub SAT jest na temat nowoczesnych solverów do uczenia się klauzul autorstwa Pipatsrisawat i Darwiche, doi: 10.1007 / s10817-009-9156-3 .

Teraz przejdźmy od ogólników do dzisiejszych szczegółów.

W ciągu ostatniej dekady niektórzy ludzie w CP zaczęli koncentrować się na generowaniu leniwych klauzul (LCG). Jest to zasadniczo sposób na połączenie ze sobą propagatorów CP przy użyciu bardziej elastycznych technik podobnych do SMT, a nie raczej sztywnej abstrakcji domen aktywnych. Jest to przydatne, ponieważ istnieje długa historia opublikowanych propagatorów CP do skutecznego reprezentowania i rozwiązywania wielu rodzajów problemów. (Oczywiście podobny efekt można osiągnąć poprzez skoordynowane wysiłki we wdrażaniu nowych teorii dla solverów SMT.) LCG ma wydajność, która jest często konkurencyjna w stosunku do SMT, a w przypadku niektórych problemów może być lepsza. Krótki przegląd to artykuł CPAIOR 2010 Stuckeya Generowanie leniwych klauzul: połączenie siły rozwiązywania problemów SAT i CP (i MIP?) , Doi: 10.1007 / 978-3-642-13520-0_3. Warto również przeczytać dokument przedstawiający stanowisko Garcia de la Banda, Stuckey, Van Hentenryck i Wallace, który przedstawia skoncentrowaną na CP wizję przyszłości technologii optymalizacji , doi: 10.1007 / s10601-013-9149-z .

O ile mogę powiedzieć, wydaje się, że większość badań ostatnich SMT przeniosła się na zastosowania w metodach formalnych i sformalizowanej matematyce. Przykładem jest rekonstrukcja dowodów znalezionych przez solwery SMT wewnątrz systemów proofów, takich jak Isabelle / HOL, poprzez budowanie taktyk Isabelle / HOL w celu odzwierciedlenia reguł wnioskowania w śladach proofów SMT; patrz Szybka rekonstrukcja dowodu w stylu LCF dla Z3 autorstwa Böhmera i Webera na ITP 2010.

Najlepsze solwery ASP zostały opracowane w ciągu ostatnich kilku lat, aby stały się konkurencyjne w stosunku do solverów CP, SMT i SAT. Znam tylko niejasno szczegóły implementacji, które pozwoliły rozwiązaniom takim jak claspkonkurencja, więc nie mogę tak naprawdę porównać ich z SMT i CP, ale klamra wyraźnie reklamuje swoje skupienie się na nauce nogoods.

Przekraczanie tradycyjnych granic między tymi formalizmami przekłada się z bardziej abstrakcyjnych reprezentacji problemów na formalizmy o niższym poziomie, które można skutecznie wdrożyć. Kilka najlepszych solverów ASP i CP teraz jawnie tłumaczy swoje dane wejściowe na instancję SAT, która jest następnie rozwiązywana przy użyciu gotowego solvera SAT. W CP asystent modelowania ograniczeń Savile Row wykorzystuje techniki projektowania kompilatorów do tłumaczenia problemów wyrażonych w języku średnim Essence 'na formalizm niższego poziomu, odpowiedni do wprowadzania do solverów CP, takich jak Minion lub MiniZinc . Savile Row początkowo pracował z reprezentacją CP jako formalizmem niskiego poziomu, ale wprowadził SAT jako cel w wersji 1.6.2. Co więcej, esencja języka jeszcze wyższego poziomumoże być teraz automatycznie przetłumaczone na Essence ”za pomocą narzędzia Conjure . Jednocześnie niskopoziomowe solvery tylko SAT, takie jak Lingeling, są udoskonalane każdego roku, ostatnio poprzez naprzemienne uczenie się klauzul i etapy przetwarzania; zobacz krótki przegląd Co nowego w konkursach SAT i ASP autorstwa Heule i Schaub w AAAI 2015.

Analogia z historią języków programowania wydaje się zatem odpowiednia. SAT staje się rodzajem „kodu maszynowego”, ukierunkowanego na niskopoziomowy model eksploracji klauzul w strukturze klauzul. Abstrakcyjne paradygmaty stają się coraz bardziej podobne do języków komputerowych wyższego poziomu, z własnymi odrębnymi metodologiami i aplikacjami, do których są dobre. Wreszcie coraz bardziej gęsta kolekcja połączeń między tymi różnymi warstwami zaczyna przypominać ekosystem optymalizacji kompilatora.