Czy możesz zdecydować o równoważności monotonicznych wyrażeń boolowskich, które nie zawierają negacji w PTIME?

Czy następujący problem występuje w trybie PTIME lub coNP-hard:

Biorąc pod uwagę dwa wyrażenia logiczne i w zmiennych$e_1$$e_2$ , bez negacji (tzn. Wyrażenia są w całości budowane przez ∧ i ∨ ). Zdecyduj, czy e 1 ≡ e 2 , czyli mają taką samą wartość dla wszystkich przypisań do zmiennych.$x_1,\dots,x_n$$\wedge$$\vee$$e_1 \equiv e_2$

Jeśli oba wyrażenia byłyby podane w DNF, to problem występuje w PTIME, ponieważ moglibyśmy najpierw leksykograficznie uporządkować zdania spójne i porównać. Ale wprowadzenie arbitralnego wyrażenia do DNF może wybuchnąć wykładniczo. Podobny argument wydaje się dotyczyć diagramów decyzji binarnych.

Oczywiście problem dotyczy coNP.

Szukałem w Google w sporej ilości, ale nie mogłem znaleźć żadnej odpowiedzi.

Przepraszamy za podstawowe pytanie.

Wniosek 3.5 w [BHR84] pokazuje, że problem jest coNP-zupełny.

[BHR84] PA Bloniarz, HB Hunt, III i DJ Rosenkrantz. Struktury algebraiczne z trudnymi zagadnieniami równoważności i minimalizacji. Journal of the ACM , 31 (4): 879-904, październik 1984. http://dx.doi.org/10.1145/1634.1639