DROPS

Document

DOI: 10.4230/LIPIcs.CP.2026.51

Computing Short SAT Implicants via Ising/QUBO Encodings

Authors: Giuseppe Spallitta, Leonardo Duenas-Osorio, and Moshe Y. Vardi

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

Abstract

Many reasoning tasks require short partial satisfying assignments (implicants), sometimes focusing on a set of important variables. SAT-to-Ising-QUBO formulations are implicitly designed so that ground states correspond to total assignments, since the Ising/QUBO model assigns a value to every spin and has no native representation of unassigned variables. We introduce an Ising/QUBO framework that incorporates "don’t-care" semantics into the quadratic model via a dual-polarity representation, enabling the retrieval of short implicants. The encoding supports implicant shrinking and projection through minor objective modifications. We provide parameter regimes under which ground states correspond to short partial satisfying assignments, achieving minimality and, when the quadratic penalty function permits, minimum-cardinality. We empirically evaluate the encoding with simulated annealing on random 3-SAT enumeration benchmarks and non-CNF formulas, showing that it leaves about one-third of variables unassigned on random 3-SAT formulas while preserving satisfiability, and that consecutive polarity-freezing rounds achieve minimality (and minimum-cardinality) with high probability.

Cite as

Giuseppe Spallitta, Leonardo Duenas-Osorio, and Moshe Y. Vardi. Computing Short SAT Implicants via Ising/QUBO Encodings. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 51:1-51:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{spallitta_et_al:LIPIcs.CP.2026.51,
  author =	{Spallitta, Giuseppe and Duenas-Osorio, Leonardo and Vardi, Moshe Y.},
  title =	{{Computing Short SAT Implicants via Ising/QUBO Encodings}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{51:1--51:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.51},
  URN =		{urn:nbn:de:0030-drops-266843},
  doi =		{10.4230/LIPIcs.CP.2026.51},
  annote =	{Keywords: SAT-to-QUBO, Ising encodings, prime implicants, minimum-cardinality implicant, partial and projected assignments}
}

Search Results

Documents authored by Duenas-Osorio, Leonardo

Computing Short SAT Implicants via Ising/QUBO Encodings

Abstract

Cite as

Thanks for your feedback!

Could not send message