arxiv: 2605.07017 · v1 · submitted 2026-05-07 · 💻 cs.LO

Recognition: no theorem link

Computing Short SAT Implicants via Ising/QUBO Encodings

Giuseppe Spallitta, Leonardo Duenas-Osorio, Moshe Y. Vardi

Authors on Pith no claims yet

Pith reviewed 2026-05-11 00:59 UTC · model grok-4.3

classification 💻 cs.LO

keywords SATimplicantsQUBOIsing modelpartial assignmentsdon't caresquadratic optimizationsimulated annealing

0 comments

The pith

A modified Ising/QUBO model finds short SAT implicants by representing some variables as don't-cares.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops an encoding that turns SAT formulas into quadratic optimization problems where ground states can leave variables unassigned. Traditional Ising models assign every variable, but this version uses a dual-polarity trick to embed don't-care semantics directly into the quadratic terms. If the right parameters are chosen, the lowest-energy solutions become short partial assignments that still satisfy the original formula. The approach also supports shrinking those assignments to minimal size and, under some penalty functions, to minimum cardinality. Tests on random 3-SAT instances show roughly one-third of variables left unassigned while satisfiability is preserved.

Core claim

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. 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. The encoding supports implicant shrinking and projection through minor objective modifications.

What carries the argument

Dual-polarity representation that incorporates don't-care semantics directly into the quadratic terms of the Ising/QUBO model.

If this is right

Ground states correspond to short partial satisfying assignments under the identified parameter regimes.
Minor objective modifications enable implicant shrinking and projection onto subsets of variables.
When the quadratic penalty permits, the method reaches minimum-cardinality implicants.
Consecutive polarity-freezing rounds achieve minimality with high probability on the tested benchmarks.
On random 3-SAT formulas the encoding typically leaves about one-third of variables unassigned while preserving satisfiability.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Hardware solvers for quadratic problems could return short implicants directly without separate post-processing steps.
The same dual-polarity idea might apply to other constraint problems where partial assignments carry explanatory value.
Repeated freezing rounds could be adapted to other energy-based models to enforce minimality without changing the core encoding.
The framework offers a direct route from logical satisfiability to physical energy minimization while controlling assignment length.

Load-bearing premise

Suitable parameter regimes exist such that the ground states of the modified QUBO exactly match short partial satisfying assignments without introducing invalid solutions or excluding valid short implicants.

What would settle it

A concrete SAT instance on which the lowest-energy state of the encoded QUBO either violates the formula or produces a longer assignment than a known short implicant, even when parameters are set to the claimed regimes.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a workable dual-polarity QUBO encoding for short SAT implicants, but the claimed parameter regimes rest on unverified assumptions about ground-state correctness.

read the letter

The main takeaway is that this work adds a dual-polarity trick to standard SAT-to-QUBO reductions so the model can leave some variables unassigned and still produce short implicants. They tweak the objective for shrinking and projection, then state parameter regimes under which the minima should match minimal partial assignments. On random 3-SAT benchmarks with simulated annealing, the method leaves about a third of the variables free while keeping the formula satisfiable, and repeated freezing rounds reach near-minimal size most of the time. They also run some non-CNF cases. That empirical behavior is the clearest positive result here. The dual-polarity encoding itself looks like a clean, incremental step beyond the total-assignment reductions in the cited prior work. It directly supports the goal of minimal explanations without forcing a full assignment. The experiments give concrete numbers on how many variables stay free and how often minimality is recovered, which is useful data for anyone trying to apply QUBO solvers to SAT-derived problems. The soft spot sits in the parameter regimes. The paper asserts that under those values every ground state is a valid short implicant and every short implicant appears as a ground state, with no invalid low-energy solutions that satisfy the quadratic terms but falsify a clause under the partial assignment. Because the evaluation uses only simulated annealing, it cannot confirm that the true minima obey the correspondence; any regime that works for the states SA finds could still admit spurious ground states. The abstract says the regimes are provided, yet the mapping from clause penalties through the dual-polarity terms needs to be shown to block those cases for all instances, including the non-CNF formulas. Without that check or a formal argument that no such configurations exist, the central guarantee stays conditional. This paper is for researchers who already work at the SAT-QUBO boundary and want a practical way to extract short partial models. A reader focused on optimization encodings or minimal explanations would get value from the construction and the benchmark numbers. It deserves a serious referee because the encoding idea is coherent and the experiments are reported clearly, even though the theoretical regimes will need closer scrutiny.

