SMT-based Weighted Model Integration with Structure Awareness
This addresses scalability issues in probabilistic inference for hybrid domains, though it appears incremental as it builds on existing WMI and SMT techniques.
The paper tackled the challenge of scaling Weighted Model Integration (WMI) algorithms for probabilistic inference in hybrid domains by developing an SMT-based algorithm with structure-aware encoding. The result was substantial computational savings, confirmed through extensive evaluation on synthetic and real-world datasets.
Weighted Model Integration (WMI) is a popular formalism aimed at unifying approaches for probabilistic inference in hybrid domains, involving logical and algebraic constraints. Despite a considerable amount of recent work, allowing WMI algorithms to scale with the complexity of the hybrid problem is still a challenge. In this paper we highlight some substantial limitations of existing state-of-the-art solutions, and develop an algorithm that combines SMT-based enumeration, an efficient technique in formal verification, with an effective encoding of the problem structure. This allows our algorithm to avoid generating redundant models, resulting in substantial computational savings. An extensive experimental evaluation on both synthetic and real-world datasets confirms the advantage of the proposed solution over existing alternatives.