skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.

Explore Research Products in the PAR
It may take a few hours for recently added research products to appear in PAR search results.


Title: Beyond NP: Quantifying over Answer Sets
Abstract Answer Set Programming (ASP) is a logic programming paradigm featuring a purely declarative language with comparatively high modeling capabilities. Indeed, ASP can model problems in NP in a compact and elegant way. However, modeling problems beyond NP with ASP is known to be complicated, on the one hand, and limited to problems in $$\[\Sigma _2^P\]$$ on the other. Inspired by the way Quantified Boolean Formulas extend SAT formulas to model problems beyond NP, we propose an extension of ASP that introduces quantifiers over stable models of programs. We name the new language ASP with Quantifiers (ASP(Q)). In the paper we identify computational properties of ASP(Q); we highlight its modeling capabilities by reporting natural encodings of several complex problems with applications in artificial intelligence and number theory; and we compare ASP(Q) with related languages. Arguably, ASP(Q) allows one to model problems in the Polynomial Hierarchy in a direct way, providing an elegant expansion of ASP beyond the class NP.  more » « less
Award ID(s):
1707371
PAR ID:
10169519
Author(s) / Creator(s):
; ;
Date Published:
Journal Name:
Theory and Practice of Logic Programming
Volume:
19
Issue:
5-6
ISSN:
1471-0684
Page Range / eLocation ID:
705 to 721
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. ; ; ; ; (, Theory and Practice of Logic Programming)
    Abstract We present a general approach to planning with incomplete information in Answer Set Programming (ASP). More precisely, we consider the problems of conformant and conditional planning with sensing actions and assumptions. We represent planning problems using a simple formalism where logic programs describe the transition function between states, the initial states and the goal states. For solving planning problems, we use Quantified Answer Set Programming (QASP), an extension of ASP with existential and universal quantifiers over atoms that is analogous to Quantified Boolean Formulas (QBFs). We define the language of quantified logic programs and use it to represent the solutions different variants of conformant and conditional planning. On the practical side, we present a translation-based QASP solver that converts quantified logic programs into QBFs and then executes a QBF solver, and we evaluate experimentally the approach on conformant and conditional planning benchmarks. 
    more » « less
  2. ; ; (, Logic Programming and Nonmonotonic Reasoning)
    Answer set programming (ASP) has long been used for modeling and solving hard search problems. Experience shows that the performance of ASP tools on different ASP encodings of the same problem may vary greatly from instance to instance and it is rarely the case that one encoding outperforms all others. We describe a system and its implementation that given a set of encodings and a training set of instances, builds performance models for the encodings, predicts the execution time of these encodings on new instances, and uses these predictions to select an encoding for solving. 
    more » « less
  3. ; ; (, Mathematics of Operations Research)
    This paper studies Positivstellensätze and moment problems for sets K that are given by universal quantifiers. Let Q be the closed set of universal quantifiers. Fix a finite nonnegative Borel measure whose support is Q and assume it satisfies the multivariate Carleman condition. First, we prove a Positivstellensatz with universal quantifiers: if a polynomial f is positive on K, then f belongs to the associated quadratic module, under the archimedeanness assumption. Second, we prove some necessary and sufficient conditions for a full (or truncated) multisequence to admit a representing measure supported in K. In particular, the classical flat extension theorem of Curto and Fialkow is generalized to truncated moment problems on such a set K. Third, we present applications of the above Positivstellensatz and moment problems in semi-infinite optimization, where feasible sets are given by infinitely many constraints with universal quantifiers. This results in a new hierarchy of Moment-SOS relaxations. Its convergence is shown under some usual assumptions. The quantifier set Q is allowed to be non-semialgebraic, which makes it possible to solve some optimization problems with non-semialgebraic constraints. Funding: X. Hu and J. Nie are partially supported by the NSF [Grant DMS-2110780]. I. Klep is supported by the Slovenian Research Agency program P1-0222 [also Grants J1-50002, J1-60011, J1-50001, J1-2453, N1-0217, and J1-3004] and was partially supported by the Marsden Fund Council of the Royal Society of New Zealand. I. Klep’s work was partly performed within the project COMPUTE, funded within the QuantERA II program that has received funding from the EU’s H2020 research and innovation program under the GA No 101017733. 
    more » « less
  4. ; ; (, Theory and Practice of Logic Programming)
    null (Ed.)
    Abstract In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining a formal proof showing that the answer sets of a given (non-ground) logic program P correctly correspond to the solutions to the problem encoded by P , regardless of the problem instance. To this aim, we use a formal specification language based on ASP modules, so that each module can be proved to capture some informal aspect of the problem in an isolated way. This specification language relies on a novel definition of (possibly nested, first order) program modules that may incorporate local hidden atoms at different levels. Then, verifying the logic program P amounts to prove some kind of equivalence between P and its modular specification. 
    more » « less
  5. ; (, IEEE Symposium on Foundations of Computer Science)
    null (Ed.)
    Consider the following two fundamental open problems in complexity theory: • Does a hard-on-average language in NP imply the existence of one-way functions? • Does a hard-on-average language in NP imply a hard-on-average problem in TFNP (i.e., the class of total NP search problem)? Our main result is that the answer to (at least) one of these questions is yes. Both one-way functions and problems in TFNP can be interpreted as promise-true distributional NP search problems—namely, distributional search problems where the sampler only samples true statements. As a direct corollary of the above result, we thus get that the existence of a hard-on-average distributional NP search problem implies a hard-on-average promise-true distributional NP search problem. In other words, It is no easier to find witnesses (a.k.a. proofs) for efficiently-sampled statements (theorems) that are guaranteed to be true. This result follows from a more general study of interactive puzzles—a generalization of average-case hardness in NP—and in particular, a novel round-collapse theorem for computationallysound protocols, analogous to Babai-Moran’s celebrated round-collapse theorem for informationtheoretically sound protocols. As another consequence of this treatment, we show that the existence of O(1)-round public-coin non-trivial arguments (i.e., argument systems that are not proofs) imply the existence of a hard-on-average problem in NP/poly. 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email