Referee Report

2 major / 1 minor

Summary. The paper introduces an Ising/QUBO encoding for SAT that incorporates don't-care semantics for variables via a dual-polarity representation, extending standard total-assignment encodings. It claims to supply explicit parameter regimes under which the ground states of the resulting quadratic model correspond exactly to short partial satisfying assignments (implicants), achieving minimality and (under suitable penalty functions) minimum cardinality. The encoding also supports implicant shrinking and projection via objective modifications. Empirical results using simulated annealing on random 3-SAT enumeration benchmarks and non-CNF formulas report that roughly one-third of variables remain unassigned while preserving satisfiability, with successive polarity-freezing rounds achieving minimality with high probability.

Significance. If the parameter regimes are shown to be correct and the ground-state correspondence holds without spurious solutions, the work would provide a principled way to compute short implicants directly on Ising/QUBO hardware, which is relevant to automated reasoning, verification, and knowledge compilation. The dual-polarity mechanism for don't-cares is a clean technical contribution that avoids post-processing of total assignments. The empirical demonstration on benchmarks is a positive indicator of practicality, though the reliance on simulated annealing rather than exact minimization limits the strength of the validation.

major comments (2)

[parameter-regimes section] The section deriving the parameter regimes for the dual-polarity penalties and clause quadratic terms: the manuscript asserts that suitable regimes exist making every ground state a valid short partial assignment and every short implicant a ground state, but does not supply a complete case analysis or energy-gap argument showing that no invalid configuration (one that falsifies a clause under the partial assignment) can achieve lower or equal energy. This correspondence is load-bearing for the central claim of minimality and minimum-cardinality.
[empirical evaluation] Empirical evaluation section: because only simulated annealing is used, the reported solutions are not guaranteed to be true ground states of the QUBO. Consequently the experiments cannot confirm that the claimed regimes produce the asserted correspondence for the actual minima; any regime that works for SA-found states may still admit invalid lower-energy configurations.

minor comments (1)

[abstract] The abstract states that minimum-cardinality is achieved 'when the quadratic penalty function permits' but does not define the precise condition on the penalty function in the main text.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful reading and constructive feedback. We appreciate the recognition of the dual-polarity representation as a clean technical contribution for incorporating don't-care semantics. We address each major comment below, agreeing that additional rigor is warranted in the theoretical analysis and that the empirical validation requires qualification due to the heuristic solver. We will revise the manuscript to incorporate these improvements.

read point-by-point responses

Referee: [parameter-regimes section] The section deriving the parameter regimes for the dual-polarity penalties and clause quadratic terms: the manuscript asserts that suitable regimes exist making every ground state a valid short partial assignment and every short implicant a ground state, but does not supply a complete case analysis or energy-gap argument showing that no invalid configuration (one that falsifies a clause under the partial assignment) can achieve lower or equal energy. This correspondence is load-bearing for the central claim of minimality and minimum-cardinality.

Authors: We agree that the current derivation of parameter regimes would be strengthened by an explicit case analysis and energy-gap argument. The manuscript establishes regimes ensuring positive penalties for clause violations under the dual-polarity encoding and favoring shorter assignments, but it does not exhaustively enumerate invalid configurations (such as those that falsify clauses via mixed polarities or unassigned variables) nor bound the energy difference from valid ground states. In the revision, we will expand the parameter-regimes section to include a complete case analysis of all possible invalid partial assignments and a rigorous energy-gap proof showing that any configuration violating the implicant conditions has strictly higher energy than valid short implicants. This will confirm the absence of spurious lower-energy solutions and solidify the minimality claims. revision: yes
Referee: [empirical evaluation] Empirical evaluation section: because only simulated annealing is used, the reported solutions are not guaranteed to be true ground states of the QUBO. Consequently the experiments cannot confirm that the claimed regimes produce the asserted correspondence for the actual minima; any regime that works for SA-found states may still admit invalid lower-energy configurations.

