arXiv 1007.07882010-07-06cs.LO

A Geometric Presentation of Probabilistic Satisfiability

Guillermo Morales-Luna

英文摘要：

By considering probability distributions over the set of assignments the expected truth values assignment to propositional variables are extended through linear operators, and the expected truth values of the clauses at any given conjunctive form are also extended through linear maps. The probabilistic satisfiability problems are discussed in terms of the introduced linear extensions. The case of multiple truth values is also discussed.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL

We investigate the satisfiability and finite satisfiability problem for probabilistic computation-tree logic (PCTL) where operators are not restricted by any step bounds. We establish decidability for several fragments containing quantitative operators and pinpoint the difficulties arising in more complex fragments where the decidability remains open.

2018-06-29cs.LO

概率计算树逻辑的可满足性与有效性问题是高度不可判定的

The Satisfiability and Validity Problems for Probabilistic Computational Tree Logic are Highly Undecidable

本文证明了概率计算树逻辑（PCTL）的可满足性与有效性问题均高度不可判定，超出了算术层级，因此该逻辑不存在可靠且完备的演绎系统。

2025-04-30cs.LO

Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems with Applications to Probabilistic State Reachability and Region Stability

The stochastic Boolean satisfiability (SSAT) problem has been introduced by Papadimitriou in 1985 when adding a probabilistic model of uncertainty to propositional satisfiability through randomized quantification. SSAT has many applications, among them probabilistic bounded model checking (PBMC) of symbolically represented Markov decision processes. This article identifies a notion of Craig interpolant for the SSAT framework and develops an algorithm for computing such interpolants based on a resolution calculus for SSAT. As a potential application area of this novel concept of Craig interpola…

2012-06-25cs.LO

A Probabilistic Approach to Satisfiability of Propositional Logic Formulae

University of New Hampshire（新罕布什尔大学）

We propose a version of WalkSAT algorithm, named as BetaWalkSAT. This method uses probabilistic reasoning for biasing the starting state of the local search algorithm. Beta distribution is used to model the belief over boolean values of the literals. Our results suggest that, the proposed BetaWalkSAT algorithm can outperform other uninformed local search approaches for complex boolean satisfiability problems.

2019-12-04cs.AIcs.LO

A Simple Probabilistic Extension of Modal Mu-calculus

Probabilistic systems are an important theme in AI domain. As the specification language, the logic PCTL is now the default logic for reasoning about probabilistic properties. In this paper, we present a natural and succinct probabilistic extension of mu-calculus, another prominent logic in the concurrency theory. We study the relationship with PCTL. Interestingly, the expressiveness is highly orthogonal with PCTL. The proposed logic captures some useful properties which cannot be expressed in PCTL. We investigate the model checking and satisfiability problem, and show that the model checking …

2015-05-08cs.LO

The Complexity of Satisfiability in Non-Iterated and Iterated Probabilistic Logics

Let L be some extension of classical propositional logic. The non-iterated probabilistic logic over L, is the logic PL that is defined by adding non-nested probabilistic operators in the language of L. For example in PL we can express a statement like "the probability of truthfulness of A is at 0.3" where A is a formula of L. The iterated probabilistic logic over L is the logic PPL, where the probabilistic operators may be iterated (nested). For example, in PPL we can express a statement like "this coin is counterfeit with probability 0.6". In this paper we investigate the influence of probabi…

2019-02-10cs.CCcs.LO

更多相关论文收起更多论文

On the Hardness of PCTL Satisfiability

This paper shows that the satisfiability problem for probabilistic CTL (PCTL, for short) is undecidable. By a reduction from $1\frac{1}{2}$-player games with PCTL winning objectives, we establish that the PCTL satisfiability problem is $Σ_1^1$-hard. We present an exponential-time algorithm for the satisfiability of a bounded, negation-closed fragment of PCTL, and show that the satisfiability problem for this fragment is EXPTIME-hard.

2015-11-29cs.LO

用概率电路精确求解模计数可满足性问题

Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits

Department of Computer Science, Purdue University, IN, USA（计算机科学系，普渡大学）

