DPER: Dynamic Programming for Exist-Random Stochastic SAT

• URL: http://arxiv.org/abs/2205.09826v1
• Date: Thu, 19 May 2022 19:54:34 GMT
• Title: DPER: Dynamic Programming for Exist-Random Stochastic SAT
• Authors: Vu H. N. Phan and Moshe Y. Vardi
• Abstract summary: We present the exist-random satisfiability (ER-SSAT) problem, which combines the satisfiability (SAT) and weighted model counting (WMC) problems. We extend this WPMC framework to exactly solve ER-SSAT and implement a dynamic-programming solver named DPER.
• Score: 26.704502486686128
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In Bayesian inference, the maximum a posteriori (MAP) problem combines the most probable explanation (MPE) and marginalization (MAR) problems. The counterpart in propositional logic is the exist-random stochastic satisfiability (ER-SSAT) problem, which combines the satisfiability (SAT) and weighted model counting (WMC) problems. Both MAP and ER-SSAT have the form $\operatorname{argmax}_X \sum_Y f(X, Y)$, where $f$ is a real-valued function over disjoint sets $X$ and $Y$ of variables. These two optimization problems request a value assignment for the $X$ variables that maximizes the weighted sum of $f(X, Y)$ over all value assignments for the $Y$ variables. ER-SSAT has been shown to be a promising approach to formally verify fairness in supervised learning. Recently, dynamic programming on graded project-join trees has been proposed to solve weighted projected model counting (WPMC), a related problem that has the form $\sum_X \max_Y f(X, Y)$. We extend this WPMC framework to exactly solve ER-SSAT and implement a dynamic-programming solver named DPER. Our empirical evaluation indicates that DPER contributes to the portfolio of state-of-the-art ER-SSAT solvers (DC-SSAT and erSSAT) through competitive performance on low-width problem instances.

Related papers

• Sample-efficient Learning of Infinite-horizon Average-reward MDPs with General Function Approximation [53.17668583030862]
  We study infinite-horizon average-reward Markov decision processes (AMDPs) in the context of general function approximation. We propose a novel algorithmic framework named Local-fitted Optimization with OPtimism (LOOP) We show that LOOP achieves a sublinear $tildemathcalO(mathrmpoly(d, mathrmsp(V*)) sqrtTbeta )$ regret, where $d$ and $beta$ correspond to AGEC and log-covering number of the hypothesis class respectively
  arXiv  Detail & Related papers  (2024-04-19T06:24:22Z)
• Efficient Frameworks for Generalized Low-Rank Matrix Bandit Problems [61.85150061213987]
  We study the generalized low-rank matrix bandit problem, proposed in citelu2021low under the Generalized Linear Model (GLM) framework. To overcome the computational infeasibility and theoretical restrain of existing algorithms, we first propose the G-ESTT framework. We show that G-ESTT can achieve the $tildeO(sqrt(d_1+d_2)3/2Mr3/2T)$ bound of regret while G-ESTS can achineve the $tildeO
  arXiv  Detail & Related papers  (2024-01-14T14:14:19Z)
• Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
  We introduce the notion of decomposition hardness (d-hardness) We show that the d-hardness expresses an estimate of the hardness of $C$ w.r.t.
  arXiv  Detail & Related papers  (2023-12-16T12:44:36Z)
• Modeling Complex Mathematical Reasoning via Large Language Model based MathAgent [15.81048994298046]
  Large language models (LLMs) face challenges in solving complex mathematical problems. We propose a formal description of the mathematical solving and extend LLMs with an agent-based zero-shot framework. Experiments on miniF2F and MATH have demonstrated the effectiveness of PRER and proposed MathAgents.
  arXiv  Detail & Related papers  (2023-12-14T13:33:50Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  We propose a new satisfiability-aided language modeling (SatLM) approach for improving the reasoning capabilities of large language models (LLMs) We use an LLM to generate a declarative task specification rather than an imperative program and leverage an off-the-shelf automated theorem prover to derive the final answer. We evaluate SATLM on 8 different datasets and show that it consistently outperforms program-aided LMs in the imperative paradigm.
  arXiv  Detail & Related papers  (2023-05-16T17:55:51Z)
• Contextual Combinatorial Bandits with Probabilistically Triggered Arms [45.305256056479045]
  We study contextual bandits with probabilistically triggered arms (C$2$MAB-T) under a variety of smoothness conditions. Under the triggering modulated (TPM) condition, we devise the C$2$-UC-T algorithm and derive a regret bound $tildeO(dsqrtT)$.
  arXiv  Detail & Related papers  (2023-03-30T02:51:00Z)
• Multi-block-Single-probe Variance Reduced Estimator for Coupled Compositional Optimization [49.58290066287418]
  We propose a novel method named Multi-block-probe Variance Reduced (MSVR) to alleviate the complexity of compositional problems. Our results improve upon prior ones in several aspects, including the order of sample complexities and dependence on strongity.
  arXiv  Detail & Related papers  (2022-07-18T12:03:26Z)
• DPO: Dynamic-Programming Optimization on Hybrid Constraints [26.704502486686128]
  In Bayesian inference, the most probable explanation (MPE) problem requests a variable instantiation with the highest probability given some evidence. It is known that Boolean MPE can be solved via reduction to (weighted partial) MaxSAT. We build on DPMC and introduce DPO, a dynamic-programming that exactly solves MPE.
  arXiv  Detail & Related papers  (2022-05-17T21:18:54Z)
• Iterative Feature Matching: Toward Provable Domain Generalization with Logarithmic Environments [55.24895403089543]
  Domain generalization aims at performing well on unseen test environments with data from a limited number of training environments. We present a new algorithm based on performing iterative feature matching that is guaranteed with high probability to yield a predictor that generalizes after seeing only $O(logd_s)$ environments.
  arXiv  Detail & Related papers  (2021-06-18T04:39:19Z)
• Provably Efficient Model-Free Algorithm for MDPs with Peak Constraints [38.2783003051101]
  This paper considers the peak Constrained Markov Decision Process (PCMDP), where the agent chooses the policy to maximize total reward in the finite horizon as well as satisfy constraints at each epoch with probability 1. We propose a model-free algorithm that converts PCMDP problem to an unconstrained problem and a Q-learning based approach is applied.
  arXiv  Detail & Related papers  (2020-03-11T23:23:29Z)

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.