Authors: We concur that simulated annealing provides heuristic rather than exact solutions, so the reported states are not guaranteed to be true minima; this limits direct empirical confirmation of the regime correspondence on the tested instances. The experiments demonstrate practical utility in finding short implicants that preserve satisfiability, but cannot rule out the theoretical possibility of undetected lower-energy invalid configurations. To address this, we will add a new subsection with exact verification on small-scale instances (using exhaustive enumeration or exact QUBO solvers such as Gurobi on reduced benchmarks), confirming that SA solutions align with true ground states and that no invalid lower-energy states exist under the regimes. For the larger random 3-SAT and non-CNF benchmarks, we will explicitly qualify the results as heuristic and report statistics on energy consistency. This is a partial revision, as exact solving remains intractable for the full benchmark suite. revision: partial

Circularity Check

0 steps flagged

No significant circularity in the dual-polarity QUBO encoding for short SAT implicants

full rationale

The paper introduces a new Ising/QUBO framework that augments standard SAT-to-QUBO encodings with an explicit dual-polarity representation to encode don't-care semantics for short implicants. It then states that it derives and provides specific parameter regimes under which the ground states of the resulting quadratic model correspond exactly to minimal (or minimum-cardinality) partial satisfying assignments. No load-bearing step reduces by construction to a fitted input, self-definition, or self-citation chain; the central mapping from clause penalties plus polarity terms to the desired implicant property is presented as a direct derivation from the quadratic objective. The empirical section uses simulated annealing only for evaluation, not for defining the regimes themselves. The derivation chain is therefore self-contained against the stated assumptions and does not exhibit any of the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

1 free parameters · 1 axioms · 1 invented entities

The central claim rests on extending standard SAT-to-Ising reductions with a new dual-polarity construct and tuned penalty parameters whose regimes are asserted to produce the desired ground states.

free parameters (1)

dual-polarity penalty coefficients
The paper states that parameter regimes must be chosen so ground states correspond to short implicants; these coefficients are not derived from first principles but selected to enforce the semantics.

axioms (1)

domain assumption Existing SAT-to-Ising/QUBO reductions map satisfying assignments to ground states of a quadratic objective
The new framework builds directly on these standard reductions before adding the dual-polarity layer.

invented entities (1)

dual-polarity representation no independent evidence
purpose: To encode don't-care (unassigned) variables inside the quadratic Ising/QUBO model
New construct introduced to allow partial assignments; no independent evidence outside the encoding itself is provided.

pith-pipeline@v0.9.0 · 5488 in / 1302 out tokens · 31935 ms · 2026-05-11T00:59:40.721440+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

19 extracted references · 18 canonical work pages

[1]

URL:https://www.sciencedirect.com/ science/article/pii/S0890540120300973,doi:10.1016/j.ic.2020.104609. 2 Z. Bian, F. A. Chudak, W. G. Macready, A. Roy, R. Sebastiani, and S. Varotti. Solving SAT and MaxSAT with a quantum annealer: Foundations and a preliminary report. In C. Dixon and M. Finger, editors,Frontiers of Combining Systems - 11th International S...

work page doi:10.1016/j.ic.2020.104609 2020
[2]

https://doi.org/10.1609/aaai.v32i1

URL:https://doi.org/10.1609/aaai.v32i1. 12204,doi:10.1609/AAAI.V32I1.12204. 4 N. Chancellor, S. Zohren, P. A Warburton, S. C Benjamin, and S. Roberts. A direct mapping of max k-SAT and high order parity checks to a chimera graph.Scientific reports, 6(1):37107, 2016.doi:10.1038/srep37107. 5 J. Ding, G. Spallitta, and R. Sebastiani. Effective prime factoriz...

