Cover Image

Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Spallitta, Giuseppe, Sebastiani, Roberto, Biere, Armin
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Disjoint Partial Enumeration without Blocking Clauses
by: Spallitta, Giuseppe, et al.
Published: (2023)

On CNF Conversion for SAT and SMT Enumeration
by: Masina, Gabriele, et al.
Published: (2023)

On Enumerating Short Projected Models
by: Möhle, Sibylle, et al.
Published: (2021)

Beyond Eager Encodings: A Theory-Agnostic Approach to Theory-Lemma Enumeration in SMT
by: Civini, Emanuele, et al.
Published: (2026)

Extending CDCL-based Model Enumeration with Weights
by: Spallitta, Giuseppe, et al.
Published: (2026)

Canonical Decision Diagrams Modulo Theories
by: Michelutti, Massimo, et al.
Published: (2024)

Computing Short SAT Implicants via Ising/QUBO Encodings
by: Spallitta, Giuseppe, et al.
Published: (2026)

SAT Solving for Variants of First-Order Subsumption
by: Coutelier, Robin, et al.
Published: (2024)

Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration
by: Sebastiani, Roberto
Published: (2025)

Rethinking Clause Management for CDCL SAT Solvers
by: Cai, Yalun, et al.
Published: (2026)

Exploiting Partial-Assignment Enumeration in Optimization Modulo Theories
by: Masina, Gabriele, et al.
Published: (2025)

Evaluating SAT and SMT Solvers on Large-Scale Sudoku Puzzles
by: Davis, Liam, et al.
Published: (2025)

Lean-SMT: An SMT tactic for discharging proof goals in Lean
by: Mohamed, Abdalrhman, et al.
Published: (2025)

Incremental SAT-Based Enumeration of Solutions to the Yang-Baxter Equation
by: Van Caudenberg, Daimy, et al.
Published: (2025)

Characterizing Sets of Theories That Can Be Disjointly Combined
by: Przybocki, Benjamin, et al.
Published: (2025)

LLM2SMT: Building an SMT Solver with Zero Human-Written Code
by: Janota, Mikoláš, et al.
Published: (2026)

Search-Driven Clause Learning for Product-State Quantum $k$-SAT (PRODSAT-QSAT)
by: González-Castillo, Samuel, et al.
Published: (2026)

An SMT Theory for n-Indexed Sequences
by: Hara, Hichem Rami Ait El, et al.
Published: (2024)

An SMT-LIB Theory of Finite Fields
by: Hader, Thomas, et al.
Published: (2024)

On SMT Theory Design: The Case of Sequences
by: Hara, Hichem Rami Ait El, et al.
Published: (2024)

Efficient Volume Computation for SMT Formulas
by: Shaw, Arijit, et al.
Published: (2025)

Hint-Based SMT Proof Reconstruction
by: Clune, Joshua, et al.
Published: (2026)

Invariant Checking for SMT-based Systems with Quantifiers
by: Redondi, Gianluca, et al.
Published: (2024)

Number theory combination: natural density and SMT
by: Toledo, Guilherme V., et al.
Published: (2025)

Integer Reasoning Modulo Different Constants in SMT
by: Pertseva, Elizaveta, et al.
Published: (2025)

System ASPMT2SMT:Computing ASPMT Theories by SMT Solvers
by: Bartholomew, Michael, et al.
Published: (2025)

Partial Quantifier Elimination By Certificate Clauses
by: Goldberg, Eugene
Published: (2020)

Towards SMT Solver Stability via Input Normalization
by: Amrollahi, Daneshvar, et al.
Published: (2024)

Towards Learning Infinite SMT Models (Work in Progress)
by: Janota, Mikoláš, et al.
Published: (2025)

SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology
by: Huvar, Ondřej, et al.
Published: (2026)

RustSAT: A Library For SAT Solving in Rust
by: Jabs, Christoph
Published: (2025)

A Relational Theory of Grounding and a new Grounder for SMT
by: Carbonnelle, Pierre
Published: (2026)

Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols
by: Hozzová, Petra, et al.
Published: (2025)

Equational Theorem Proving for Clauses over Strings
by: Kim, Dohan
Published: (2023)

MCSat-based Finite Field Reasoning in the Yices2 SMT Solver
by: Hader, Thomas, et al.
Published: (2024)

SMT and Functional Equation Solving over the Reals: Challenges from the IMO
by: Brown, Chad E., et al.
Published: (2025)

CTL* Verification and Synthesis using Existential Horn Clauses
by: Carelli, Mishel, et al.
Published: (2024)

Logic Optimization Meets SAT: A Novel Framework for Circuit-SAT Solving
by: Shi, Zhengyuan, et al.
Published: (2024)

Expressiveness of SHACL Features and Extensions for Full Equality and Disjointness Tests
by: Bogaerts, Bart, et al.
Published: (2022)

Enumerating Minimal Unsatisfiable Cores of LTLf formulas
by: Ielo, Antonio, et al.
Published: (2024)