Faster lifting for two-variable logic using cell graphs
Timothy van Bremen, Ondřej Kuželka
Abstract
We consider the weighted first-order model counting (WFOMC) task, a problem with important applications to inference and learning in structured graphical models. Bringing together earlier work [Van den Broeck et al., 2011, 2014], a formal proof was given by Beame et al. [2015] showing that the two-variable fragment of first-order logic, FO^2, is domain-liftable, meaning it admits an algorithm for WFOMC whose runtime is polynomial in the given domain size. However, applying this theoretical upper bound is often impractical for real-world problem instances. We show how to adapt their proof into a fast algorithm for lifted inference in FO^2, using only off-the-shelf tools for knowledge compilation, and several careful optimizations involving the cell graph of the input sentence, a novel construct we define that encodes the interactions between the cells of the sentence. Experimental results show that, despite our approach being largely orthogonal to that of Forclift [Van den Broeck et al., 2011], our algorithm often outperforms it, scaling to larger domain sizes on more complex input sentences.
BibTeX
@InProceedings{pmlr-v161-bremen21a,
title = {Faster lifting for two-variable logic using cell graphs},
author = {van Bremen, Timothy and Ku\v{z}elka, Ond\v{r}ej},
booktitle = {Proceedings of the Thirty-Seventh Conference on Uncertainty in Artificial Intelligence},
pages = {1393--1402},
year = {2021},
editor = {de Campos, Cassio and Maathuis, Marloes H.},
volume = {161},
series = {Proceedings of Machine Learning Research},
month = {27--30 Jul},
publisher = {PMLR},
pdf = {https://proceedings.mlr.press/v161/bremen21a/bremen21a.pdf},
url = {https://proceedings.mlr.press/v161/bremen21a.html},
abstract = {We consider the weighted first-order model counting (WFOMC) task, a problem with important applications to inference and learning in structured graphical models. Bringing together earlier work [Van den Broeck et al., 2011, 2014], a formal proof was given by Beame et al. [2015] showing that the two-variable fragment of first-order logic, FO^2, is domain-liftable, meaning it admits an algorithm for WFOMC whose runtime is polynomial in the given domain size. However, applying this theoretical upper bound is often impractical for real-world problem instances. We show how to adapt their proof into a fast algorithm for lifted inference in FO^2, using only off-the-shelf tools for knowledge compilation, and several careful optimizations involving the cell graph of the input sentence, a novel construct we define that encodes the interactions between the cells of the sentence. Experimental results show that, despite our approach being largely orthogonal to that of Forclift [Van den Broeck et al., 2011], our algorithm often outperforms it, scaling to larger domain sizes on more complex input sentences.}
}