pywmi

This is the pywmi package. It offers a unified and high-level API to a variety of weighted model integration solvers.

If you use the pywmi library in your own research please cite us as follows:

@inproceedings{kolb2019pywmi,
  title     = {The pywmi Framework and Toolbox for Probabilistic Inference using Weighted Model Integration},
  author    = {Kolb, Samuel and Morettin, Paolo  and Zuidberg Dos Martires, Pedro and Sommavilla, Francesco and Passerini, Andrea and Sebastiani, Roberto and De Raedt, Luc},
  booktitle = {Proceedings of the Twenty-Eighth International Joint Conference on
               Artificial Intelligence, {IJCAI-19}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},             
  pages     = {6530--6532},
  year      = {2019},
}

Installation

pip install pywmi

pywmi offers various services and engines that require additional installation steps. pywmi includes a helper utility pywmi-install to help installing components required by various engines. To see an overview of the solvers, the components they depend on and wether or not they are installed run:

pywmi-install --list

SMT solvers

pywmi relies upon pysmt to interface with SMT solvers. If you want to benefit from functionality relying on SMT solvers please install an SMT solver through the pysmt-install tool that comes as part of your pywmi installation.

pysmt-install --msat  # example to install mathsat, more solvers are available

PyXADD engine

pywmi includes a native Python implementation of XADDs (a sublibrary called pyxadd). The PyXaddEngine uses pyxadd to perform WMI inference. To use the PyXaddEngine, you need to install an SMT solver (see instructions above) and optionally the symbolic computation library PSI (see instructions below).

XADD engine

The XADD engine performs WMI using XADDs as described in Kolb et al., 2018. To use this engine you need Java, Gurobi and the xadd library JAR file. The pywmi-install tool that comes with your pywmi installation can automatically download and install the JAR file, however, you need to install Java and Gurobi manually. Once you did that, just call:

pywmi-install xadd
pywmi-install xadd --force  # To download a new version

Predicate abstraction engine

The predicate abstraction engine (short PA engine) uses MathSAT and Latte to solve WMI using predicate abstraction, as described in Morettin et al., 2017 and Morettin et al., 2019. In order to use the PA engine, you need to install the MathSAT SMT solver (see instructions above) and Latte (see instructions below).

MPWMI engine

The MPWMI engine performs WMI using the message-passing scheme described in Zeng et al., 2020. The solver works exclusively with problems having a dependency (aka primal) graph with treewidth 1 and per-literal weights, i.e.:

weight = Times(Ite(lit_1, wlit_1, Real(1)), ... , Ite(lit_k, wlit_k, Real(1)))

Installation

git clone https://github.com/UCLA-StarAI/mpwmi
pip install -e mpwmi/

PSI support

By default pywmi uses Sympy as a symbolic computer algebra backend. For an enhanced performance pywmi does also provide support to using the PSiPSI solver.

Installation

Make sure you have your Python virtual environment active.

