System ASPMT2SMT:Computing ASPMT Theories by SMT Solvers

Michael Bartholomew, Joohyung Lee
6/12/2025
cs.AIcs.LO

No confident code implementation found for this paper.

Abstract

Answer Set Programming Modulo Theories (ASPMT) is an approach to combining answer set programming and satisfiability modulo theories based on the functional stable model semantics. It is shown that the tight fragment of ASPMT programs can be turned into SMT instances, thereby allowing SMT solvers to compute stable models of ASPMT programs. In this paper we present a compiler called {\sc aspsmt2smt}, which implements this translation. The system uses ASP grounder {\sc gringo} and SMT solver {\sc z3}. {\sc gringo} partially grounds input programs while leaving some variables to be processed by {\sc z3}. We demonstrate that the system can effectively handle real number computations for reasoning about continuous changes.

View on arXivView PDF

Code Implementations

No confident code match yet

We couldn't find an author-owned or strongly-evidenced community implementation for this paper. Any repos shown below are weak matches — verify before relying on them.

No code implementations found yet.

Know of an implementation? Let us know in the comments below!

Similar Papers

Answer Set Programming Modulo Theories and Reasoning about Continuous Changes

88% match2025

Finite Groundings for ASP with Functions: A Journey through Consistency

79% match2024

Continuous Optimization for Satisfiability Modulo Theories on Linear Real Arithmetic

79% match2026

Action Language BC+

77% match2025

Refining Gelfond Rationality Principle Towards More Comprehensive Foundational Principles for Answer Set Semantics

76% match2025

Satisfiability-Aided Language Models Using Declarative Prompting

76% match1 repo542026

Cite this paper

@article{bartholomew2025system,
  title  = {System ASPMT2SMT:Computing ASPMT Theories by SMT Solvers},
  author = {Michael Bartholomew and Joohyung Lee},
  year   = {2025},
  eprint = {2506.10708},
  archivePrefix = {arXiv},
  url    = {http://arxiv.org/abs/2506.10708v1}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/2506.10708.svg)](https://codeofpaper.com/paper/2506.10708)

Discussion