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, under the supervision of Roberto Sebastiani. 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	Thrilled to 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	Very excited to have 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	Delighted to 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},
}

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