The novelty is relatively low since the compilation algorithm presented here is very similar to the compilation algorithm for AND/OR Multi-Valued Decision Diagrams (AOMDDs), which are a special case of PSDDs. Theorem 6 follows directly from the similar theorem that already holds for AOMDDs. The multiplication algorithm in section 3 is essentially the same as the one for SDDs, and it is no surprise that it operates in polytime. The main novelty and significance is in the experimental results, which suggest that PSDD compilation is more effective than AOMDD compilation. The paper would be more interesting if it gave a deeper analysis of where these advantages come from.

Real-world automated reasoning systems must contend with inconsistencies and the vast amount of information stored in relational databases.  In this paper, we introduce compilation techniques for inconsistency-tolerant reasoning over the combination of classical logic and a relational database.  Our resolution-based algorithms address a quantifier-free, function-free fragment of first-order logic while leveraging off-the-shelf database technology for all data-intensive computation.