EZSMT Version 3, Matured

• URL: http://arxiv.org/abs/2607.13344v1
• Date: Wed, 15 Jul 2026 00:07:15 GMT
• Title: EZSMT Version 3, Matured
• Abstract summary: This paper presents the design and implementation of EZSMTV3, an SMT-based CASP framework that advances the translational approach to CASP solving.<n>Building upon the foundation of the EZSMT+ system, EZSMTV3 introduces a more expressive input language, supports optimization via weak constraints, and offers foundations for streamlined integration of new constraint types.<n>The paper provides benchmarking results comparing EZSMTV3 with its CASP peers such as CLINGCON, CLINGO[DL], and CLINGO[LP]
• Score: 2.4387391584956
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Constraint Answer Set Programming (CASP) is a hybrid reasoning paradigm that combines Answer Set Programming (ASP) with Constraint Processing and Satisfiability Modulo Theories (SMT), enabling powerful declarative encodings of complex combinatorial search problems. This paper presents the design and implementation of EZSMTV3, an extensible SMT-based CASP framework that advances the translational approach to CASP solving. Building upon the foundation of the EZSMT+ system, EZSMTV3 introduces a more expressive input language, supports optimization via weak constraints, and offers foundations for streamlined integration of new constraint types. Rather than implementing custom search procedures, EZSMTV3 leverages state-of-the-art SMT solvers, such as CVC5, YICES, and Z3 to perform reasoning. The paper provides benchmarking results comparing EZSMTV3 with its CASP peers such as CLINGCON, CLINGO[DL], and CLINGO[LP], while showcasing its ability to handle mixed-domain constraints involving both integers and reals. The system provides a robust platform for future extensions and theoretical exploration within the CASP domain.

Related papers

• When LLMs Develop Languages: Symbolic Communication for Efficient Multi-Agent Reasoning [85.36421257648294]
  Chain-of-Thought (CoT) improves large language models (LLMs) on difficult reasoning tasks.<n>We propose Communicative Language Symbolism Routing (R)<n>R treats each Language Symbolism Framework as a reusable symbolic protocol with compact symbols, usage rules, and a message-passing contract.<n>R reduces latency-oriented generated token completion by $3sim 6times$ compared to standard CoT.
  arXiv  Detail & Related papers  (2026-06-28T12:02:42Z)
• STAIF: A Stage-wise Optimization for Complex Instruction Following [50.48101504556211]
  STAIF is a stage-wise optimization framework that decouples the alignment of subjective (soft) constraints from the optimization of objectively verifiable (hard) constraints.<n>To support this method, we construct STAINSTRUCT, a high-quality bilingual (English, Chinese) dataset of approximately 31,000 complex multi-constraint instructions.
  arXiv  Detail & Related papers  (2026-06-26T06:14:07Z)
• ThinkBooster: A Unified Framework for Seamless Test-Time Scaling of LLM Reasoning [110.46431027868954]
  ThinkBooster is a framework for seamless test-time compute scaling of large language model (LLM) reasoning.<n>It consists of a modular Python library implementing state-of-the-art TTC scaling strategy and scorer families.<n>A deployable OpenAI-compatible proxy service enables drop-in integration of adaptive reasoning into real-world applications.
  arXiv  Detail & Related papers  (2026-06-05T05:28:46Z)
• Structured Prompt Optimization Meets Reinforcement Learning for Global and Local Interpretability over Complex Text [14.95562040863983]
  LLMs have advanced text classification, yet existing paradigms face a trade-off.<n>We introduce eXTC with three progressive stages: learning a SOP, reasoning distillation from a large teacher LLM into a compact LM, and expanding reasoning capabilities beyond the initial SOP.<n>This design enables (i) fast inference via a compact LM, with (ii) inference-time local reasoning traces, alongside a global, modular explanation of its learned domain rules, while (iii) significantly outperforming existing paradigms across diverse benchmarks in both classification performance and explanation quality, with stage-by-stage gains.
  arXiv  Detail & Related papers  (2026-05-27T20:29:41Z)
