Faster Lifting for Ordered Domains with Predecessor Relations

TL;DR

This paper introduces a novel algorithm for lifted inference on ordered domains with predecessor relations, achieving significant speedups over previous methods, especially for immediate and second predecessor relations.

Contribution

The paper presents a new algorithm that natively supports predecessor relations in lifted inference, providing exponential speedups and improved practical performance.

Findings

Achieves up to tenfold speedup in inference tasks.

Handles general k-th predecessor relations efficiently.

Demonstrates effectiveness on lifted inference and combinatorics problems.

Abstract

We investigate lifted inference on ordered domains with predecessor relations, where the elements of the domain respect a total (cyclic) order, and every element has a distinct (clockwise) predecessor. Previous work has explored this problem through weighted first-order model counting (WFOMC), which computes the weighted sum of models for a given first-order logic sentence over a finite domain. In WFOMC, the order constraint is typically encoded by the linear order axiom introducing a binary predicate in the sentence to impose a linear ordering on the domain elements. The immediate and second predecessor relations are then encoded by the linear order predicate. Although WFOMC with the linear order axiom is theoretically tractable, existing algorithms struggle with practical applications, particularly when the predecessor relations are involved. In this paper, we treat predecessor relations as a native part of the axiom and devise a novel algorithm that inherently supports these relations. The proposed algorithm not only provides an exponential speedup for the immediate and second predecessor relations, which are known to be tractable, but also handles the general k-th predecessor relations. The extensive experiments on lifted inference tasks and combinatorics math problems demonstrate the efficiency of our algorithm, achieving speedups of a full order of magnitude.