It is well known that the problems of stochastic planning and probabilistic inference are closely related. This paper makes two contributions in this context. The first is to provide an analysis of the recently developed SOGBOFA heuristic planning algorithm that was shown to be effective for problems with large factored state and action spaces. It is shown that SOGBOFA can be seen as a specialized inference algorithm that computes its solutions through a combination of a symbolic variant of belief propagation and gradient ascent. The second contribution is a new solver for Marginal MAP (MMAP) inference. We introduce a new reduction from MMAP to maximum expected utility problems which are suitable for the symbolic computation in SOGBOFA. This yields a novel algebraic gradient-based solver (AGS) for MMAP. An experimental evaluation illustrates the potential of AGS in solving difficult MMAP problems.
more »
« less
QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
This paper presents and proves totally correct a new algorithm, called QSMA, for the satisfiability of a quantified formula modulo a complete theory and an initial assignment. The optimized variant of implemented in YicesQS is described and shown to preserve total correctness. A report on the performance of YicesQS at the 2022 SMT competition is included. YicesQS ran in the LIA, NIA, LRA, NRA, and BV categories and ranked second for the “largest contribution” award (single queries). It was the only solver to solve all LRA instances, where it was about two orders of magnitude faster than the second best solver (Z3).
more »
« less
- Award ID(s):
- 1816936
- PAR ID:
- 10487975
- Editor(s):
- Pientka, Brigitte; Tinelli, Cesare
- Publisher / Repository:
- Springer-Verlag
- Date Published:
- Journal Name:
- CADE 2023: Automated Deduction – CADE 29
- Volume:
- LNAI 14132
- ISBN:
- 978-3-031-38498-1
- Format(s):
- Medium: X
- Location:
- Roma, Italy
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Learning multiple tasks sequentially is important for the development of AI and lifelong learning systems. However, standard neural network architectures suffer from catastrophic forgetting which makes it difficult for them to learn a sequence of tasks. Several continual learning methods have been proposed to address the problem. In this paper, we propose a very different approach, called Parameter Generation and Model Adaptation (PGMA), to dealing with the problem. The proposed approach learns to build a model, called the solver, with two sets of parameters. The first set is shared by all tasks learned so far and the second set is dynamically generated to adapt the solver to suit each test example in order to classify it. Extensive experiments have been carried out to demonstrate the effectiveness of the proposed approach.more » « less
-
Abstract The Boltzmann Transport equation (BTE) was solved numerically in cylindrical coordinates and in time domain to simulate a Frequency Domain Thermo-Reflectance (FDTR) experiment. First, a parallel phonon BTE solver that accounts for all phonon modes, frequencies, and polarizations was developed and tested. The solver employs the finite-volume method (FVM) for discretization of physical space, and the finite-angle method (FAM) for discretization of angular space. The solution was advanced in time using explicit time marching. The simulations were carried out in time domain and band-based parallelization of the BTE solver was implemented. The phase lag between the temperature averaged over the probed region of the transducer and the modulated laser pump signal was extracted for a pump laser modulation frequency ranging from 20–200 MHz. It was found that with the relaxation time scales used in the present study, the computed phase lag is underpredicted when compared to experimental data, especially at smaller modulation frequencies. The challenges in solving the BTE for such applications are highlighted.more » « less
-
We discuss the efficient implementation of a high-performance second-order collocation-type finite-element scheme for solving the compressible Euler equations of gas dynamics on unstructured meshes. The solver is based on the convex-limiting technique introduced by Guermond et al. (SIAM J. Sci. Comput. 40, A3211–A3239, 2018). As such, it is invariant-domain preserving ; i.e., the solver maintains important physical invariants and is guaranteed to be stable without the use of ad hoc tuning parameters. This stability comes at the expense of a significantly more involved algorithmic structure that renders conventional high-performance discretizations challenging. We develop an algorithmic design that allows SIMD vectorization of the compute kernel, identify the main ingredients for a good node-level performance, and report excellent weak and strong scaling of a hybrid thread/MPI parallelization.more » « less
-
Octo-Tiger is a code for modeling three-dimensional self-gravitating astrophysical fluids. It was particularly designed for the study of dynamical mass transfer between interacting binary stars. Octo-Tiger is parallelized for distributed systems using the asynchronous many-task runtime system, the C++ standard library for parallelism and concurrency (HPX) and utilizes CUDA for its gravity solver. Recently, we have remodeled Octo-Tiger’s hydro solver to use a three-dimensional reconstruction scheme. In addition, we have ported the hydro solver to GPU using CUDA kernels. We present scaling results for the new hydro kernels on ORNL’s Summit machine using a Sedov-Taylor blast wave problem. We also compare Octo-Tiger’s new hydro scheme with its old hydro scheme, using a rotating star as a test problem.more » « less
An official website of the United States government

