W jaki sposób Z3 obsługuje arytmetyczną liczbę całkowitą nieliniową?

Question

Wiem, że teoria liczb całkowitych z mnożeniem jest generalnie nierozstrzygalna. Niemniej jednak w niektórych przypadkach Z3 zwraca model. Jestem ciekawa, jak to się robi. Czy ma to coś wspólnego z nową procedurą decyzyjną dotyczącą nieliniowej arytmetyki ponad realiami? Jakie specyficzne instancje (np. Liczba całkowita w skończonym module itd.) Zostały rozpoznane, dla których Z3 zwraca model zapytania mnożenia? Każda pomoc jest doceniana.

Answer 1

Tak, problem decyzyjny dla nieliniowej arytmetyki całkowitej jest nierozstrzygalny. Możemy zakodować problem zatrzymania dla maszyn Turinga w nieliniowej arytmetyce całkowitej. Gorąco polecam piękną książkę Hilbert's tenth problem dla każdego zainteresowanego tym problemem.

Należy pamiętać, że jeśli formuła ma rozwiązanie, zawsze możemy ją znaleźć za pomocą brutalnej siły. Oznacza to, że ciągle wyliczamy wszystkie możliwe przypisania i testujemy, czy spełniają one formułę, czy nie. Nie różni się to od próby rozwiązania problemu zatrzymania po prostu przez uruchomienie programu i sprawdzenie, czy kończy się po określonej liczbie kroków.

Z3 nie wykonuje naiwnego wyliczenia. Biorąc pod uwagę numer k, koduje on każdą liczbę całkowitą za pomocą bitów k i redukuje wszystko do logiki zdaniowej. Następnie, do znalezienia rozwiązania służy solver SAT. Jeśli zostanie znalezione rozwiązanie, przekształca je z powrotem w rozwiązanie integer dla oryginalnej formuły. Jeśli nie ma rozwiązania formalnego, to próbuje zwiększyć wartość k lub zmienić inną strategię. To ograniczenie do logiki zdaniowej jest w zasadzie procedurą szukania modelu/rozwiązania. Nie może pokazać, że problem nie ma rozwiązania. W rzeczywistości dla problemów, w których każda zmienna całkowita ma dolną i górną granicę, może to zrobić. Tak więc Z3 musi używać innych strategii, aby pokazać, że nie istnieje żadne rozwiązanie.

Co więcej, redukcja do logiki zdaniowej działa tylko wtedy, gdy istnieje bardzo małe rozwiązanie (rozwiązanie wymagające zakodowania niewielkiej liczby bitów). Omówię że w następnym poście:

• Need help understanding the equation

Z3 nie posiada dobre wsparcie dla nieliniowego arytmetyki liczb całkowitych. Opisane powyżej podejście jest bardzo uproszczone. Moim zdaniem, Mathematica wydaje się mieć najbardziej kompleksową gamę technik:

http://reference.wolfram.com/legacy/v5_2/functions/AdvancedDocumentationDiophantinePolynomialSystems

Wreszcie nieliniowa prawdziwy arytmetyka (NLSat) Solver nie jest używany domyślnie dla nieliniowych problemów całkowitych. Zwykle jest bardzo nieskuteczny w przypadku problemów z liczbą całkowitą. Mimo to możemy zmusić Z3 do używania NLSat nawet w przypadku problemów z liczbami całkowitymi. Po prostu trzeba wymienić:

(check-sat) 

Z

(check-sat-using qfnra-nlsat) 

Przy zastosowaniu tej komendy, Z3 rozwiąże problemu jako realnego problemu. Jeśli nie znajdziemy prawdziwego rozwiązania, wiemy, że nie ma rozwiązania całkowitego. Jeśli rozwiązanie zostanie znalezione, Z3 sprawdzi, czy rozwiązanie rzeczywiście przypisuje wartości całkowite do zmiennych całkowitych. Jeśli tak nie jest, zwróci unknown, aby wskazać, że nie udało się rozwiązać problemu.