Jakie są ograniczenia rozumowania w ilościowej arytmetyki w SMT?

Question

Próbowałem kilka rozwiązują SMT (CVC3, CVC4 i Z3) na poniższym pozornie trywialny odniesienia:

(set-logic LIA) 
(set-info :smt-lib-version 2.0) 
(assert (forall ((x Int)) (forall ((y Int)) (= y x)))) 
(check-sat) 
(exit) 

W Solvers wszystkie powrócić nieznany. Rozumiem, że jest to nierozstrzygalny fragment (dobrze nieliniowy), ale spodziewałem się, że będzie kilka prostych heurystyk instancji, które mogą go rozwiązać. Próbowałem również dodawać pewne dodatkowe twierdzenia ze stałymi, ale to nie pomogło.

Czy istnieje sposób na zaatakowanie tych problemów i jakie są ograniczenia rozumowania w kwantyfikacji arytmetycznej w SMT?

Answer 1

Twój przykład przypada na kategorię LI (Linear Integer Aitmetic).

LIA, tj. Presburger Arithmetic, przyznaje eliminację kwantyfikatora (qe), chociaż złożoność czasowa procedur qe jest zbyt wysoka.

nie jestem pewien, że eliminacja CVC3 i CVC4 kwantyfikator wsparcie dla LIA, ale w Z3 można zrobić

(set-logic LIA) 
(set-info :smt-lib-version 2.0) 
(assert (forall ((x Int)) (forall ((y Int)) (= y x)))) 
(check-sat-using (then qe smt)) 

Od Rise4Fun execution, mam unsat wynik.

Tu taktyka qe jest etapem wstępnego przetwarzania przed zastosowaniem taktyki zakończenia gry smt.

Answer 2

Podkładka jest poprawna, preprocesor qe może być dość drogi. Co więcej, nie jest skuteczne we wzorach pochodzących z narzędzi sprawdzających oprogramowanie takie jak VCC, Poirot, Dafny, VeriFast, Why3 i ESCJava2. Nie jest to efektywne, ponieważ formuły tworzone przez te aplikacje zawierają również niezinterpretowane funkcje, tablice itp.

Jak sugeruje Pad, Z3 to zbiór silników. Udostępnia interfejsy API i polecenia, które pozwalają użytkownikom wybrać, który silnik (lub kombinacja silników) zostanie wykorzystany do rozwiązania problemu. Kiedy użytkownik po prostu mówi, że (check-sat) próbuje odgadnąć, jaki jest najlepszy silnik do rozwiązania formuły wejściowej. Zgadywanie opiera się na strukturze wzoru wejściowego i adnotacjach dostarczonych przez użytkownika (przykład: komenda set-logic). Ciągle rozszerzamy zbiór fragmentów, które są automatycznie wykrywane, oraz zestaw silników, które dostarczamy.

Jest to krępujące, że Z3 pominął fragment, taki jak LIA i nie zastosował do niego automatycznie procedury . Dla formuł LIA zwykle najlepsza jest opcja qe. Alternatywy oparte na dopasowaniu E lub MBQI nie są skuteczne, ponieważ są przeznaczone dla zupełnie innych fragmentów.

Po prostu committed code, który wykrywa LIA (nawet gdy nie jest używane set-logic). Zmiana jest już dostępna w gałęzi unstable (praca w toku). Będzie dostępna jutro w nocnych kompilacjach, aw następnym oficjalnym wydaniu.