Strange stuff in there though, transforming non-clausal forms to CNF is not linear and destroys the structure of the formula. Seems nonsense to me? All transforms to CNF I know are linear and keep the structure of the original formula. Often, it is even easier to understand why a DPLL solver works when reminding 'what it does' with respect to the original formula. (Usually it defaults to a pebbling game or resolution.)
After scanning the paper, they transform the formula to NNF, and DPLL the resulting CNF of the graph translation. It shouldn't matter, in a direct translation of a term to CNF, all the information is stored directly. At best, they end up with a slightly different search strategy on an expanded graph which 'shrinks' faster.
