Złożoność SMT z jedną alternatywą

Szukam złożoności spełniania formuły $\forall y_1, \dots,y_n, \exists x_1,\dots,x_m, \phi$ lub o wzorze $\exists x_1,\dots,x_m \forall y_1, \dots,y_n,\phi$ gdzie $\phi$ jest formuła formularza:

ϕ := ϕ \land ϕ | \neg ϕ | ϕ \to ϕ | ψ

$\phi:= \phi \wedge\phi ~| ~\neg \phi ~| ~ \phi\to \phi~| ~\psi$

ψ := t > t | t = t

$\psi := t>t~| ~t=t$

t := t + t | x_{i} | y_{i} | c

$t:= t+t~| ~x_i~|~y_i ~| ~c$ Gdzie

c

$c$ są stałe w

N

$\mathbb{N}$ oraz dziedzina zmiennych

x_{i}, y_{i}

$x_i,y_i$ jest również

N

$\mathbb{N}$ .

W rzeczywistości $y_i$ są albo $0$ lub $1$ . Czy to upraszcza złożoność?

Każda odpowiedź z referencjami byłaby chętnie przyjęta.

Dzięki

cc.complexity-theory reference-request lo.logic

— wece
źródło

Jeśli phi było logiczne, to jesteś na drugim poziomie wielomianowej hierarchii, ponieważ mogę rozwiązać problem za pomocą niedeterministycznej maszyny Turinga, używając solvera SAT jako wyroczni. Czy nie działałoby tu to samo rozumowanie?

— Mikolas

Jak stwierdzono w pytaniu, wydaje się nawet nierozstrzygalne, ponieważ obejmuje 10. problem Hilbertsa en.wikipedia.org/wiki/Hilbert%27s_tenth_problem

— Magnus Znajdź

@MagnusFind Dzięki, masz rację. Ale tak naprawdę nie mam mnożenia (edytowanego, przepraszam).

— wece

@Mikolas przez drugi poziom masz na myśli

Π_{2}

$\Pi_2$ lub

Σ_{2}

$\Sigma_2$ ? Przykro mi, ale nie bardzo znam hierarchię wielomianów.

— wece

Czy masz inne wolne zmienne inne niż te skwantyfikowane? Jeśli tak, powinieneś to również wyjaśnić. Przy okazji, łatwa obserwacja wydaje się być taka, że jest to co najmniej trudne dla trzeciego poziomu hierarchii wielomianowej, nawet jeśli weźmiesz zmienne kwantyfikowane za

0

$0$ i

1

$1$ .

— Kaveh

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:

Członkostwo w $\mathrm{PA}(m)$ (gdzie $m$ to liczba wariantów kwantyfikatora) o długości $n$ można zdecydować w przestrzeni kosmicznej
$2^{d n^{m + 4}}$ $2^{dn^{m+4}}$ oraz w (deterministycznym) czasie $2^{2^{e n^{m + 4}}}$ $2^{2^{en^{m+4}}}$ Gdzie $d$ i $e$ są stałymi.

Nabierający $m=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”.

— cody
źródło

Wystarczy jedna alternatywa w arytmetyce Presburger'a, aby uzyskać wykładnicze dolne granice, a dokładniej formuły, jak w pytaniu z $m=1$ i $n$ nie ustalone wystarczające ( Grädel 1989 ).

— Sylvain
ź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.

Dwie proste teorie, których kombinacja jest trudna. Pratt, 1977.

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.

Decydowanie o formułach logicznych separacji przez SAT i przyrostową eliminację cyklu ujemnego. Chao Wang, Franjo Ivančić, Malay Ganai, Aarti Gupta, 2005.

Obecnie twoje pytanie dopuszcza tylko współczynniki $0$ 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.

Skuteczna procedura decyzyjna w przypadku ograniczeń UTVPI. Shuvendu K. Lahiri i Madanlal Musuvathi, 2005.

Nadal jesteśmy w bardzo ograniczonym fragmencie. Rozszerzenie spójników $n$ -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ł daje $\mathcal{O}(3^n)$ procedura decydowania o spełnianiu takich ograniczeń. Zauważ, że wciąż znajdujemy się we fragmencie wolnym od kwantyfikatora.

Domena abstrakcyjna ośmiościanu. Robert Clarisó i Jordi Cortadella, 2004.

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.

— Vijay D.
źródło