First-Order Model Counting in a Nutshell

1 Why First-Order Model Counting?

Model counting comes in many flavors, depending on the form of logic being used. In propositional model counting, or #SAT, one counts the number of assignments ! that satisfy a propositional sentence ∆, denoted ! ♣= ∆ [Gomes et al., 2009]. In weighted model counting (WMC), one accords a weight to every model, and computes the sum of the weights of all models. The weight of a model is often factorized into weights of assignments to individual variables. The WMC formulation has recently emerged as an assembly language for probabilistic reasoning, offering a basic formalism for encoding various inference problems. State-of-the-art reasoning algorithms for Bayesian networks [Chavira and Darwiche, 2008], their relational extensions [Chavira et al., 2006], and factor graphs [Choi et al., 2013]. Exact WMC solvers are based on knowledge compilation [Darwiche, 2004; Muise et al., 2012] or exhaustive DPLL search [Sang et al., 2005]. (Approximate WMC algorithms use local search [Wei and Selman, 2005] or sampling [Chakraborty et al., 2014; Ermon et al., 2014].)

The popularity of WMC can be explained as follows. Its formulation elegantly decouples the logical or symbolic representation from the statistical or numeric representation, which is encapsulated in the weight function. This is a separation of concerns that is quite familiar in AI:

Factor Graph = Bipartite Graph + Potentials

Weighted model counting takes this to another level, where any logical language can now specify the qualitative structural properties of what constitutes a model. Independently, the weight function quantifies how probable each model is in the probability space.

Formally, we have the following.

Definition 1 (Weighted Model Count). The WMC of

• a sentence ∆ in propositional logic over literals L, and

One benefit of this approach is that it leverages decades of work on formal semantics and logical reasoning. When building solvers, this allows us to reason about logical equivalence and reuse solver technology (such as constraint propagation and clause learning). WMC also naturally reasons about deterministic, hard constraints in a probabilistic context.

First-Order Generalizations of Model Counting

The model counting philosophy has recently transformed several areas of uncertainty reasoning.

First-Order Logic Within statistical relational learning [Getoor and Taskar, 2007], lifted inference algorithms aim for efficient probabilistic inference in relational models [Poole, 2003], in particular for Markov logic networks (MLNs) [Richardson and Domingos, 2006]. Stateof-the art lifted inference algorithms reduce the problem to a weighted first-order model counting (WFOMC) problem, where the models (satisfying assignments) are defined by a sentence in finite-domain first-order logic [Van den Broeck et al., 2011; Gogate and Domingos, 2011].

WFOMC = First-Order Sentence + Weights A classical example is the first-order sentence

over a finite domain of n people. First-order model counting asks how many friendship and smokes relations exist that satisfy the formula. WFOMC additionally assigns a weight to each of these models to represent a distribution over them.

Logic Programs In the closely-related field of probabilistic programming, the goal is to augment programming languages with the ability to represent probability distributions. One prominent approach augments logic programming languages with probabilities. In their purest form, these representations express the distribution as the models of a logic program, with associated weights [Fierens et al., 2015].

Consider for example, the following inductive definition.

Smokes(x) : - Stress(y)▷ Smokes(x) : - Friends(x↪ y)↪ Smokes(y)▷

The program defines a set of models (in a higher-order logic). By assigning weights, for example to express the probability that people have stress and are friends, we can capture probabilistic spread of influence through a social network. This view of probabilistic programming has indeed spurred the development of probabilistic inference algorithms that use advanced logical reasoning techniques [Vlasselaer et al., 2015].

Databases Another form of first-order model counting can be found in the probabilistic database community [Suciu et al., 2011]. Here, the database query is a sentence in firstorder logic (usually a monotone DNF sentence, called UCQ). The goal is to compute the probability of the query given a database that assigns probabilities to tuples.

Within this field, the model counting perspective has shown to be fruitful, for identifying logical transformations that empower the probabilistic reasoning system. For example, firstorder resolution on the query can turn hard queries into easy ones [Gribkoff et al., 2014]. Moreover, efficient first-order solvers can significantly speed up querying of real-world knowledge graphs [Ceylan et al., 2016].

SMT One limitation of the WMC approaches above is that they operate on discrete distributions. This limitation is addressed in Belle et al.; Chistikov et al. [2015a; 2015]. The notion of weighted model integration (WMI) is based on satisfiability modulo theories (SMT), which enable us to, for example, reason about the satisfiability of linear constraints over the rationals (LRA). The WMI task is defined on the models of an SMT theory ∆, containing mixtures of Boolean and continuous variables.

For every assignment to the Boolean and continuous variables, the WMI problem defines a weight, for example as a polynomial density. The total WMI is computed by integrating these weights over the domain of solutions of ∆, which is a mixed discrete-continuous space. Consider, for example, the special case when ∆ has no Boolean variables, and the weight of every model is 1. Then, the WMI simplifies to computing the volume of the polytope encoded in ∆.

For example, the following SMT theory from Belle et al. [2015a] talks about travel times ji on various road segments, and how they relate to the time of day. Three Boolean features fi are defined. Their weight, together with a density on the continuous variables, defines a probability distribution.

Overall, weighted SMT theories admit a natural encoding of hybrid Markov and Bayesian networks, analogous to the encodings of discrete graphical networks using WMC.

Again, these encodings empower the probabilistic reasoning algorithms with the semantics and solvers for the logic at hand. For example, Belle et al. [2015b] use a highly efficient SMT solver to sample possible worlds from this distribution.

2 A First-Order Reasoning Tutorial

The give a flavor for the reasoning that is required in firstorder model counting, we will go through simple examples and identify the necessary principles. Algorithmic details can be found in Van den Broeck [2013]. For the sake of simplicity, the examples are non-weighted.

