Buchumschlag

Beyond Eager Encodings: A Theory-Agnostic Approach to Theory-Lemma Enumeration in SMT

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Civini, Emanuele, Masina, Gabriele, Spallitta, Giuseppe, Sebastiani, Roberto
Format:	Preprint
Veröffentlicht:	2026
Schlagworte:	Logic in Computer Science
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

On CNF Conversion for SAT and SMT Enumeration
von: Masina, Gabriele, et al.
Veröffentlicht: (2023)

Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses
von: Spallitta, Giuseppe, et al.
Veröffentlicht: (2024)

Canonical Decision Diagrams Modulo Theories
von: Michelutti, Massimo, et al.
Veröffentlicht: (2024)

Exploiting Partial-Assignment Enumeration in Optimization Modulo Theories
von: Masina, Gabriele, et al.
Veröffentlicht: (2025)

Disjoint Partial Enumeration without Blocking Clauses
von: Spallitta, Giuseppe, et al.
Veröffentlicht: (2023)

Extending CDCL-based Model Enumeration with Weights
von: Spallitta, Giuseppe, et al.
Veröffentlicht: (2026)

Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration
von: Sebastiani, Roberto
Veröffentlicht: (2025)

Computing Short SAT Implicants via Ising/QUBO Encodings
von: Spallitta, Giuseppe, et al.
Veröffentlicht: (2026)

On Enumerating Short Projected Models
von: Möhle, Sibylle, et al.
Veröffentlicht: (2021)

An SMT Theory for n-Indexed Sequences
von: Hara, Hichem Rami Ait El, et al.
Veröffentlicht: (2024)

An SMT-LIB Theory of Finite Fields
von: Hader, Thomas, et al.
Veröffentlicht: (2024)

On SMT Theory Design: The Case of Sequences
von: Hara, Hichem Rami Ait El, et al.
Veröffentlicht: (2024)

Enhancing SMT-based Weighted Model Integration by Structure Awareness
von: Spallitta, Giuseppe, et al.
Veröffentlicht: (2023)

A Relational Theory of Grounding and a new Grounder for SMT
von: Carbonnelle, Pierre
Veröffentlicht: (2026)

System ASPMT2SMT:Computing ASPMT Theories by SMT Solvers
von: Bartholomew, Michael, et al.
Veröffentlicht: (2025)

An Encoding for CLP Problems in SMT-LIB
von: Amrollahi, Daneshvar, et al.
Veröffentlicht: (2024)

A Naive Encoding of Russell's Paradox in Type Theory
von: Qu, Zhuoyuan
Veröffentlicht: (2025)

A Beluga Formalization of the Harmony Lemma in the $π$-Calculus
von: Cecilia, Gabriele, et al.
Veröffentlicht: (2024)

Lean-SMT: An SMT tactic for discharging proof goals in Lean
von: Mohamed, Abdalrhman, et al.
Veröffentlicht: (2025)

Realizability in Semantics-Guided Synthesis Done Eagerly
von: Meyer, Roland, et al.
Veröffentlicht: (2024)

Approximate SMT Counting Beyond Discrete Domains
von: Shaw, Arijit, et al.
Veröffentlicht: (2025)

Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols
von: Hozzová, Petra, et al.
Veröffentlicht: (2025)

LLM2SMT: Building an SMT Solver with Zero Human-Written Code
von: Janota, Mikoláš, et al.
Veröffentlicht: (2026)

Typed Non-determinism in Concurrent Calculi: The Eager Way
von: Heuvel, Bas van den, et al.
Veröffentlicht: (2024)

SMT-Layout: A MaxSMT-based Approach Supporting Real-time Interaction of Real-world GUI Layout
von: Li, Bohan, et al.
Veröffentlicht: (2024)

Hint-Based SMT Proof Reconstruction
von: Clune, Joshua, et al.
Veröffentlicht: (2026)

Efficient Volume Computation for SMT Formulas
von: Shaw, Arijit, et al.
Veröffentlicht: (2025)

Number theory combination: natural density and SMT
von: Toledo, Guilherme V., et al.
Veröffentlicht: (2025)

Integer Reasoning Modulo Different Constants in SMT
von: Pertseva, Elizaveta, et al.
Veröffentlicht: (2025)

Invariant Checking for SMT-based Systems with Quantifiers
von: Redondi, Gianluca, et al.
Veröffentlicht: (2024)

SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology
von: Huvar, Ondřej, et al.
Veröffentlicht: (2026)

Towards Learning Infinite SMT Models (Work in Progress)
von: Janota, Mikoláš, et al.
Veröffentlicht: (2025)

Towards SMT Solver Stability via Input Normalization
von: Amrollahi, Daneshvar, et al.
Veröffentlicht: (2024)

A Local Search Algorithm for MaxSMT(LIA)
von: He, Xiang, et al.
Veröffentlicht: (2024)

Rings and Boolean Algebras as Algebraic Theories
von: De Faveri, Arturo
Veröffentlicht: (2025)

Primitive Recursive Dependent Type Theory
von: Buchholtz, Ulrik, et al.
Veröffentlicht: (2024)

Fixed Point Theorems in Computability Theory
von: Terwijn, Sebastiaan A.
Veröffentlicht: (2024)

Feasibly Constructive Proof of Schwartz-Zippel Lemma and the Complexity of Finding Hitting Sets
von: Atserias, Albert, et al.
Veröffentlicht: (2024)

MCSat-based Finite Field Reasoning in the Yices2 SMT Solver
von: Hader, Thomas, et al.
Veröffentlicht: (2024)

SMT and Functional Equation Solving over the Reals: Challenges from the IMO
von: Brown, Chad E., et al.
Veröffentlicht: (2025)