Satysfakcja z ograniczeń otwartych lub interaktywnych

W przeszłości wdrażałem modele koordynacji, wykorzystując SAT i regularną satysfakcję z ograniczeń jako podstawowy koń roboczy w ich silnikach. Kontynuując tę ​​linię pracy, chciałbym uczynić modele bardziej interaktywnymi, a najlepszym sposobem, jaki to widzę, jest otwarcie solvera więzów, aby nie był już czarną skrzynką.

Dlatego chcę dowiedzieć się więcej na temat satysfakcji z ograniczeń, gdzie ograniczenia mają to, co nazywam zmiennymi zewnętrznymi , predykatami i funkcjami , tzn. Język ograniczeń może mieć predykaty, takie jak które mogą być tylko satysfakcjonujące, konsultując się z jakimś agentem spoza solwera, a dopiero wtedy, gdy jest uziemiony. Scenariusz, w którym jest to przydatne, występuje wtedy, gdy odpowiada procesowi decyzyjnemu z zewnątrz, którego nie można włączyć do solvera ograniczeń. Takie rozwiązania rozwiązywania problemów można nazwać otwartymi (ponieważ ograniczenia nie są całkowicie znane) lub interaktywnymi$\mathbf{P}(x)$$x$$\mathbf{P}$ (ponieważ wymagana jest interakcja, aby postępować z satysfakcją z ograniczeń).

Chciałbym wiedzieć oba:

• badania teoretyczne przeprowadzone w tym kierunku
• narzędzia lub biblioteki, które implementują solwery ograniczeń, które umożliwiają interakcję ze światem zewnętrznym podczas procesu rozwiązywania ograniczeń.

Nie do końca mnie przekonują poprzednie prace nad ograniczeniami otwartymi i interaktywnymi.

Próba przestudiowania pytań dotyczących wykonalności była:

• Martin J. Green i Christopher Jefferson, Structural Tractability of Propagated Constraints , CP 2008. doi: 10.1007 / 978-3-540-85958-1_25

chociaż ten dokument pozostawia kilka głównych pytań bez odpowiedzi. Podejście oparte na propagatorach w tym dokumencie jest ściśle powiązane z istniejącymi implementacjami solvera ograniczania.

Myślę, że praca nad SMT (teorie modulo satysfakcji) jest również ściśle związana z twoim pytaniem. Teorie SMT są często motywowane problemami z weryfikacją oprogramowania i sprzętu, ale istnieją teorie o smaku AI. Z niecierpliwością czekam na więcej aplikacji zbudowanych z SMT jako podstawową technologią i na więcej pracy z ograniczeniami, stosując pomysły z SMT.

Czytając twoje pytanie, zgadzam się również z twierdzeniem, że teorie modulo satysfakcji są ściśle związane z twoimi potrzebami. Proponuję przeczytać książkę Procedury decyzyjne - algorytmiczny punkt widzenia .

$\mathbf P(x)$

Jestem trochę zdezorientowany terminem „interaktywny”. Zajmę się innymi i dodam, że solver SMT może być pomocny. Aby dodać do komentarza Waltera Bishopa, dostępne są slajdy do książki Procedury decyzyjne (Kroening i Strichman). Interesujące może być również dokładne potraktowanie Johna Harrisona w Podręczniku praktycznej logiki i automatycznego rozumowania. Przykładowy kod jest dostępny online.

Księżniczka Filipa Ruemmera obsługuje arytmetykę z nieinterpretowanymi predykatami, które mogą pasować do tego, co masz na myśli przez słowo otwarte. Jest napisany w Scali, używa E-dopasowania w obsłudze kwantyfikacji i zapewnia interpolanty.

Co z narzędziami, jeśli zdecydujesz się na Prolog jako język wyboru, mogę zasugerować kilka metod wdrażania:

• GNU Prolog z biblioteką programowania C. Możesz wywoływać funkcje C z Prologa i Prolog z C. Otwiera to wiele możliwości rozszerzania funkcjonalności. Pro: Gnu Prolog jest jednym z najszybszych darmowych kompilatorów Prolog. Uwaga: niektóre osoby narzekają na brak wbudowanych predykatów ... właściwie większość z nich można zaimplementować, sprawdź warstwy zgodności Prolog @SO
• SWI-Prolog ma interesującą bibliotekę programowania, w tym komunikację sieciową, obsługę buforów protokołów itp. I jest dość popularny.
• XSB Prolog niektórzy twierdzą, że jest to najbardziej interesujący projekt pod względem interoperacyjności - w tym: interfejsy baz danych itp.

Prolog to język programowania, który jest odpowiedni do wykonywania wielu rodzajów solverów (a większość z nich ma swoje solvery o skończonej domenie).