Komplexität SMT mit einem Wechsel

Ich suche nach der Komplexität der Erfüllbarkeit einer Formel oder einer Formel wobei die Formel der Form ist: Wobei die Konstante in und die Domäne der Variablen auch . $\forall y_1, \dots,y_n, \exists x_1,\dots,x_m, \phi$ $\exists x_1,\dots,x_m \forall y_1, \dots,y_n,\phi$ $\phi$

ϕ := ϕ \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$

c

$c$

N

$\mathbb{N}$

x_{i}, y_{i}

$x_i,y_i$

N

$\mathbb{N}$

Tatsächlich sind die entweder oder . Vereinfacht das die Komplexität? $y_i$ $0$ $1$

Alle Antworten mit Referenzen würden gerne angenommen.

Vielen Dank

cc.complexity-theory reference-request lo.logic wece
quelle

Wenn phi boolesch war, befinden Sie sich in der zweiten Ebene der Polynomhierarchie, da ich das Problem durch eine nicht deterministische Turing-Maschine lösen kann, die einen SAT-Löser als Orakel verwendet. Würde hier nicht die gleiche Argumentation funktionieren?

Mikolas

Wie in der Frage angegeben, scheint es sogar unentscheidbar, da es Hilberts 10. Problem enthält en.wikipedia.org/wiki/Hilbert%27s_tenth_problem

Magnus Find

@MagnusFind Danke, du hast recht. Tatsächlich habe ich aber keine Multiplikation (bearbeitet, sorry).

Wece

@Mikolas mit zweiter Ebene meinst du oder ? In nicht wirklich vertraut mit Polynomhierarchie sorry.

Π_{2}

$\Pi_2$

Σ_{2}

$\Sigma_2$

Wece

Haben Sie andere freie Variablen als diese quantifizierten? Wenn ja, sollten Sie das auch klarstellen. Übrigens scheint eine einfache Beobachtung zu sein, dass dies für die dritte Ebene der Polynomhierarchie zumindest schwierig ist, selbst wenn Sie die quantifizierten Variablen als und annehmen .

0

$0$

1

$1$

Kaveh

Antworten:

Die Frage nach der Wahrheit in der Presburger Arithmetik mit begrenztem Quantifiziererwechsel wurde von Reddy und Loveland mit einiger Präzision beantwortet:

CR Reddy & DW Loveland: Presburger-Arithmetik mit Bounded Quantifier Alternation .

Das Papier kann hier gefunden werden (Entschuldigung für den hässlichen Link). Ihr Hauptergebnis wird wie folgt angegeben:

Die Mitgliedschaft in (wobei $\mathrm{PA}(m)$ $m$ $n$
$2^{d n^{m + 4}}$ $2^{dn^{m+4}}$ $2^{2^{e n^{m + 4}}}$ $2^{2^{en^{m+4}}}$ $d$ $e$

$m=2$

Cody
quelle

$m=1$ $n$

Sylvain
quelle

Ich kenne keine Referenzen für das quantifizierte Fragment, aber Ihr Problem ist nicht dasselbe wie die Entscheidung über gut untersuchte Fragmente der Presburger-Arithmetik, da Sie Einheitskoeffizienten haben.

$x + c < y$ $x$ $y$ $c$

Zwei einfache Theorien, deren Kombination schwierig ist. Pratt, 1977.

$x$ $y$

Festlegen von Trennungslogikformeln durch SAT und inkrementelle Eliminierung negativer Zyklen. Chao Wang, Franjo Ivančić, malaiischer Ganai, Aarti Gupta, 2005.

$0$ $1$ $-1$

Ein effizientes Entscheidungsverfahren für UTVPI-Einschränkungen. Shuvendu K. Lahiri und Madanlal Musuvathi, 2005.

$n$ $\mathcal{O}(3^n)$

Die abstrakte Oktaeder-Domäne. Robert Clarisó und Jordi Cortadella, 2004.

Für den Fall des begrenzten Quantifiziererwechsels kenne ich keine besseren Ergebnisse als die von Reddy und Loveland, aber vielleicht kann ein Experte Sie in die richtige Richtung weisen.

Vijay D.
quelle