Complexidade de uma alternância SMT

9

Eu estou olhando para a complexidade de satisfazibilidade de uma fórmula ou de uma fórmula x 1 , ... , x my 1 , ... , y n , ϕ onde ϕ é a fórmula da forma: ϕ : = ϕ ϕ | ¬ & Phi; | ϕy1,,yn,x1,,xm,ϕx1 1,...,xmy1 1,...,yn,ϕϕψ : = t > t | t = t t : = t + t | x i | e eu | c onde c é a constante em N , e o domínio de variáveis x i , y i também é N .

ϕ:=ϕϕ | ¬ϕ | ϕϕ | ψ
ψ:=t>t | t=t
t:=t+t | xi | yi | c
cNxi,yiN

Na verdade, a são ou 0 ou 1 . Isso simplifica a complexidade?yi01

Todas as respostas com referências serão aceitas com prazer.

obrigado

wece
fonte
Se phi era booleano, você está no segundo nível da hierarquia polinomial, porque eu posso resolver o problema por uma máquina de Turing não determinística, usando um solucionador SAT como um oráculo. O mesmo raciocínio não funcionaria aqui?
Mikolas
11
Como afirmado na questão parece ainda indecidível, já que inclui Hilberts 10 problema en.wikipedia.org/wiki/Hilbert%27s_tenth_problem
Magnus Encontrar
@MagnusFind Obrigado, você está certo. Mas, na verdade, não tenho a multiplicação (editada, desculpe).
wece
@ Mikolas por segundo nível, você quer dizer ou Σ 2 ? Em não realmente familiarizado com a hierarquia polinomial desculpe. Π2Σ2
wece
Você tem outras variáveis ​​livres além daquelas quantificadas? Nesse caso, você deve esclarecer isso também. Aliás, uma observação fácil parece ser que isso é pelo menos difícil para o terceiro nível da hierarquia polinomial, mesmo se você considerar as variáveis ​​quantificadas como e 1 . 01
Kaveh

Respostas:

6

A questão da verdade na aritmética de Presburger com alternância de quantificador limitado foi respondida com bastante precisão por Reddy e Loveland:

CR Reddy e DW Loveland: aritmética de pré -burger com alternância de quantificador limitado .

O documento pode ser encontrado aqui (desculpe pelo feio link). O principal resultado é apresentado da seguinte forma:

A adesão em (ondePA(m) é o número de quantificador alternâncias) de comprimento n pode ser decidido no espaço 2 d n m + 4 e no tempo (determinístico) 2 2 e n m + 4 onde d e e são constantes.mn

2dnm+4
22enm+4
de

Tomando , isso parece dar pelo menos um limite superior ao que você deseja, e eu suspeito que não esteja longe de ser apertado, pois você tem quase todas as fórmulas atômicas do Presburger "na raiz".m=2

cody
fonte
6

Uma única alternância em Presburger aritmética é suficiente para obter limites inferiores exponenciais, mais precisamente fórmulas como na pergunta com e n não são suficientes fixo ( GRADEL 1989 ).m=1n

Sylvain
fonte
5

Não conheço referências para o fragmento quantificado, mas seu problema não é o mesmo que decidir fragmentos bem estudados da aritmética de Presburger, porque você tem coeficientes de unidade.

x+c<yxyc

Duas teorias fáceis cuja combinação é difícil. Pratt, 1977.

xy

Decidir fórmulas de lógica de separação por SAT e eliminação do ciclo negativo incremental. Chao Wang, Franjo Ivančić, malaio Ganai, Aarti Gupta, 2005.

011

Um procedimento de decisão eficiente para restrições de UTVPI. Shuvendu K. Lahiri e Madanlal Musuvathi, 2005.

nO(3n)

O domínio abstrato do octaedro. Robert Clarisó e Jordi Cortadella, 2004.

Para o caso de alternância de quantificadores limitados, não conheço melhores resultados do que os de Reddy e Loveland, mas talvez um especialista possa apontá-lo na direção certa.

Vijay D
fonte