本文提出KOCO-SMC，一种集成的精确模计数可满足性求解器，通过跟踪上下界和部分变量赋值实现早期估计，显著提升求解效率。

2025-06-17cs.AIcs.LO

基于可满足性模概率模型检查的约束鲁棒策略合成

Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking

Radboud University（拉德堡德大学）；Brno University of Technology（布尔诺理工大学）

针对有限MDP上带结构约束的鲁棒奖励最优策略计算难题，本文提出结合可满足性求解器与概率模型检查的合成框架，实验证明其可行且性能媲美现有最优方法。

2025-11-15cs.AIcs.LO

概率与因果可满足性：约束模型

Probabilistic and Causal Satisfiability: Constraining the Model

Saarland University（萨尔大学）；University of Lübeck（吕贝克大学）

本文研究概率与因果推理中的可满足性问题，通过固定结构因果模型的图结构并引入小模型约束这两个新维度扩展已有工作，刻画了不同算术、因果层级及紧凑边缘化设置下的复杂度。

2025-04-28cs.AIcs.CCcs.LO

A Specification Logic for Programs in the Probabilistic Guarded Command Language (Extended Version)

The semantics of probabilistic languages has been extensively studied, but specification languages for their properties have received little attention. This paper introduces the probabilistic dynamic logic pDL, a specification logic for programs in the probabilistic guarded command language (pGCL) of McIver and Morgan. The proposed logic pDL can express both first-order state properties and probabilistic reachability properties, addressing both the non-deterministic and probabilistic choice operators of pGCL. In order to precisely explain the meaning of specifications, we formally define the s…

2022-08-19cs.LO

From QBFs to MALL and back via focussing: fragments of multiplicative additive linear logic for each level of the polynomial hierarchy

In this work we investigate how to extract alternating time bounds from 'focussed' proof systems. Our main result is the obtention of fragments of MALLw (MALL with weakening) complete for each level of the polynomial hierarchy. In one direction we encode QBF satisfiability and in the other we encode focussed proof search, and we show that the composition of the two encodings preserves quantifier alternation, yielding the required result. By carefully composing with well-known embeddings of MALLw into MALL, we obtain a similar delineation of MALL formulas, again carving out fragments complete f…

2020-03-03cs.LO

Bayesian Statistical Model Checking for Multi-agent Systems using HyperPCTL*

Kansas State University（堪萨斯州立大学）

In this paper, we present a Bayesian method for statistical model checking (SMC) of probabilistic hyperproperties specified in the logic HyperPCTL* on discrete-time Markov chains (DTMCs). While SMC of HyperPCTL* using sequential probability ratio test (SPRT) has been explored before, we develop an alternative SMC algorithm based on Bayesian hypothesis testing. In comparison to PCTL*, verifying HyperPCTL* formulae is complex owing to their simultaneous interpretation on multiple paths of the DTMC. In addition, extending the bottom-up model-checking algorithm of the non-probabilistic setting is …

2022-09-06cs.AIcs.LOcs.MA

Approximate Counting in SMT and Value Estimation for Probabilistic Programs

Max Planck Institute for Software Systems (MPI-SWS)（马克斯·普朗克软件系统研究所）

#SMT, or model counting for logical theories, is a well-known hard problem that generalizes such tasks as counting the number of satisfying assignments to a Boolean formula and computing the volume of a polytope. In the realm of satisfiability modulo theories (SMT) there is a growing need for model counting solvers, coming from several application domains (quantitative information flow, static analysis of probabilistic programs). In this paper, we show a reduction from an approximate version of #SMT to SMT. We focus on the theories of integer arithmetic and linear real arithmetic. We propose m…

2015-10-29cs.AIcs.LO

针对SAT和SMT的不相交投影枚举

Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses

University of Trento（特伦托大学）；University of Freiburg（弗赖堡大学）

本文提出两种新型求解器，结合CDCL与时间顺序回溯，实现高效且不相交的枚举。通过改进的implicant shrinking算法减少部分赋值数量，提升搜索效率，并在投影枚举和SMT推理中表现优异。

2024-11-21cs.LO