Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2611.09022

Optimal Probabilistic Answer Set Programming: Complexity and Implementations

Damiano Azzolini·Giuseppe Mazzotta·Francesco Ricca·Fabrizio Riguzzi
View original source ↗Read source document ↗Export metadata ↓

Abstract

Probabilistic Answer Set Programming (PASP) extends Answer Set Programming with the possibility of representing uncertain data. Among the possible available semantics, we focus here on the credal semantics. In this setting, prior work has focused exclusively on plain ASP programs, i.e., programs without optimization constructs. However, many real world tasks define optimality criteria over the possible solutions, which cannot be conveniently modeled with existing probabilistic ASP frameworks. In this paper, we close this gap and propose optimal Probabilistic Answer Set Programming, which extends PASP by also allowing weak constraints, which are the standard optimization construct of ASP. We define the semantics of such programs, study the computational complexity of the inference and most probable explanation tasks, and propose practical implementations based on Algebraic Model Counting and Answer Set Programming with Quantifiers. An empirical evaluation of the proposed approach on three real world tasks confirms the applicability of our framework.

Explore related subjects

cs.LOcs.AI

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Damiano Azzolini, Giuseppe Mazzotta, Francesco Ricca, Fabrizio Riguzzi. 2026-11-06. Optimal Probabilistic Answer Set Programming: Complexity and Implementations. https://arxiv.org/abs/2611.09022

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

The Yoneda embedding in simplicial type theory

Riehl and Shulman introduced simplicial type theory (STT), a variant of homotopy type theory which aimed to study not just homotopy theory, but its fusion with category theory: $(\infty,1)$-category theory. While notoriously technical, manipulating $\infty$-categories in simplicial type theory is often easier than working with ordinary categories, with the type theory handling infinite stacks of coherences in the background. We capitalize on recent work by Gratzer et al. defining the $(\infty,1)$-category of $\infty$-groupoids in STT to define presheaf categories within STT and systematically develop their theory. In particular, we construct the Yoneda embedding, prove the universal property of presheaf categories, refine the theory of adjunctions in STT, introduce the theory of Kan extensions, and prove Quillen's Theorem A.

cs.LO↗
arXiv2026

The Program Logic of Abstract Interpretation

Hoare-style program logics and abstract interpretation are two of the principal frameworks for reasoning about programs, and their affinity has long been recognised informally: both derive over-approximate judgements about program behaviour by structural, syntax-directed reasoning. Turning this analogy into a formal correspondence runs into two challenges. First, the disjunction (or join) rule, sound and admissible in Hoare logic, becomes unsound over non-additive abstract semantics. Second, the extrapolation operators that make abstract interpretation effective on unbounded computations, i.e. widening and narrowing, have no analogue in the derivations of existing program logics. We introduce APPL (Abstract Program Property Logic), a Hoare-style program logic that provides a proof-theoretic foundation for abstract interpretation while addressing both challenges. The key technical idea is density: abstract semantics is additive over dense families of logical assertions. This leads to a density-guarded join rule that enables sound disjunctive reasoning over arbitrary abstract domains. We also internalise the application of widening and narrowing through inference rules for iterative commands. As a result, an entire analysis by abstract interpretation can be viewed as a logical derivation in APPL. The logic is sound over any abstract domain and, when the assertion language is expressive enough, it is also relatively complete. Finally, by interpreting nondeterminism through a monoidal operator, APPL provides a single logical framework that uniformly subsumes Hoare logic, incorrectness logic, and Hoare-style logics for hyperproperties, thereby enabling their abstraction. Remarkably, the density-guarded join rule introduced to handle non-additive abstract semantics is also fundamental in guaranteeing completeness for hyperproperties.

cs.LO↗
arXiv2026

A Deeper Look at Depth: Stable Generation Accounting for Quantifier Reasoning

SMT solvers make automated verification convenient. At the same time, solvers suffer from instability, whereby seemingly inconsequential changes to the input may cause a previously quickly produced proof to fail or time out. This paper addresses a common cause of outcome instability (i.e., unsat/unknown fluctuations) in the context of program verification. We demonstrate that the generation (i.e., depth) accounting used to make quantifier instantiation practical and implemented in multiple state-of-the-art SMT solvers is non-confluent (i.e., prone to divergence), and that this leads to instability. We then address this deficiency and develop a new accounting method that is stable. The new method is justified using a sequence of refinements from an abstract, confluent solver model all the way to our implementation in Z3. Our empirical evaluation demonstrates that our implementation reduces outcome instability by 94% in the unstable core of the Mariposa benchmark without leading to performance regressions.

cs.LO↗