Cover Image

Disjoint Partial Enumeration without Blocking Clauses

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Spallitta, Giuseppe, Sebastiani, Roberto, Biere, Armin
Format:	Preprint
Published:	2023
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 Projected Enumeration for SAT and SMT without Blocking Clauses
by: Spallitta, Giuseppe, et al.
Published: (2024)

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)

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

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

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

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

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

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

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)

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

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

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

CTL* Verification and Synthesis using Existential Horn Clauses
by: Carelli, Mishel, 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)

Testing for Renamability to Classes of Clause Sets
by: Brandl, Albert, et al.
Published: (2025)

Extended Resolution Clause Learning via Dual Implication Points
by: Buss, Sam, et al.
Published: (2024)

Enumerating Independent Linear Inferences
by: Das, Anupam, et al.
Published: (2021)

Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes
by: Schirrmacher, Nicole, et al.
Published: (2023)

From MBQI to Enumerative Instantiation and Back
by: Dančo, Marek, et al.
Published: (2025)

Efficient Neural Clause-Selection Reinforcement
by: Suda, Martin
Published: (2025)

Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
by: Katsura, Hiroyuki, et al.
Published: (2025)

Catamorphic Abstractions for Constrained Horn Clause Satisfiability
by: De Angelis, Emanuele, et al.
Published: (2024)

Univalence without function extensionality
by: Cavallo, Evan, et al.
Published: (2026)

Enriching Ontologies with Disjointness Axioms using Large Language Models
by: Crum, Elias, et al.
Published: (2024)

PICID: Proof-Driven Clause Learning in Neural Network Verification
by: Isac, Omri, et al.
Published: (2025)

FO-Query Enumeration over SLP-Compressed Structures of Bounded Degree
by: Lohrey, Markus, et al.
Published: (2025)

A Linear Temporal Logic of Frequencies on Series of Events
by: Antonelli, Melissa, et al.
Published: (2026)

Normalisation for Negative Free Logics without and with Definite Descriptions
by: Kürbis, Nils
Published: (2024)

A Simple and Effective ASP-Based Tool for Enumerating Minimal Hitting Sets
by: Kabir, Mohimenul, et al.
Published: (2025)

Internal and External Calculi: Ordering the Jungle without Being Lost in Translations
by: Lyon, Tim S., et al.
Published: (2023)

Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification
by: Somorjai, Márk, et al.
Published: (2024)

Using Color Refinement to Boost Enumeration and Counting for Acyclic CQs of Binary Schemas
by: Riveros, Cristian, et al.
Published: (2024)

Partial Redundancy in Saturation
by: Hajdu, Márton, et al.
Published: (2025)

Refutation calculi for lattice-based logics: from display to tableaux
by: De Domenico, Andrea, et al.
Published: (2026)

CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses
by: Dobos-Kovács, Mihály, et al.
Published: (2025)

Proceedings of the 12th Workshop on Horn Clauses for Verification and Synthesis
by: De Angelis, Emanuele, et al.
Published: (2025)

Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity
by: Meng, Qiaolan, et al.
Published: (2025)