论文标题
基于SMT的加权模型集成与结构意识
SMT-based Weighted Model Integration with Structure Awareness
论文作者
论文摘要
加权模型集成（WMI）是一种流行的形式主义，旨在统一混合域的概率推断的方法，涉及逻辑和代数约束。尽管最近的工作大量工作，但允许WMI算法随着混合问题的复杂性而扩展仍然是一个挑战。在本文中，我们重点介绍了现有最新解决方案的一些实质性局限，并开发了一种算法，该算法将基于SMT的枚举（一种有效的正式验证技术）与问题结构的有效编码结合在一起。这使我们的算法避免生成冗余模型，从而获得大量的计算节省。对合成数据集和现实数据集进行了广泛的实验评估，这证实了该解决方案的优势比现有替代方案的优势。
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.