work page doi:10.1609/aaai.v32i1 2016
[3]

3389/fcomp.2024.1335369,doi:10.3389/FCOMP.2024.1335369

URL:https://doi.org/10. 3389/fcomp.2024.1335369,doi:10.3389/FCOMP.2024.1335369. 7 D. Déharbe, P. Fontaine, D. Le Berre, and B. Mazure. Computing prime implicants. In2013 Formal Methods in Computer-Aided Design, pages 46–52, 2013.doi:10.1109/FMCAD.2013. 6679390. 8 F. Glover. Tabu search: A tutorial.Interfaces, 20(4):74–94, 1990.doi:10.1287/inte.20.4.74. 9 ...

work page doi:10.3389/fcomp.2024.1335369 2024
[4]

doi: 10.1287/ijoc.2.1.4. 10 A. Ignatiev, A. Previti, and J. Marques-Silva. On finding minimum satisfying assignments. In M. Rueher, editor,Principles and Practice of Constraint Programming - 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings, Lecture Notes in Computer Science, pages 287–297. Springer, 2016.doi:10.10...

work page doi:10.1287/ijoc.2.1.4 2016
[5]

URL:https://link.aps.org/doi/10.1103/PhysRevE.58.5355, doi:10.1103/PhysRevE.58.5355. 12 S. Kirkpatrick, C. D. Gelatt, and M. P. Vecchi. Optimization by simulated anneal- ing.Science, 220(4598):671–680,

work page doi:10.1103/physreve.58.5355
[6]

4598.671,doi:10.1126/science.220.4598.671

URL:https://www.science.org/doi/abs/10.1126/ science.220.4598.671, arXiv:https://www.science.org/doi/pdf/10.1126/science.220. 4598.671,doi:10.1126/science.220.4598.671. 13 A. Lucas. Ising formulations of many NP problems.Frontiers in Physics, Volume 2 - 2014, 2014.doi:10.3389/fphy.2014.00005. 14 A. Mandal, A. Roy, S. Upadhyay, and H. Ushijima-Mwesigwa. Co...

work page doi:10.1126/science.220 2014
[7]

doi:10.1145/3387902.3392627. 15 G. Masina and R. Sebastiani. Exploiting partial-assignment enumeration in optimization modulo theories. In R. Thiemann and C. Weidenbach, editors,Frontiers of Combining Systems G. Spallitta, L. Duenas-Osorio and M. Y. Vardi 25:17 - 15th International Symposium, FroCoS 2025, Reykjavik, Iceland, September 29 - October 1, 2025...

work page doi:10.1145/3387902.3392627 2025
[8]

doi:10.1007/978-3-032-04167-8\_7. 16 G. Masina, G. Spallitta, and R. Sebastiani. On CNF conversion for disjoint SAT enumeration. In M. Mahajan and F. Slivovsky, editors,26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, Alghero, Italy, July 4-8, 2023, LIPIcs, pages 15:1–15:16. Schloss Dagstuhl - Leibniz-Zentrum f...

work page doi:10.1007/978-3-032-04167-8 2023
[9]

URL:https://doi.org/ 10.4230/LIPIcs.SAT.2023.15,doi:10.4230/LIPICS.SAT.2023.15. 17 G. Masina, G. Spallitta, and R. Sebastiani. On CNF conversion for SAT and SMT enumeration. J. Artif. Intell. Res., 83,

work page doi:10.4230/lipics.sat.2023.15 2023
[10]

URL:https://doi.org/10.1613/jair.1.16870, doi:10.1613/ JAIR.1.16870. 18 S. Möhle, R. Sebastiani, and A. Biere. On enumerating short projected models.Discret. Appl. Math., 361:412–439,

work page doi:10.1613/jair.1.16870
[11]

