The pywmi Framework and Toolbox for Probabilistic Inference using Weighted Model Integration

1 ModelingWMI Problems

In a nutshell, WMI [Belle et al., 2015] traces back to SAT, the problem of deciding if a Boolean formula is satisfiable. #SAT builds on SAT but answers the question of how many models satisfy a formula and WMC extends #SAT by allowing models to be weighted. Like SMT(LRA) extends SAT to answer satisfiability for logical formulas with linear inequalities over real variables, WMI extends WMC to integrate over (instead of summing) over the (possibily infinitely many) weighted models of an SMT(LRA) formula. A WMI problem consists of a support φ, an SMT(LRA) formula that describes all feasible worlds, a weight function w : Rr ×Bb ↦→ R that assigns a weight to every possible world and a set of queries, every query being an SMT(LRA) formula whose probability we want to compute. Worlds are value assignments to the problem variables. Internally, pywmi represents WMI problems as tuples 〈dom, φ,w,Q〉. The domain dom contains problem variables, their types and, optionally, the valid ranges for numeric variables (e.g., x ∈ [0, 1]). Both SMT(LRA) formulas (φ, q ∈ Q) and weight functions (w) are represented as Abstract Syntax Trees (ASTs) using the implementation provided by the PySMT library [Gario and Micheli, 2015].

∗ SK is supported by the Research Foundation-Flanders (FWO), this work has been partially supported by the ERC AdG 694980 and received funding from EU's Horizon 2020 programme under grant agreement No 823783.

The internal representation is exposed to developers and, for example, probabilistic programming languages can interface with it. For example, a language such as Problog [Dries et al., 2015] produces ground programs to be solved using WMC, an extension with continuous variables can solve ground programs using WMI instead. However, for endusers, pywmi also provides two modeling languages for WMI problems that can be directly parsed to the pywmi representation (see Figure 1 for an overview). Both formats can be used to compactly encode a WMI problem, differing in the syntax used for the expressions (inspired by MiniZinc [Nethercote et al., 2007] or SMT-LIB.v2 [Barrett et al., 2010]).

As an example, consider modelling a factory that produces banana and chocolate flavoured ice cream. Figure 2 shows a toy model of the factory production in the MiniZinc-inspired syntax. Variables b and c represent the amount of banana and

1 var float : b; % banana-flavoured ice cream 2 var float : c; % chocolate-flavoured ice cream 3 var bool : weekday; % weekday or weekend 4 5 par float : CAPACITY = 10.0; 6 7 % production is nonnegative 8 constraint (b >= 0) /\ (c >= 0); 9 10 % production cannot exceed the storage capacity 11 constraint (b + c < CAPACITY); 12 13 weight : (if weekday then 5/7 else 2/7) * 14 (if weekday 15 then (0.004 * b + 0.002 * c) 16 else (0.002 * b + 0.004 * c)) 17 18 % queries and evidence 19 constraint (not weekday); 20 query (b >= 2*c); 21 query (b >= 9.0) \/ (c > 9.0);

chocolate ice cream produced in a work day by the factory, while weekday is a Boolean variable distinguishing between weekdays and weekends. Intuitively, the production is determined by physical constraints, i.e., being non-negative and not exceeding the capacity of the factory, and market trends causing the preference over flavours to produce to be inverted in the weekends. In this toy example, the density functions combines the probability of weekday vs weekend and a linear combination of the amount of flavours produced, conditioned on weekday, that increases with the amount of ice cream produced. The WMI file can also contain evidence, e.g., conditioning on weekend days, and a list of queries to, for example, compute the probability that the banana ice cream production at least doubles the chocolate one (0.40), or the probability of having a particularly high production of any flavour (0.03).

2 Framework forWMI Solvers

Given a WMI problem in a standardized format, a WMI solver is employed to calculate weighted model integrals, most frequently, with the aim to compute query probabilities. The core interface for WMI solvers in pywmi consists of two methods: 1) computing a weighted model integral, given a domain, support and weight functions; and 2) computing the probability of a set of queries, given a domain, support, weight function and a set of queries. As computing the probabilities of a set of queries can be reduced to a set of weighted model integral computations, pywmi offers a default implementation. However, solvers that can only compute query probabilities or offer more efficient ways to compute query probabilities (e.g., using knowledge compilation [Kolb et al., 2018]), can override the default implementation.

The solving interface makes it possible to use any supported solver to solve any WMI problem in the common representation format. For users, pywmi offers a command-line interface to call or compare different solvers for a problem. Additionally, it can assist with converting file formats, installing new solvers or visualizing WMI problems. For developers, pywmi offers a growing amount of common functionality that might be useful to manipulating WMI problems or implementing a new solver, such as, easy-to-use data-structures for WMI problems and domains, wrappers around numeric integration software (e.g., Latte [De Loera et al., 2013]) and symbolic computation systems (e.g., PSI [Gehr et al., 2016]) that make it easy to write backend-agnostic solvers, and subroutines for computing with PySMT ASTs, linear inequalities, polynomials, sampling from WMI densities, evaluating points w.r.t. to their feasibility and density, etc.

3 ComparingWMI Solvers

As mentioned, pywmi allows the performance of different solvers to be compared. Aside from a common interface, however, pywmi also provides implementations for many state-of-the-art algorithms. These implementations either wrap around existing tools or libraries, or are (re-)implemented natively in pywmi. For solvers with external dependencies, pywmi tries to make the installation as easy as possible by automating installations or providing detailed instructions. The supported solvers are: WMI-PA [Morettin et al., 2019], XADD-based path-enumeration [Sanner et al., 2011] or bound-resolution (BR) algorithms [Kolb et al., 2018], symbolic SDD-based solver Symbo [Zuidberg Dos Martires et al., 2019], PRAiSE [De Salvo Braz et al., 2016] 1 . Additionally, pywmi includes a native implementation of XADDs and the BR algorithm, a fast approximate solver based on rejection-sampling and new WMI solvers are currently being developed using pywmi.

Using pywmi, we can now easily compare how different solvers behave on different problems. For example, we can compare how two state-of-the-art solvers (WMI-PA and BR) compare on some of the problems they introduce: highly structured xor and mutex problems with sparse inequalities (introduced alongside the BR solver), and synthetic WMI problems with random ASTs as support and weight function (using the WMI-PA problem generator). Running both solvers on these problems shows that the search-based WMIPA solver and its numeric integration software outperform the BR solver for the WMI problems with random ASTs, while the compilation-based BR solver better exploits the structure of the xor and mutex problems (Figure 3).

1 through the WMI-PA wrapper, without support for raw WMI computations - only query probabilities