Giuseppe Spallitta

Rice University

Houston, Texas, USA

I am an Italian researcher and a Postdoctoral Associate at Rice University, where I work with Moshe Y. Vardi. Our current research investigates the relationship between quantum computing and SAT solving in both directions: using SAT-based techniques to support quantum verification, and using quantum computing to optimize SAT-solving tasks. More broadly, my research focuses on formal verification and automated reasoning, particularly model counting and model enumeration for SAT and SMT.

I received my Ph.D. in Information and Communication Technology from the University of Trento in 2025, advised by Roberto Sebastiani and co-advised by Armin Biere. My dissertation, Efficient and Effective Model Enumeration in SAT and SMT: Investigating Novel Procedures and Applications, developed new procedures and applications for AllSAT and AllSMT.

My broader interests include knowledge compilation, weighted model integration, probabilistic inference, and quantum approaches to reasoning. I am always happy to discuss research ideas and potential collaborations.

news

Jul 24, 2026	I have been named runner-up for the Fahiem Bacchus PhD Award in Satisfiability! It is a wonderful recognition of my Ph.D. work and its contributions to satisfiability research.
Jun 20, 2026	I got four papers appearing at FLoC 2026 across different venues! I am looking forward to sharing our work, meeting the community, and enjoying a fantastic week of logic. See you there!
May 11, 2025	I have won first place in the Poster Competition at the VIII Italian Research Day in the World, the MIUR event in Houston! It was a wonderful opportunity to present my research and connect with the Italian research community.

selected publications

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

@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},
}

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

@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},
}

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}, }

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

@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},
}

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

@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},
}