[pfedak]

Unsurprisingly, there's nothing here. Most of the paper describes a brute force search across all possible variable assignments in the form of a graph (with some pointless polynomial improvements like making it a trie), where you build a path of vertices representing each set of truth values that satisfies a given expression. This clearly has exponential size, which the author alludes to in the "improvements" section by noting it does "redundant work". This is addressed by collapsing the exponential graph down to have only one vertex for each variable*expression pair (if you ignore the trie) and adding exponentially many labels for the different paths to reach a given vertex. (incidentally, to the extent that it's described clearly, it seems like the improved layered graph would basically be the same as the original non-layered graph)

The final complexity discussion uses the graph size constraint gained by the "improvement" but doesn't consider how to handle the extra labeling meaningfully. Basically, the pre- and post-improvement algorithms put the exponential work in different spots, and the sloppiness of the algorithm description (I mean, really, why tell us you're using a stack for BFS and then have "determine the subset of satisfied constraints" as a step) makes it easy to ignore.

I'm also being a little generous with the algorithm itself. As described, some of the trie optimizations seem to make certain combinations of satisfied expressions impossible to notice, but I think it's not a big deal to make this part work. The properties of the trie structure (and of sorting the variables by occurrence, for that matter) don't seem to be used.

[BrejlaCZ]

I haven't really understood how the proposed simplification should work... It's clearly exponential without it, but I am not sure about the supposed added labels. What should those be, conjunction and group subsets? Does that make them exponential?

The proofs and even explanations in this paper aren't very clear to me...

[tgflynn]

I'm stuck in the III.A "Main Idea" section where he says:

> Doing this enables us to represent each Di as a variable sequence, but with all the negative literals being removed. See Table I for illustration.

What justification does he have for throwing out negated variables ? If you do that the problem likely becomes trivial, but has nothing to do with the original problem.

[pfedak]

I had trouble with that too initially. I think that's actually fine: the representation the paper wants to use is that the variables in a path are the ones set to true, so omitting one means that variable must be false to satisfy the expression.

It does create issues with determining which expressions are satisfied, since two different paths can meet at a merged trie vertex higher up, which requires the extra bookkeeping that kills it.

[tgflynn]

Ah, OK thanks, that definitely could have been more clearly explained.