Satysfakcja z ograniczeń otwartych lub interaktywnych

17

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ń.

sat lo.logic csp

— Dave Clarke
źródło

9

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.

— András Salamon
źródło

1

Ten papier z pewnością wygląda interesująco. Nigdy nie myślałem o rozwiązaniach SMT jako robieniu tego, czego wymagam. Z pewnością jest to droga do odkrycia.

— Dave Clarke

Jestem zaskoczony ostatnim komentarzem. Solwery SMT służą do logiki i teorii, a nie do konkretnych predykatów. Ludzie mogą wnieść nowe teorie i punkty odniesienia. Wiem, że programiści MathSAT badali AI i problemy z planowaniem.

— Vijay D

@Vijay D: masz rację, to zdanie jest nadmiernie stronnicze, a ja je poprawię. Skuteczne wdrożenie INJECTIVE jako teorii SMT zostało opublikowane w 2010 r. Przez Banković i Marić ( argo.matf.bg.ac.rs/publications/2010/alldiff-smt2010.pdf ).

— András Salamon,

7

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 .

— Giorgio Camerani
źródło

Jak powiązana / opłacalna jest książka The Calculus of Computation: Procedury decyzyjne z wnioskami o weryfikację autorstwa Aarona R. Bradleya i Zohara Manny? Wiem, gdzie jego kopia jest w odległości spaceru.

— Dave Clarke

@Dave: Oświadczenie: Moje osobiste doświadczenia z SMT są na samym początku ;-) Właśnie spojrzałem na spis treści tej książki; wydaje się, że istnieje duże skrzyżowanie tego z tym, które wskazałem. W tym drugim, to, co nazywacie tutaj funkcjami zewnętrznymi, nazywa się tam funkcjami niezinterpretowanymi i jest szeroko omówione. Nie udało mi się znaleźć niezinterpretowanych funkcji w spisie treści procedur decyzyjnych z wnioskami o weryfikację ; wydaje się jednak, że jest to bardzo dobra książka i może okazać się przydatna.

— Giorgio Camerani

@Dave: Obecnie czytam Procedury decyzyjne - algorytmiczny punkt widzenia . Nie dotarłem jeszcze do rozdziału o funkcjach niezinterpretowanych , ale jeśli się nie mylę, formuły z niezinterpretowanymi funkcjami są konwertowane na formuły w teorii równości. Jest tak, że teoria równości jest ujęta w Procedurach decyzyjnych wraz z wnioskami o weryfikację (rozdział 9).

— Giorgio Camerani

1

Myślę, że Amazon dzwoni.

— Dave Clarke

@Dave: OK, świetnie! ;-)

— Giorgio Camerani

7

$\mathbf P(x)$

— Evgenij Thorstensen
źródło

4

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.

— Vijay D.
źródło

0

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).

— Grzegorz Wierzowiecki
źródło