Qual é a complexidade do problema de equivalência para árvores de decisão de leitura única?

Uma árvore de decisão de leitura única é definida da seguinte maneira:

• $True$ e são árvores de decisão de leitura única.$False$
• Se e são árvores de decisão de leitura única e é uma variável que não ocorre em e , também é uma árvore de decisão leitura única.$A$$B$$x$$A$$B$$(x \land A) \lor (\bar x \land B)$

Qual é a complexidade do problema de equivalência para árvores de decisão de leitura única?

• Entrada: Dois leitura uma vez árvores de decisão e .$A$$B$
• Saída: ?$A \equiv B$

Motivação:

Esse problema surgiu enquanto eu examinava o problema da equivalência de prova (permutação de regras) de um fragmento da lógica linear.

Encontrei uma solução parcial. O problema está em L.

A negação de é equivalente a que é equivalente a se ambos e são.$A \leftrightarrow B$$(\bar A \land B) \lor (A \land \bar{B})$$False$$(\bar A \land B)$$(A \land \bar{B})$

A árvore de decisão leitura uma vez para pode ser obtido a partir da leitura uma vez árvore de decisão para , alternando e em . Isso pode ser feito no espaço de log.$\bar{A}$$A$$True$$False$$A$

Para verificar se é equivalente a (e da mesma forma para ), percorremos todos os pares de folhas , uma de cada árvore, e verificamos se elas são compatíveis ( ou seja, não há em um dos caminhos e no outro). É equivalente a se não encontrarmos um par compatível. Isso pode ser feito no espaço de log.$\bar A \land B$$False$${A} \land \bar{B}$$True$$x$$\bar x$$False$

Então o problema está pelo menos em L.

EDIT: Eu tenho algumas idéias para provar que isso é L-completo, provavelmente sob a redução . Mas eu precisaria verificar os detalhes e não caberá aqui. Vou postar um link para o artigo que estou escrevendo, se tudo der certo!$AC_0$

EDIT2: aqui está, http://iml.univ-mrs.fr/~bagnol/drafts/mall_bdd.pdf

Portanto, o problema é realmente completo no espaço de log.

Em uma fórmula ITE , é possível calcular polinomialmente uma lista de atribuições reduzida para descrever todas as avaliações, o que a torna verdadeira.$\phi$

Para fazer isso, basta olhar para sua fórmula como uma árvore com nós rotulados por variáveis ​​e folhas por e . Ramos esquerdos são a parte "then" que define a variável como true e ramos direitos são a parte "else" que define false. Cada ramificação que leva a uma licença será rotulada por um conjunto de atribuição de variáveis ​​parciais, por exemplo . Computar a lista de todos esses conjuntos de sua fórmula é polinomial. Você pode calcular uma forma normal dessa lista removendo um conjunto, se ele estiver contido em outro, e mesclando conjuntos que diferem em uma variável: se e estão na sua lista, você os remove e adiciona$0$$1$$1$$\{x,\overline{y},z\}$$\{x,\overline{y},z\}$$\{x,y,z\}$$\{x,z\}$, o que significa que ele funciona, independentemente do valor de . No entanto, se você tiver e , não poderá mesclá-los e mantê-los assim. Você aplica essas regras até estabilizar, mais uma vez esse procedimento é polinomial.$y$$\{x,\overline{y},z,t\}$$\{x,y,z\}$

Finalmente, escolha uma ordenação arbitrária de variáveis , e chamá- o peso de . O peso de uma lista é a soma de todos os pesos que aparecem em que (com multiplicites). Aplique "rotações" sempre que possível, para minimizar o peso total da sua forma normal. Uma rotação alterações a com ( é uma lista, e e também pode ser negada variáveis). Podemos ver que ele faz a diminuição do peso total em$\{x_1,\dots,x_n\}$$i$$x_i$$\{\vec x,x_i,x_j\},\{\vec x,\overline{x_j}\}$$\{\vec x,x_i\},\{\vec x,\overline{x_i},\overline{x_j}\}$$i<j$$\vec x$$x_i$$x_j$$j-i$. Espero que agora a forma normal seja única, tentarei uma prova formal mais tarde.

Então, duas fórmulas são equivalentes se tiverem a mesma lista de forma normal de atribuições. Então, o problema parece estar em .$P$