Szukam złożoności spełniania formuły lub o wzorze gdzie jest formuła formularza:
Gdzie są stałe w oraz dziedzina zmiennych jest również .
W rzeczywistości są albo lub . Czy to upraszcza złożoność?
Każda odpowiedź z referencjami byłaby chętnie przyjęta.
Dzięki
Odpowiedzi:
Na pytanie o prawdę w Presburger Arithmetic z ograniczoną naprzemiennością kwantyfikatora Reddy i Loveland odpowiedzieli dość precyzyjnie:
CR Reddy i DW Loveland: Arytmetyka Presburgera z ograniczoną alternatywą kwantyfikatora .
Artykuł można znaleźć tutaj (przepraszam za brzydki link). Ich główny wynik jest następujący:
Nabierającym=2 , wydaje się, że daje to co najmniej górną granicę tego, czego chcesz, i podejrzewam, że nie jest to zbyt ścisłe, ponieważ masz prawie pełne formuły atomowe Presburger „u podstawy”.
źródło
Wystarczy jedna alternatywa w arytmetyce Presburger'a, aby uzyskać wykładnicze dolne granice, a dokładniej formuły, jak w pytaniu zm=1 i n nie ustalone wystarczające ( Grädel 1989 ).
źródło
Nie znam referencji dla skwantyfikowanego fragmentu, ale twój problem nie jest taki sam, jak decydowanie o dobrze zbadanych fragmentach arytmetyki Presburger, ponieważ masz współczynniki jednostkowe.
Poniższy artykuł Pratta analizuje przypadek, w którym ograniczenia mają formęx+c<y , gdzie x i y są zmiennymi i c w liczbie naturalnej. Pokazuje, że problem decydowania o tym, czy połączenie takich ograniczeń można skutecznie wykonać za pomocą algorytmu grafowego.
Ten fragment jest również nazywany logiką różnic i przez krótki czas był niestety nazywany logiką separacji (ponieważx i y są oddzielone stałą). Poniższy artykuł przedstawia praktyczny pogląd na rozwiązanie fragmentu problemu bez kwantyfikatora.
Obecnie twoje pytanie dopuszcza tylko współczynniki0 i 1 . Jeśli również pozwolisz−1 jako współczynnik, otrzymane sprzężenia ograniczeń nazywane są w literaturze analizy programowej ośmiokątami . Koniunkcje i rozłączenia ograniczeń są logiką Zmiennych drugiej jednostki na nierówność (UTVPI) . Wprowadzenie następujących papierowych algorytmów ankietowych do decydowania o spełnianiu sprzężeń ograniczeń UTVPI bez kwantyfikatora.
Nadal jesteśmy w bardzo ograniczonym fragmencie. Rozszerzenie spójnikówn -zmienne liniowe nierówności o współczynnikach jednostkowych nazywane są ośmiościanem . Jest to tak naturalne rozszerzenie, że spodziewałbym się, że zostało to przestudiowane w literaturze poświęconej programowaniu matematycznemu i optymalizacji, ale ja nie znam tej literatury. Poniższy artykuł dajeO(3n) procedura decydowania o spełnianiu takich ograniczeń. Zauważ, że wciąż znajdujemy się we fragmencie wolnym od kwantyfikatora.
W przypadku ograniczonej alternatywy kwantyfikatora nie znam lepszych wyników niż Reddy i Loveland, ale być może ekspert może wskazać właściwy kierunek.
źródło