You need to install the D language runtime -- PSI is written in D (https://dlang.org/).

On Mac you might need to install gnupg to verify the installation, e.g., through brew install gnupg -- be aware that this might install a lot of requirements. The alternative way to install the D runtime through brew install dmd is currently broken.
```
curl -fsS https://dlang.org/install.sh | bash -s dmd -p PATH/TO/WHERE/YOU/WANT/DLANG/
```

Now, make sure that the D runtime is in your path.

Either you use the follwong command

source PATH/TO/WHERE/YOU/WANT/DLANG/dmd-2.0**.*/activate

Or by adding the following lines to your .bashr file, for instance:

  #export PATH=$HOME/software/dlang/dmd-2.0**.*/linux/bin64:$PATH
  #export LD_LIBRARY_PATH=$HOME/software/dlang/dmd-2.0**.*/linux/lib64:$LD_LIBRARY_PATH

Next, you need to install Python bindings for PSI (make sure that you have activated your Python virtual environment).

cd pywmi/pywmi/weight_algebra/psi
python build_psi.py
python setup.py install --force

This will build python bindings to the symbolic inference engine of PSI, which can be used in in the backend.

Latte

The Latte integration backend as well as the predicate abstraction solver require Latte to be installed. You can find the latest releases on their GitHub releases page. You'll probably want the bundle: latte-integrale.

Summary

wget "https://github.com/latte-int/latte/releases/download/version_1_7_5/latte-integrale-1.7.5.tar.gz"
tar -xvzf latte-integrale-1.7.5.tar.gz
cd latte-integrale-1.7.5
./configure
make

Then, include the binaries folder to your PATH variable.

Usage

Calling pywmi

Setup density and query

import pysmt.shortcuts as smt

# Create a "domain" with boolean variables a and b and real variables x, y (both between 0 and 1)
domain = Domain.make(["a", "b"], ["x", "y"], [(0, 1), (0, 1)])

a, b = domain.get_bool_symbols()  # Get PySMT symbols for the boolean variables
x, y = domain.get_real_symbols()  # Get PySMT variables for the continuous variables

# Create support
support = (a | b) & (~a | ~b) & (x <= y) & domain.get_bounds()

# Create weight function (PySMT requires constants to be wrapped, e.g., smt.Real(0.2))
weight_function = smt.Ite(a, smt.Real(0.2), smt.Real(0.8)) * (smt.Ite(x <= 0.5, smt.Real(0.2), 0.2 + y) + smt.Real(0.1))

# Create query
query = x <= y / 2

Use engine to perform inference

# Create rejection-sampling based engine (no setup required)
rejection_engine = RejectionEngine(domain, support, weight_function, sample_count=100000)

print("Volume (Rejection):           ", rejection_engine.compute_volume())  # Compute the weighted model integral
print("Query probability (Rejection):", rejection_engine.compute_probability(query))  # Compute query probability

Use XADD engine (make sure you have installed the prerequisites)

# Create XADD engine (mode resolve refers to the integration algorithm described in
# Kolb et al. Efficient symbolic integration for probabilistic inference. IJCAI 2018)
# !! Requires XADD solver to be setup (see above) !!
xadd_engine = XaddEngine(domain, support, weight_function, mode="resolve")

print("Volume (XADD):                ", xadd_engine.compute_volume())  # Compute the weighted model integral
print("Query probability (XADD):     ", xadd_engine.compute_probability(query))  # Compute query probability

Generating uniform samples and their labels

from pywmi.sample import uniform
# n: Required number of samples
# domain, support: Domain and support defined as above
samples = uniform(domain, n)
labels = evaluate(samples, support, samples)

Generating weighted positive samples

from pywmi.sample import positive
# n: Required number of samples
# domain, support, weight: Defining the density as above
# Optional:
#   sample_pool_size: The number of uniformly sampled positive samples to weight and select the samples from
#   sample_count: The number of samples to draw initially, from which to build the positive pool
#   max_samples: The maximum number of uniformly sampled samples (positive or negative) to generate before failing
#                => If max_samples is exceeded a SamplingError will be raised
samples, positive_ratio = positive(n, domain, support, weight)

Handle densities and write to files

# Wrap support and weight function (and optionally queries) in a density object
density = Density(domain, support, weight_function, [query])

# Density object can be saved to and loaded from files
filename = "my_density.json"
density.to_file(filename)  # Save to file
density = Density.from_file(filename)  # Load from file

Work from command line

# Compare engines from command line
python -m pywmi my_density.json compare rej:n100000 xadd:mresolve  # Compute the weighted model integral
python -m pywmi my_density.json compare rej:n100000 xadd:mresolve -q 0  # Compute query probability (query at index 0)

# Compute volumes and probabilities from command line
# You can provide multiple engines and the result of the first engine not to fail will be returned
python -m pywmi my_density.json volume rej:n100000  # Compute weighted model integral
python -m pywmi my_density.json prob rej:n100000  # Compute all query probabilities

# Plot 2-D support
python -m pywmi my_density.json plot -o my_density.png

Find the complete running example in pywmi/tests/running_example.py

weighted-model-integration/pywmi