• Synthesizing Inductive Invariants for Distributed Protocols via IC3 and Large Language Models [10.962435384504301]
  We present IC3Syn, a neuro-symbolic framework that synthesizes inductive invariants by executing an IC3-style process over TLA+ states.<n>We evaluate IC3Syn on 29 distributed protocols spanning consensus, reconfiguration and client-server systems.
  arXiv  Detail & Related papers  (2026-05-23T15:06:15Z)
• SGA-MCTS: Decoupling Planning from Execution via Training-Free Atomic Experience Retrieval [74.1918709002557]
  We introduce textbfSGA-MCTS, a framework that casts LLM planning as non-parametric retrieval.<n>Online, a retrieval-augmented agent employs a hybrid symbolic-semantic mechanism to fetch relevant State-Goal-Action atoms.<n>By effectively amortizing the heavy computational cost of search, SGA-MCTS achieves System 2 reasoning depth at System 1 inference speeds, rendering autonomous planning both scalable and real-time feasible.
  arXiv  Detail & Related papers  (2026-04-16T07:22:36Z)
• Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
  We propose an end-to-end deep learning (DL) framework with low inference complexity for symbol-level precoding.<n>We show that the proposed framework captures substantial performance gains of optimal SLP, while achieving an approximately 80-times speedup over conventional methods.
  arXiv  Detail & Related papers  (2025-10-02T15:15:50Z)
• System ASPMT2SMT:Computing ASPMT Theories by SMT Solvers [3.677571687801579]
  ASPMT is an approach to combining answer set programming and satisfiability modulo theories.<n>It is shown that the tight fragment of ASPMT programs can be turned into SMT instances.<n>We demonstrate that the system can effectively handle real number computations for reasoning about continuous changes.
  arXiv  Detail & Related papers  (2025-06-12T13:59:15Z)
• Syzygy of Thoughts: Improving LLM CoT with the Minimal Free Resolution [59.39066657300045]
  Chain-of-Thought (CoT) prompting enhances the reasoning of large language models (LLMs) by decomposing problems into sequential steps.<n>We propose Syzygy of Thoughts (SoT)-a novel framework that extends CoT by introducing auxiliary, interrelated reasoning paths.<n>SoT captures deeper logical dependencies, enabling more robust and structured problem-solving.
  arXiv  Detail & Related papers  (2025-04-13T13:35:41Z)
• MCP-Solver: Integrating Language Models with Constraint Programming Systems [23.191983095692223]
  The MCP solver bridges Large Language Models with symbolic solvers through the Model Context Protocol (MCP), an open-source standard for AI system integration.<n>Our implementation offers interfaces for constraint programming (Minizinc), propositional satisfiability (PySAT), and SAT modulo Theories (Python Z3)<n>The system employs an editing approach with iterated validation to ensure model consistency during modifications and enable structured refinement.
  arXiv  Detail & Related papers  (2024-12-31T16:49:27Z)
• Semantic Probabilistic Layers for Neuro-Symbolic Learning [83.25785999205932]
  We design a predictive layer for structured-output prediction (SOP) It can be plugged into any neural network guaranteeing its predictions are consistent with a set of predefined symbolic constraints. Our Semantic Probabilistic Layer (SPL) can model intricate correlations, and hard constraints, over a structured output space.
  arXiv  Detail & Related papers  (2022-06-01T12:02:38Z)
• Constraint Answer Set Programming: Integrational and Translational (or SMT-based) Approaches [2.0559497209595814]
  Constraint answer set programming or CASP, for short, is a hybrid approach in automated reasoning. It puts together the advances of distinct research areas such as answer set programming, constraint processing, and satisfiability modulo theories. It opens new horizons for declarative programming applications such as solving complex train scheduling problems.
  arXiv  Detail & Related papers  (2021-07-17T14:58:57Z)

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.