Was ist die Komplexität des Äquivalenzproblems für einmal gelesene Entscheidungsbäume?

11

Ein einmal gelesener Entscheidungsbaum ist wie folgt definiert:

  • und F a l s e sind einmal gelesene Entscheidungsbäume.TrueFalse
  • Wenn und B einmal gelesene Entscheidungsbäume sind und x eine Variable ist, die in A und B nicht vorkommt , dann ist ( x A ) ( ˉ xB ) auch ein einmal gelesener Entscheidungsbaum.ABxAB(xA)(x¯B)

Was ist die Komplexität des Äquivalenzproblems für einmal gelesene Entscheidungsbäume?

  • Input: Zwei schreib einmal Entscheidungsbäume und B .AB
  • Ausgabe: Ist ?AB

Motivation:

Dieses Problem trat auf, als ich das Problem der Beweisäquivalenz (Permutation von Regeln) eines Fragments der linearen Logik betrachtete.

Marc
quelle
Können Sie keine reduzierten binären Entscheidungsdiagramme verwenden? Edit: äh vielleicht nicht, deine Variablen sind nicht geordnet ...
Sylvain
@Kaveh Nein, es kommt in der Beweistheorie vor: Ich betrachte das Beweisäquivalenzproblem (Permutation von Regeln) eines Fragments der linearen Logik. Es läuft auf dieses boolesche Problem hinaus. Da ich kein Spezialist bin, dachte ich mir, ich würde fragen, ob dies jemals eine bekannte / einfache Frage war. Daher habe ich mir den Namen ausgedacht, weil ich es nicht besser weiß.
Marc
1
@Marc, es ist im Allgemeinen eine gute Idee zu erklären, warum Sie an einem Problem interessiert sind. Ich habe die Frage bearbeitet. Bitte schauen Sie, um sicherzustellen, dass es in Ordnung ist. (Entfernen Sie auch meine vorherigen Kommentare, da sie nicht mehr benötigt werden.)
Kaveh
@ Kaveh Ja, tut mir leid. Ich habe Ihre Neuformulierung bearbeitet, um sie meinem ursprünglichen Argument näher zu bringen (ich konnte nicht sofort herausfinden, ob Ihre in Ordnung war, daher schien es einfacher, dies zu tun)
Marc

Antworten:

5

Ich habe eine Teillösung gefunden. Das Problem ist in L.

Die Negation von ist äquivalent zu ( ˉ AB ) ( A ˉ B ), was F a l s e äquivalent ist, wenn sowohl ( ˉ AB ) als auch ( A ˉ B ) sind.AB(A¯B)(AB¯)False(A¯B)(AB¯)

Der einmal gelesene Entscheidungsbaum für kann aus dem einmal gelesenen Entscheidungsbaum für A durch Umschalten von T r u e und F a l s e in A erhalten werden . Dies kann im Protokollbereich erfolgen.A¯ATrueFalseA

Um zu überprüfen, ob gleich F a l s e ist (und ähnlich wie bei Aˉ B ), durchlaufen wir alle Paare von T r u e Blättern, eines von jedem Baum, und prüfen, ob sie kompatibel sind (das gibt es kein x auf einem der Pfade und ˉ x auf dem anderen). Es ist äquivalent zu F a l s e, wenn wir kein kompatibles Paar finden. Dies kann im Protokollbereich erfolgen.A¯BFalseAB¯Truexx¯False

Das Problem liegt also zumindest in L.


EDIT: Ich habe einige Ideen, um zu beweisen, dass dies L-vollständig ist, wahrscheinlich unter -Reduktion. Aber ich müsste die Details überprüfen und es passt nicht hierher. Ich werde einen Link zu dem Artikel posten, den ich schreibe, wenn alles klappt!AC0


EDIT2: da ist es, http://iml.univ-mrs.fr/~bagnol/drafts/mall_bdd.pdf

Das Problem ist also tatsächlich vollständig.

Marc
quelle
Wie kommst du zu dieser Negation? Die Negation von sollte ( ¯ x + ¯ A ) . ( X + ¯ B ) , das heißt x . ¯ A + ¯ x . ¯ B + ¯ A . ¯ Bx.A+x¯.B(x¯+A¯).(x+B¯)x.A¯+x¯.B¯+A¯.B¯
Denis
1
@Denis: Ich glaube das war ein Tippfehler, deine Formel vereinfacht sich zu , also wird die Negation tatsächlich berechnet, indem die 0 und 1 an den Blättern umgedreht werden. x.A¯+x¯.B¯
Nicolas Perrin
1
xx¯1L
1
Eine einfachere Möglichkeit, dies anzugeben, ist: Jeder Pfad ist ein Min- oder Max-Term, abhängig von der Beschriftung seines Blattes. Wir prüfen, ob sie die gleichen Mindestlaufzeiten haben. Wir können die Min-Terme im Protokollbereich aufzählen und prüfen, ob zwei Min-Terme identisch sind, im Protokollbereich.
Kaveh
2
NC1AC0AC0
2

ϕ

011{x,y¯,z}{x,y¯,z}{x,y,z}{x,z}y{x,y¯,z,t}{x,y,z}

{x1,,xn}ixi{x,xi,xj},{x,xj¯}{x,xi},{x,xi¯,xj¯}i<jxxixjji

P

Denis
quelle
1
x,y,zx,y¯,zx,y,z¯
Ah ja, das habe ich vergessen. Ich füge ein Update hinzu und hoffe, dass es jetzt funktioniert.
Denis
Vergessen Sie nicht, Ihre Million Dollar zu beanspruchen, wenn es funktioniert :)
Marc
L