SMT-based Weighted Model Integration with Structure Awareness

• URL: http://arxiv.org/abs/2206.13856v1
• Date: Tue, 28 Jun 2022 09:46:17 GMT
• Title: SMT-based Weighted Model Integration with Structure Awareness
• Authors: Giuseppe Spallitta, Gabriele Masina, Paolo Morettin, Andrea Passerini and Roberto Sebastiani
• Abstract summary: We 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.
• Score: 18.615397594541665
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• LLaMA-Berry: Pairwise Optimization for O1-like Olympiad-Level Mathematical Reasoning [56.273799410256075]
  The framework combines Monte Carlo Tree Search (MCTS) with iterative Self-Refine to optimize the reasoning path. The framework has been tested on general and advanced benchmarks, showing superior performance in terms of search efficiency and problem-solving capability.
  arXiv  Detail & Related papers  (2024-10-03T18:12:29Z)
• A unified consensus-based parallel ADMM algorithm for high-dimensional regression with combined regularizations [3.280169909938912]
  parallel alternating multipliers (ADMM) is widely recognized for its effectiveness in handling large-scale distributed datasets. The proposed algorithms serve to demonstrate the reliability, stability, and scalability of a financial example.
  arXiv  Detail & Related papers  (2023-11-21T03:30:38Z)
• Sample-Efficient Multi-Agent RL: An Optimization Perspective [103.35353196535544]
  We study multi-agent reinforcement learning (MARL) for the general-sum Markov Games (MGs) under the general function approximation. We introduce a novel complexity measure called the Multi-Agent Decoupling Coefficient (MADC) for general-sum MGs. We show that our algorithm provides comparable sublinear regret to the existing works.
  arXiv  Detail & Related papers  (2023-10-10T01:39:04Z)
• An Optimization-based Deep Equilibrium Model for Hyperspectral Image Deconvolution with Convergence Guarantees [71.57324258813675]
  We propose a novel methodology for addressing the hyperspectral image deconvolution problem. A new optimization problem is formulated, leveraging a learnable regularizer in the form of a neural network. The derived iterative solver is then expressed as a fixed-point calculation problem within the Deep Equilibrium framework.
  arXiv  Detail & Related papers  (2023-06-10T08:25:16Z)
• Doubly Stochastic Matrix Models for Estimation of Distribution Algorithms [2.28438857884398]
  We explore the use of Doubly Matrices (DSM) for matching and assignment nature permutation problems. Specifically, we adopt the framework of estimation of distribution algorithms and compare DSMs to some existing proposals for permutation problems. Preliminary experiments on instances of the quadratic assignment problem validate this line of research and show that DSMs may obtain very competitive results.
  arXiv  Detail & Related papers  (2023-04-05T14:36:48Z)
• Enhancing SMT-based Weighted Model Integration by Structure Awareness [10.812681884889697]
  Weighted Model Integration (WMI) emerged as a unifying formalism for probabilistic inference in hybrid domains. We develop an algorithm that combines SMT-based enumeration, an efficient technique in formal verification, with an effective encoding of the problem structure.
  arXiv  Detail & Related papers  (2023-02-13T08:55:12Z)
• The Dynamics of Riemannian Robbins-Monro Algorithms [101.29301565229265]
  We propose a family of Riemannian algorithms generalizing and extending the seminal approximation framework of Robbins and Monro. Compared to their Euclidean counterparts, Riemannian algorithms are much less understood due to lack of a global linear structure on the manifold. We provide a general template of almost sure convergence results that mirrors and extends the existing theory for Euclidean Robbins-Monro schemes.
  arXiv  Detail & Related papers  (2022-06-14T12:30:11Z)
• Efficient lifting of symmetry breaking constraints for complex combinatorial problems [9.156939957189502]
  This work extends the learning framework and implementation of a model-based approach for Answer Set Programming. In particular, we incorporate a new conflict analysis algorithm in the Inductive Logic Programming system ILASP.
  arXiv  Detail & Related papers  (2022-05-14T20:42:13Z)
• Efficient semidefinite-programming-based inference for binary and multi-class MRFs [83.09715052229782]
  We propose an efficient method for computing the partition function or MAP estimate in a pairwise MRF. We extend semidefinite relaxations from the typical binary MRF to the full multi-class setting, and develop a compact semidefinite relaxation that can again be solved efficiently using the solver.
  arXiv  Detail & Related papers  (2020-12-04T15:36:29Z)
• Efficient Consensus Model based on Proximal Gradient Method applied to Convolutional Sparse Problems [2.335152769484957]
  We derive and detail a theoretical analysis of an efficient consensus algorithm based on gradient proximal (PG) approach. The proposed algorithm is also applied to another particular convolutional problem for the anomaly detection task.
  arXiv  Detail & Related papers  (2020-11-19T20:52:48Z)
• Iterative Algorithm Induced Deep-Unfolding Neural Networks: Precoding Design for Multiuser MIMO Systems [59.804810122136345]
  We propose a framework for deep-unfolding, where a general form of iterative algorithm induced deep-unfolding neural network (IAIDNN) is developed. An efficient IAIDNN based on the structure of the classic weighted minimum mean-square error (WMMSE) iterative algorithm is developed. We show that the proposed IAIDNN efficiently achieves the performance of the iterative WMMSE algorithm with reduced computational complexity.
  arXiv  Detail & Related papers  (2020-06-15T02:57:57Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.