[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.