URL:https://doi.org/10.1016/j.dam.2024.10.021, doi: 10.1016/J.DAM.2024.10.021. 19 J. Nüßlein, S. Zielinski, T. Gabor, C. Linnhoff-Popien, and S. Feld. Solving (Max) 3- SAT via Quadratic Unconstrained Binary Optimization. In J. Mikyška, C. de Mulatier, M. Paszynski, V/ V. Krzhizhanovskaya, J. J. Dongarra, and P. M.A. Sloot, editors,Com- putational Science ...

work page doi:10.1016/j.dam.2024.10.021 2024
[12]

doi:10.1007/978-3-031-36030-5_3

Springer Nature Switzerland. doi:10.1007/978-3-031-36030-5_3. 20 R.. Paredes, L. Dueñas-Osorio, K. S. Meel, and M. Y. Vardi. Principled network reliability approximation: A counting-based approach.Reliab. Eng. Syst. Saf., 191,

work page doi:10.1007/978-3-031-36030-5_3
[13]

URL:https: //doi.org/10.1016/j.ress.2019.04.025,doi:10.1016/J.RESS.2019.04.025. 21 D. A. Plaisted and S. Greenbaum. A structure-preserving clause form translation.Journal of Symbolic Computation, 2(3):293–304,

work page doi:10.1016/j.ress.2019.04.025 2019
[14]

URL:https://www.sciencedirect.com/science/ article/pii/S0747717186800281,doi:10.1016/S0747-7171(86)80028-1. 22 K. Ravi and F. Somenzi. Minimal assignments for bounded model checking. In K. Jensen and A. Podelski, editors,Tools and Algorithms for the Construction and Analysis of Sys- tems, pages 31–45, Berlin, Heidelberg,

work page doi:10.1016/s0747-7171(86)80028-1
[15]

doi:10.1007/ 978-3-540-24730-2_3

Springer Berlin Heidelberg. doi:10.1007/ 978-3-540-24730-2_3. 23 G. Spallitta, R. Sebastiani, and A. Biere. Disjoint partial enumeration without blocking clauses. InProceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence and Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence and Fourteenth Symposium on Educat...

work page doi:10.1609/aaai.v38i8.28652 2024
[16]

https://doi.org/10.1016/j

URL:https://doi.org/10.1016/j. artint.2025.104346,doi:10.1016/J.ARTINT.2025.104346. 25 G. S. Tseitin.On the Complexity of Derivation in Propositional Calculus, pages 466–483. Springer Berlin Heidelberg, Berlin, Heidelberg, 1983.doi:10.1007/978-3-642-81955-1_28. 26 Y. Yamashiro, M. Ohkuwa, H. Nishimori, and D. A. Lidar. Dynamics of reverse annealing for th...

work page doi:10.1016/j 2025
[17]

URL: https: //link.aps.org/doi/10.1103/PhysRevA.100.052321,doi:10.1103/PhysRevA.100.052321. 27 S. Zbinden, A. Bärtschi, H. N. Djidjev, and S. J. Eidenbenz. Embedding algorithms for quantum annealers with chimera and pegasus connection topologies. In P. Sadayappan, B. L. Chamberlain, G. Juckeland, and H. Ltaief, editors,High Performance Computing - 35th In...

work page doi:10.1103/physreva.100.052321 2020
[18]

doi:10.1007/978-3-030-50743-5\_10. 28 S. Zielinski. Pattern QUBOs: Algorithmic construction of 3SAT-to-QUBO transformations. Electronics, 12(16):3492, 2023.doi:10.3390/electronics12163492. CP 2026 25:18 Computing Short SAT Implicants via Ising/QUBO Encodings A Appendix A.1 Minimum Implicant Projection Proof ▶ Theorem 7(Minimum-cardinality projected satisf...

work page doi:10.1007/978-3-030-50743-5 2023
[19]

unassigned

This example shows how iterative shrinking works in the QUBO encoding. Polarity spins are progressively switched from1to0, thereby turning fixed literals into unassigned variables. At each iteration, the optimizer may keep pruning active polarities; however, pruning too aggressively would falsify some clauses and incur a large increase in the objective va...

2026