publications

2026

1. CP

   Computing Short SAT Implicants via Ising/QUBO Encodings

   Giuseppe Spallitta, Leonardo Dueñas-Osorio, and Moshe Y. Vardi

   In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026), 2026

   Abs DOI Bib HTML

   Introduces an Ising/QUBO framework with don’t-care semantics for computing short partial SAT assignments, including projected and minimum-cardinality implicants.

   @inproceedings{spallitta2026implicants,
     title = {Computing Short {SAT} Implicants via {Ising/QUBO} Encodings},
     author = {Spallitta, Giuseppe and Due{\~n}as-Osorio, Leonardo and Vardi, Moshe Y.},
     booktitle = {32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
     series = {Leibniz International Proceedings in Informatics},
     volume = {379},
     pages = {51:1--51:21},
     year = {2026},
     publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
     doi = {10.4230/LIPIcs.CP.2026.51},
   }

2. SAT

   d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries

   Gabriele Masina, Emanuele Civini, Massimo Michelutti, and 2 more authors

   In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026), 2026

   Abs DOI Bib HTML

   Extends deterministic decomposable negation normal form compilation to SMT, enabling a range of theory-level queries to be answered in polynomial time after compilation.

   @inproceedings{masina2026ddnnf,
     title = {{d-DNNF} Modulo Theories: A General Framework for Polytime {SMT} Queries},
     author = {Masina, Gabriele and Civini, Emanuele and Michelutti, Massimo and Spallitta, Giuseppe and Sebastiani, Roberto},
     booktitle = {29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
     series = {Leibniz International Proceedings in Informatics},
     volume = {377},
     pages = {25:1--25:19},
     year = {2026},
     publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
     doi = {10.4230/LIPIcs.SAT.2026.25},
   }

3. IJCAR

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

   Emanuele Civini, Gabriele Masina, Giuseppe Spallitta, and 1 more author

   In International Joint Conference on Automated Reasoning (IJCAR 2026)Accepted at IJCAR 2026 , 2026

   Abs arXiv Bib HTML

   Presents theory-agnostic and parallelizable techniques for enumerating theory lemmas tailored to an SMT formula, improving on conventional eager encodings and baseline AllSMT enumeration.

   @inproceedings{civini2026beyond,
     title = {Beyond Eager Encodings: A Theory-Agnostic Approach to Theory-Lemma Enumeration in {SMT}},
     author = {Civini, Emanuele and Masina, Gabriele and Spallitta, Giuseppe and Sebastiani, Roberto},
     booktitle = {International Joint Conference on Automated Reasoning (IJCAR 2026)},
     year = {2026},
   }

4. PoS

   Extending CDCL-based Model Enumeration with Weights

   Giuseppe Spallitta and Moshe Y. Vardi

   In 17th International Workshop on Pragmatics of SAT (PoS 2026)Accepted paper at PoS 2026 , 2026

   Abs arXiv Bib HTML

   Introduces Weighted Model Enumeration and CDCL-based algorithms that combine weight propagation, pruning, and weight-aware conflict analysis for threshold and top-k model queries.

   @inproceedings{spallitta2026wme,
     title = {Extending {CDCL}-based Model Enumeration with Weights},
     author = {Spallitta, Giuseppe and Vardi, Moshe Y.},
     booktitle = {17th International Workshop on Pragmatics of SAT (PoS 2026)},
     year = {2026},
   }

2025

1. AIJ

   Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses

   Giuseppe Spallitta, Roberto Sebastiani, and Armin Biere

   Artificial Intelligence, 2025

   Abs DOI Bib HTML

   Develops projected AllSAT and AllSMT procedures that combine CDCL, chronological backtracking, theory reasoning, and aggressive implicant shrinking without accumulating blocking clauses.

   @article{spallitta2025disjoint,
     title = {Disjoint Projected Enumeration for {SAT} and {SMT} without Blocking Clauses},
     author = {Spallitta, Giuseppe and Sebastiani, Roberto and Biere, Armin},
     journal = {Artificial Intelligence},
     volume = {345},
     pages = {104346},
     year = {2025},
     publisher = {Elsevier},
     doi = {10.1016/j.artint.2025.104346},
   }

2. JAIR

   On CNF Conversion for SAT and SMT Enumeration

   Gabriele Masina, Giuseppe Spallitta, and Roberto Sebastiani

   Journal of Artificial Intelligence Research, 2025

   Abs DOI Bib HTML

   Studies how standard CNF transformations affect partial-assignment enumeration and shows that Plaisted-Greenbaum conversion with NNF preprocessing substantially improves SAT and SMT enumeration.

   @article{masina2025cnf,
     title = {On {CNF} Conversion for {SAT} and {SMT} Enumeration},
     author = {Masina, Gabriele and Spallitta, Giuseppe and Sebastiani, Roberto},
     journal = {Journal of Artificial Intelligence Research},
     volume = {83},
     number = {11},
     year = {2025},
     doi = {10.1613/JAIR.1.16870},
   }

2024

1. AIJ

   Enhancing SMT-based Weighted Model Integration by Structure Awareness

   Giuseppe Spallitta, Gabriele Masina, Paolo Morettin, and 2 more authors

   Artificial Intelligence, 2024

   Abs DOI Bib HTML

   Combines SMT-based enumeration with weight-structure awareness to reduce redundant integrations in Weighted Model Integration across exact and approximate integration settings.

   @article{spallitta2024wmi,
     title = {Enhancing {SMT}-based Weighted Model Integration by Structure Awareness},
     author = {Spallitta, Giuseppe and Masina, Gabriele and Morettin, Paolo and Passerini, Andrea and Sebastiani, Roberto},
     journal = {Artificial Intelligence},
     volume = {328},
     pages = {104067},
     year = {2024},
     publisher = {Elsevier},
     doi = {10.1016/j.artint.2024.104067},
   }

2. ECAI

   Canonical Decision Diagrams Modulo Theories

   Massimo Michelutti, Gabriele Masina, Giuseppe Spallitta, and 1 more author

   In 27th European Conference on Artificial Intelligence (ECAI 2024), 2024

   Abs DOI Bib HTML

   Presents a general method for constructing theory-aware decision diagrams by using AllSMT-generated theory lemmas, yielding canonical diagrams when the underlying Boolean representation is canonical.

   @inproceedings{michelutti2024canonical,
     title = {Canonical Decision Diagrams Modulo Theories},
     author = {Michelutti, Massimo and Masina, Gabriele and Spallitta, Giuseppe and Sebastiani, Roberto},
     booktitle = {27th European Conference on Artificial Intelligence (ECAI 2024)},
     series = {Frontiers in Artificial Intelligence and Applications},
     volume = {392},
     pages = {4319--4327},
     year = {2024},
     publisher = {IOS Press},
     doi = {10.3233/FAIA241007},
   }

3. AAAI

   Disjoint Partial Enumeration without Blocking Clauses

   Giuseppe Spallitta, Roberto Sebastiani, and Armin Biere

   In Proceedings of the AAAI Conference on Artificial Intelligence, 2024

   Abs DOI Bib HTML

   Proposes a disjoint AllSAT algorithm that integrates CDCL, chronological backtracking, and implicant shrinking to enumerate compact partial models without introducing blocking clauses.

   @inproceedings{spallitta2024partial,
     title = {Disjoint Partial Enumeration without Blocking Clauses},
     author = {Spallitta, Giuseppe and Sebastiani, Roberto and Biere, Armin},
     booktitle = {Proceedings of the AAAI Conference on Artificial Intelligence},
     volume = {38},
     number = {8},
     pages = {8126--8135},
     year = {2024},
     doi = {10.1609/aaai.v38i8.28652},
   }

4. Sci Rep

   Effective Prime Factorization via Quantum Annealing by Modular Locally-Structured Embedding

   Jingwen Ding, Giuseppe Spallitta, and Roberto Sebastiani

   Scientific Reports, 2024

   Abs DOI Bib HTML

   Introduces a compact modular encoding of multiplier circuits for D-Wave’s Pegasus topology and evaluates annealing strategies for factoring large biprime numbers on quantum hardware.

   @article{ding2024effective,
     title = {Effective Prime Factorization via Quantum Annealing by Modular Locally-Structured Embedding},
     author = {Ding, Jingwen and Spallitta, Giuseppe and Sebastiani, Roberto},
     journal = {Scientific Reports},
     volume = {14},
     number = {1},
     pages = {3518},
     year = {2024},
     publisher = {Springer Nature},
     doi = {10.1038/s41598-024-53708-7},
   }

5. Frontiers

   Experimenting with D-Wave Quantum Annealers on Prime Factorization Problems

   Jingwen Ding, Giuseppe Spallitta, and Roberto Sebastiani

   Frontiers in Computer Science, 2024

   Abs DOI Bib HTML

   Analyzes the experimental choices behind D-Wave prime-factorization runs, including initialization, chain-strength, and annealing-offset strategies for modular embeddings.

   @article{ding2024experimenting,
     title = {Experimenting with {D-Wave} Quantum Annealers on Prime Factorization Problems},
     author = {Ding, Jingwen and Spallitta, Giuseppe and Sebastiani, Roberto},
     journal = {Frontiers in Computer Science},
     volume = {6},
     pages = {1335369},
     year = {2024},
     publisher = {Frontiers},
     doi = {10.3389/fcomp.2024.1335369},
   }

2023

1. SAT

   On CNF Conversion for Disjoint SAT Enumeration

   Gabriele Masina, Giuseppe Spallitta, and Roberto Sebastiani

   In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), 2023

   Abs DOI Bib HTML

   Evaluates CNF conversion techniques for disjoint SAT enumeration and demonstrates how NNF preprocessing can preserve shorter partial assignments and improve runtime.

   @inproceedings{masina2023cnf,
     title = {On {CNF} Conversion for Disjoint {SAT} Enumeration},
     author = {Masina, Gabriele and Spallitta, Giuseppe and Sebastiani, Roberto},
     booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
     series = {Leibniz International Proceedings in Informatics},
     volume = {271},
     pages = {15:1--15:16},
     year = {2023},
     publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
     doi = {10.4230/LIPIcs.SAT.2023.15},
   }

2022

1. UAI

   SMT-based Weighted Model Integration with Structure Awareness

   Giuseppe Spallitta, Gabriele Masina, Paolo Morettin, and 2 more authors

   In Proceedings of the Thirty-Eighth Conference on Uncertainty in Artificial Intelligence, 2022

   Abs Bib HTML

   Introduces an SMT-based Weighted Model Integration approach that exploits problem structure to avoid redundant models and supports multiple exact and approximate integration techniques.

   @inproceedings{spallitta2022wmi,
     title = {{SMT}-based Weighted Model Integration with Structure Awareness},
     author = {Spallitta, Giuseppe and Masina, Gabriele and Morettin, Paolo and Passerini, Andrea and Sebastiani, Roberto},
     booktitle = {Proceedings of the Thirty-Eighth Conference on Uncertainty in Artificial Intelligence},
     series = {Proceedings of Machine Learning Research},
     volume = {180},
     pages = {1876--1885},
     year = {2022},
     publisher = {PMLR},
   }