Какова сложность проблемы эквивалентности для деревьев решений с однократным чтением?

11

Дерево решений однократного чтения определяется следующим образом:

  • и F L сек е считываются однократно деревьев решений.TrueFalse
  • Если и B являются деревьями решений с однократным чтением, а x является переменной, не встречающейся в A и B , то ( x A ) ( ˉ xB ) также является деревом решений с однократным чтением.ABxAB(xA)(x¯B)

Какова сложность проблемы эквивалентности для деревьев решений с однократным чтением?

  • Входные данные : Два чтения один раз деревьев решений и B .AB
  • Выход: ?AB

Мотивация:

Эта проблема возникла, когда я смотрел на проблему доказательной эквивалентности (перестановки правил) фрагмента линейной логики.

Марк
источник
Разве вы не можете использовать сокращенные диаграммы бинарных решений? Изменить: возможно, нет, ваши переменные не упорядочены ...
Сильвен
@Kaveh Нет, это происходит в теории доказательств: я смотрю на проблему эквивалентности доказательств (перестановку правил) фрагмента линейной логики. Сводится к этой логической проблеме. Поскольку я не специалист, я решил, что когда-нибудь задам вопрос, если бы это был хорошо известный / простой вопрос. Следовательно, да, я придумал имя, потому что я не знаю ничего лучше.
Марк
1
@ Марк, как правило, хорошая идея объяснить, почему ты интересуешься проблемой. Я редактировал вопрос. Пожалуйста, посмотрите, чтобы убедиться, что все в порядке. (Также удаляю мои предыдущие комментарии, так как они больше не нужны.)
Kaveh
@Kaveh Да, прости за это. Я отредактировал вашу переформулировку, чтобы приблизить ее к моему первоначальному аргументу (я не мог сразу понять, если ваш был в порядке, поэтому казалось, что это легче сделать)
Марк

Ответы:

5

Я нашел частичное решение. Проблема в Л.

Отрицанием эквивалентна ( ° AB ) ( ˉ B ) , которая эквивалентна F L сек е тогда и только тогда как ( ··· AB ) и ( ˉ B ) есть.AB(A¯B)(AB¯)False(A¯B)(AB¯)

A¯ATrueFalseA

A¯BFalseAB¯Truexx¯False

Так что проблема как минимум в Л.


AC0


РЕДАКТИРОВАТЬ 2: там это, http://iml.univ-mrs.fr/~bagnol/drafts/mall_bdd.pdf

Таким образом, проблема действительно завершена в Logspace.

Марк
источник
x.A+x¯.B(x¯+A¯).(x+B¯)x.A¯+x¯.B¯+A¯.B¯
1
x.A¯+x¯.B¯
1
xx¯1L
1
Проще всего это сформулировать так: каждый путь является минимальным или максимальным в зависимости от метки своего листа. Мы проверяем, имеют ли они одинаковые минимальные условия. Мы можем перечислить min-термины в лог-пространстве и проверить, совпадают ли два min-термина в лог-пространстве.
Каве
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

Денис
источник
1
x,y,zx,y¯,zx,y,z¯
Ах да, забыл это, я добавляю исправление, надеясь, что это работает сейчас.
Денис
Не забывайте требовать свой миллион долларов, если он работает :)
Marc
L