Exponentiation Consider ∆ to be

Assuming a finite domain D = ¶A♦, every assignment to Stress(A) and Smokes(A) satisfies ∆, except when Stress(A) is true and Smokes(A) is false. Therefore, the model count is 3. Now let ∆ be

Without changing D, the model count is still 3. When we expand D to n people, we get n independent copies of Formula 1. For each person x, Stress(x) and Smokes(x) can take 3 values, and the total model count is 3n .

This example already demonstrates the benefits of firstorder counting. A propositional model counter on Formula 2 would detect that all n clauses are independent, recompute for every clause that it has 3 models, and multiply these counts n times. Propositional model counters have no elementary operation for exponentiation. A first-order model counter reads from the first-order structure that it suffices to compute the model count of a single ground clause, and then knows to exponentiate. It never actually grounds the formula, and given the size of D, it runs in logarithmic time. This gives an exponential speedup over propositional counting, which runs in linear time.

These first-order counting techniques can interplay with propositional ones. Take for example ∆ to be

This sentence is about a specific individual who may be female, depending on the proposition Female. We can separately count the models in either case. When Female is false, ∆ is satisfied, and the ParentOf and MotherOf atoms can take any value. This gives 4n models. When Female is true, ∆ is structurally identical to Formula 2, and has 3n models. The total model count is then 3n + 4n .

These concepts can be applied recursively to count more complicated formulas. Take for example

8x↪ 8y↪ ParentOf(x↪ y) ^ Female(x) ) MotherOf(x↪ y)▷ There is now a partition of the ground clauses into n independent sets of n clauses, for values of x The formula for each specific x is structurally identical to Formula 3 and has count 3n + 4n . The total model count is then (3n + 4n )n .

Counting The most impressive improvements are attained when propositional model counters run in time exponential in n, yet first-order model counters run in polynomial time. To consider an example where this comes up, let ∆ be

8x↪ 8y↪ Smokes(x) ^ Friends(x↪ y) ) Smokes(y)▷ (4) This time, the clauses in the grounding of ∆ are no longer independent, and it would be wrong to exponentiate. Let us first assume we know that k people smoke, and that we know their identities. Then, howmany models are there? Formula 4 encodes that a smoker cannot be friends with a non-smoker. Hence, out of n2 Friends atoms, k(n - k) have to be false, and the others can take either truth value. Thus, the number of models is 2n2-k(n-k) . Second, we know that there are (nk) ways to choose k smokers, and k can range from 0 to n. This results in the total model count of Pnk=0 (nk)2n2-k(n-k) . Evaluating this formula is polynomial in n. On the other hand, propositional algorithms require time exponential in n.

Skolemization The theories so far had only universal quantifiers. Skolemization is the procedure of eliminating existential quantifiers from a theory. Van den Broeck et al. [2013] introduce a Skolemization procedure that is sound for the WFOMC task. Suppose that we are eliminating the existential quantifier in the following sentence.

We can do so without changing the model count. First, introduce a new relation S and replace the sentence by

Second, extend the weight function w with w(S(y)) = 1 and w(≻S(y)) = -1 for all y.

We can verify this transformation as follows. For a fixed position p, consider two cases: 9c↪ Card(p↪ c) is either true or false. If it is true, then so is S(p). All models of the Skolemized sentence are also models of the original sentence, and the models have the same weight. If 9c↪ Card(p↪ c) is false, then this does not correspond to any model of the original sentence. However, the Skolemized sentence is satisfied, and S(p) can be true or false. Yet, for every model with weight w where S(p) is true, there is also a model with weight -w where S(p) is false. These weights cancel out in the WFOMC, and the transformation is sound.

3 Why First-Order Model Counters?

Consider a randomly shuffled deck of 52 playing cards. Suppose that we are dealt the top card, and we want to answer: what is the probability that we get hearts? When the dealer reveals that the bottom card is black, how does our probability change? Basic statistics says it increases from 1◁4 to 13◁51.

To represent the distribution over all shuffled decks with a probabilistic graphical model, a natural choice is to have 52 random variables, one for every card. Each variable can take any of 52 values, one for every position in the deck. When the queen of hearts takes the top position, none of the other random variables are allowed to take that position. Such constraints are enforced by adding a factor between every pair of variables, setting the probability to zero that two cards are in the same position. Figure 1 depicts the graphical model for a small deck of 13 cards.

The graphical model for this problem is a completely connected. This means that classical inference algorithms will require time and space that is exponential in the number of playing cards. Indeed, for a full deck of cards, they will build a table with 5252 rows. The underlying reason for this poor performance is that the distribution has no conditional or contextual independencies. Our belief about the top card is affected by any new observation on the remaining cards. The reason why humans can still answer the above queries efficiently is different: the distribution exhibits exchangeability [Niepert and Van den Broeck, 2014]. In fact, Van den Broeck [2015] show that this distribution is intractable for any reasoning system that does not make the symmetries in this distribution explicit. More generally, Beame et al. [2015] study the complexity of first-order model counting.

The problem with this reasoning task is not one of representation. Many statistical relational languages, including Markov logic, can express the distribution concisely. It can even be written in classical first-order logic as

where Card(p↪ c) denotes that position p contains card c. Using first-order model counting, it can be solved efficiently as

This expression is evaluated in time polynomial in the number of cards n. It shows that lifted inference is strictly more powerful than propositional reasoning. The key difference is that WFOMC can assume certain symmetries that propositional techniques cannot take into account.

4 Conclusions

First-order model counting is an approach to probabilistic reasoning that has recenlty been applied to many representations of uncertainty, each time leading to highly efficient solvers. It presents a synthesis of ideas from various subfields of AI, for graphical models to knowledge representation and reasoning, and connects to fields outside of AI, in verification, databases, and theory.