Some people pointed me at E-graphs, a manner for representing and then heuristically minimizing terms. Of course, Boolean circuits are terms too and minimizing circuits is PSPACE. Very much so, even.
So, it's unclear how much minimization you can actually achieve with E-graphs.
It's worse, looks like one existential quantifier higher up than NP so PSPACE in old vernacular.
ReplyDelete