New Liftable Classes for First-Order Probabilistic Inference
Statistical relational models provide compact encodings of probabilistic dependencies in relational domains, but result in highly intractable graphical models. The goal of lifted inference is to carry out probabilistic inference without needing to reason about each individual separately, by instead treating exchangeable, undistinguished objects as a whole. In this paper, we study the domain recursion inference rule, which, despite its central role in early theoretical results on domain-lifted inference, has later been believed redundant. We show that this rule is more powerful than expected, and in fact significantly extends the range of models for which lifted inference runs in time polynomial in the number of individuals in the domain. This includes an open problem called S4, the symmetric transitivity model, and a first-order logic encoding of the birthday paradox. We further identify new classes S 2 FO 2 and S 2 RU of domain-liftable theories, which respectively subsume FO 2 and recursively unary theories, the largest classes of domain-liftable theories known so far, and show that using domain recursion can achieve exponential speedup even in theories that cannot fully be lifted with the existing set of inference rules.
The authors return to "domain-recursion" as a technique for lifted inference (that is, inference, focused on models that combine probabilities and logical construction, that avoids grounding the whole model). The technique is shown to tackle problems that have defied liftable inference so far. Also the authors characterise a new class of liftable models. Small scale tests show the gains from the technique (somewhat unsurprisingly, as we know that liftable inference, whenever applicable, may lead to exponential gains). 
The authors present a novel assessment of domain-recursion, and show that it can handle previously open problems. This is very interesting, and the paper is clear in its main goals and results. Overall the paper is an incremental effort in revisiting previous results and previous algorithms; the contribution is focused and narrow, but it can be quite valuable for other researchers interested in this topic. I should note that this is a difficult topic. The paper requires some polishing but still it contains a contribution.  Concerning the presentation, I find that the authors must add some comments on their assumptions. For instance, what exactly is the language they allow (I know that previous papers on this subject follow the same path, but still this is a something that must be fixed). I mean, is a formula an expression without quantifiers, and understood as universally quantified? But then what is a "theory in first-order logic" mentioned in page 2 (is it with quantifiers)? And then why is it that the birthday paradox uses an existential quantifier (and then the authors mention that it can be dealt with by Skolemization, but how? The exact way Skolemization is used should be shown). I find that the description of the language in Section 2 should be clear and leave no space for doubts. The authors must improve that aspect of the paper. Later, the same effort should be made to clarify FO^2 and its variants (do they accept quantifiers? where? how?).  Note for instance that if formulas are actually open formulas without quantifiers, then it is hard to imagine how they are interpreted for weighted first-order model count; I guess such a formula must be closed (but then, I suppose all formulas are implicitly closed with universal quantifiers?).   A relatively small point: I find Section 2.1 not to be very useful, the example with MLN is interesting but not needed here. Perhaps this can be shortened so that space is left for more important material.  A point about notation: it is funny that a PRV, say Q, appears as q in formula, while a logical variable, say x, appear capitalized as X; what is the logic concerning capitalization here?  There seems to be something wrong with the expression in the section about Shattering; the first expression has two quantifiers, but it should only have one (??).  It is a pity that S4-clauses and symmetric transitivities are not shown, however shortly, to be liftable. They are not in FO^2+, so the reader is left without any clue as to why they are liftable. Perhaps some space can be found to add some explanation on this matter.  I find the definition of FO^2+ to be harder to parse than necessary; please improve Definition 1.   One point I did not quite get: can one know the gains that will be obtained from domain-recursion BEFORE applying it? I mean, suppose we have a model and we cannot solve by other rules. We check and see that the model is NOT in FO^2+. Can we know whether domain-recursion will be useful, or not?   At the end of Section 6, the authors mention that costs are n^5 and n^2. How was that concluded? Just by empirical testing indicated in the graphs? But the gains should be derived from the algorithms that are used; if it is liftable against something exponential, the gains are exponential. I did not get the meaning of n^5 and n^2 there.  Concerning the text, here are some specific comments: - Page 1, line -4: the concept of domain-liftability may seem similar to data complexity, but actually lqe-liftability as defined by Van den Broeck and coauthors is more akin to data complexity; I don't think domain complexity has such a clear counterpart in the database world. - Is footnote 1 correct (perhaps conjoin X != Y)? - Right before Section 2.3: "process exponential in the number of individuals" is quite imprecise; this depends on the algorithm used to handle grounding, I suppose.  - Right before Section 6, the authors use "suggesting", but I suppose they mean "showing". - Footnote 3 misses an ending period. - Page 8: "straightforward" instead of "straight-forward". - Problems with capitalization in references: prolog, markov.