Strong Structural Bounds for MaxSAT: The Fine Details of Using Neuromorphic and Quantum Hardware Accelerators

Jai Grover; Markus Hecher; Max Bannach

REVIEW 3 major objections 4 minor 49 references

Strong Structural Bounds for MaxSAT: The Fine Details of Using Neuromorphic and Quantum Hardware Accelerators

T0 review · 3 major / 4 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper proves that MaxSAT, Max2SAT, and QUBO—the optimization problem behind quantum annealers and neuromorphic chips—reduce to one another in linear time while preserving treewidth up to small constants.

desk verdict The primal-treewidth reductions are solid and citable; the incidence-treewidth half of the main theorem rests on Lemma 3, which has a concrete counterexample and needs major repair before the headline claims can stand. read the letter →

arxiv 2412.10289 v2 pith:CMEC75HY submitted 2024-12-13 cs.LO quant-ph

Max Bannach , Jai Grover , Markus Hecher This is my paper · ORCID

classification cs.LOquant-ph MSC 68Q1768Q2568Q2705C85

keywords MaxSATMax2SATQUBOtreewidthincidencefixed-parameteralgorithmsETHandSETHmodelcounting

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper studies the chain of encodings that send optimization problems to specialized hardware: a problem is encoded as MaxSAT, then Max2SAT, then a quadratic unconstrained binary optimization problem (QUBO), whose ground state the hardware finds. The central claim is that all three formats are equivalent under reductions that run in linear time and preserve treewidth—a measure of how tree-like a formula's variable interactions are—up to small constants. This matters because earlier encoding studies looked only at formula size, while both dynamic-programming solvers and hardware embedding become practical when treewidth stays small. If the claim is right, a MaxSAT instance with small treewidth maps to a QUBO with small treewidth and back, and the matching lower bounds show the exponential dependence on treewidth cannot be avoided. The paper also gives new algorithms for Max2SAT, QUBO, and several weighted MaxSAT fragments by reducing to model counting.

What carries the argument

The argument is carried by a sequence of eight local reduction rules together with one tree-decomposition-guided encoding. Each rule replaces a clause (or a QUBO term) by a constant number of new pieces while a proof shows how to update any tree decomposition by attaching small bags, so the structural parameter grows only by the stated constant. For example, Rule 5 replaces a three-literal clause by six binary clauses using a fresh variable, and Rule 6 rewrites positive literals into double-railed form so that only negative literals remain before the final translation into QUBO terms. The step that carries the incidence-treewidth claim is Lemma 3, which splits long hard clauses along a supplied tree decomposition: it creates synchronized copies $x_t$ of each variable in every bag and clause-copy variables $c_t$, then adds a reason clause $c_t \to \bigvee_{\ell \in c \cap \chi(t)} \ell \lor \bigvee_{t'} c_{t'}$ so every satisfied clause copy is justified by a true literal in the current bag or a copy in a child bag. Chains of bags inserted between parent and child keep the incidence treewidth of the encoded formula at $2k$.

What would settle it

Take a small weighted formula with known optimum cost, fix a width-$k$ tree decomposition of its incidence graph, apply the Lemma 3 rewriting, and verify that the resulting three-literal formula has the same optimum cost and incidence treewidth at most $2k$. A mismatch on any instance would refute the central structural claim, since the proof of Theorem 1 applies Lemma 3 to every hard clause.

Watch

Extended reading notes

Core claim

The main theorem is that MaxSAT, Max2SAT, and QUBO are equivalent under linear-time reductions: primal treewidth increases by an additive constant at most two, and incidence treewidth increases by a multiplicative constant at most three. Here primal treewidth is the treewidth of the graph connecting variables that occur together in a clause, and incidence treewidth is the treewidth of the bipartite graph connecting variables to the clauses containing them. From this equivalence the paper derives an $O(2^{\mathrm{tw}(H)}|H|)$ algorithm for finding the ground state of a QUBO and, under the exponential-time hypotheses, lower bounds of $\Omega(2^{\mathrm{tw}(\phi)})\mathrm{poly}(|\phi|)$ and $\Omega(2^{\mathrm{itw}(\phi)/3})\mathrm{poly}(|\phi|)$ for Max2SAT and QUBO. For binary formulas it closes the gap in the exponent by proving Max2SAT and QUBO are solvable in $O(2^{\mathrm{itw}(\phi)}|\phi|)$. For weighted fragments with unbounded clause length, unary-MaxSAT, multiplicative-MaxSAT, and lexicographic-MaxSAT are shown to reduce to #SAT with incidence treewidth increased by one, giving the same $O(2^{\mathrm{itw}(\phi)}|\phi|)$ running time from model counting.

Load-bearing premise

The claim stands or falls on Lemma 3, which says that a tree decomposition of width $k$ for a weighted formula can be used to rewrite it into a formula with three-literal clauses, unchanged optimal cost, and incidence treewidth at most $2k$; if that rewriting has a counterexample, the factor-three equivalence and its lower bounds collapse.

Editorial extensions

If this is right

A QUBO whose Hamiltonian has primal treewidth $k$ can have its ground state computed in $O(2^k|H|)$, so treewidth—not just term count—determines when Ising-style hardware embedding is viable.
Under SETH, Max2SAT and QUBO each require $\Omega(2^{\mathrm{tw}})\mathrm{poly}$ time, and under ETH they require $2^{o(\mathrm{tw})}\mathrm{poly}$, matching the existing treewidth-based dynamic programs.
Max2SAT and QUBO can be solved in $O(2^{\mathrm{itw}}|\phi|)$, removing the factor-two gap that earlier incidence-treewidth algorithms carried.
Unary-, mult-, and lex-MaxSAT can be solved in $O(2^{\mathrm{itw}}|\phi|)$ via structure-preserving reductions to #SAT.
The two directions of the reduction mean MaxSAT and QUBO can be interchanged inside an encoding pipeline without changing the structural difficulty of the instance.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Editorial inference: the factor-three loss for incidence treewidth is probably not a proof artifact; an additive-loss reduction would resolve the paper's Open Problem 1 and make the MaxSAT incidence lower bound tight. Until then, practical encoding pipelines should supply a tree decomposition rather than hoping the structure survives.
Editorial inference: a direct engineering test follows from the paper's claims—on any accelerator that solves QUBO, instances of equal size but different treewidth should show different embedding success and solution quality if the structure-preserving reductions are doing real work.
Editorial inference: the #SAT reductions place weighted MaxSAT fragments under the same structural bottleneck as model counting, so any future improvement to incidence-treewidth counting algorithms immediately upgrades these MaxSAT solvers.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Two things to know. First, this paper is worth reading for the primal-treewidth chain and for the upper-bound results. The reduction rules from MaxSAT to Max2SAT to QUBO are mostly standard, but the careful bookkeeping of primal treewidth is genuinely useful, and the O(2^tw) QUBO algorithm plus the model-counting reductions for unary/mult/lex MaxSAT are real contributions. The exposition is honest about the open gaps, and the citation pattern is fine; the self-citation [7] is contextual and does not carry any theorem.

Second, the incidence-treewidth story is not established. Lemma 3, the load-bearing step for the factor-3 incidence chain and the itw/3 lower bounds, is false as stated. Take phi = {(x)^\infty} and the valid width-1 tree decomposition with root {c,x} and child {x}. The encoding produces the hard unit (c_root)^\infty plus sync clauses, and Eq. (3) at the root becomes c_root -> false because x appears in the only child. The output is unsatisfiable even though cost(phi) = 0. The proof of cost(psi) <= cost(phi) claims that for a satisfied clause and a true literal there is a bag t where the literal is usable, but it never proves the necessary condition that the literal's variable is absent from every child of t. That condition is essential, and the counterexample shows it can fail. The same obstruction occurs whenever a clause's satisfying literal lives in a child subtree that does not contain the clause copy.

This does not kill the primal-treewidth results, nor Theorem 2 or the model-counting lemmas, which look sound to me. But it does mean the incidence-treewidth equivalence in Theorem 1, Corollaries 2 and 3' incidence halves, and Lemma 5 need either a real fix or a downgrade. The authors should add a normalization step that ensures a witness bag exists for every clause-literal pair, prove it, or restrict the claims to primal treewidth.

Who gets value from this paper: people encoding MaxSAT into QUBO for annealers or neuromorphic hardware, and the parameterized complexity community. The paper deserves a serious referee, but the referee should be told to focus on Lemma 3 and the incidence-treewidth chain. My recommendation: send to peer review with a request for major revision rather than desk reject; the primal results and the algorithms are worth keeping, and the incidence claims may be repairable.

Referee Report

3 major / 4 minor

Summary. The paper studies structure-preserving reductions between MaxSAT, Max2SAT, and QUBO, motivated by encoding problems for Ising machines and neuromorphic accelerators. The main theorem claims that MaxSAT, Max2SAT, and QUBO are equivalent under linear-time reductions that preserve primal treewidth up to an additive factor of two and incidence treewidth up to a multiplicative factor of three. From these reductions the paper derives ETH/SETH lower bounds for Max2SAT and QUBO, a 2^{tw(H)}|H| algorithm for QUBO, and improved incidence-treewidth algorithms for binary fragments via a contraction argument. It also gives model-counting based O(2^{itw}|φ|) algorithms for unary-, mult-, and lex-MaxSAT.

Significance. If the main claims are correct, the paper makes a valuable contribution: it gives the first structure-aware reductions along the MaxSAT-to-QUBO pipeline, yields tight ETH/SETH lower bounds for Max2SAT and QUBO with respect to primal treewidth, and provides new fixed-parameter algorithms for QUBO and MaxSAT fragments. The model-counting reductions are elegant and likely correct. The primal-treewidth half of the paper is elementary and appears sound. However, the incidence-treewidth claims, including Corollaries 2 and 3 for the incidence parameter, rest on Lemma 3, which contains a load-bearing correctness gap: the reason-clause (Eq. (3)) does not always admit the witness bag that the proof requires. Since the paper's abstract and Theorem 1 explicitly emphasize the incidence-treewidth equivalence, this issue must be resolved before the results can be accepted.

major comments (3)

[Section 3.1, Lemma 3] The same obstruction can occur more generally: whenever a clause's true literals all appear in child subtrees that do not contain the clause, Eq. (3) at the clause's root bag has no witness. The lemma needs either a normalization condition on the rooted tree decomposition — for example, a guarantee that a witness bag exists for every satisfiable clause and true literal — or a modified reason-clause semantics. Re-rooting the example fixes the specific case, but the lemma as written neither states nor proves such a condition.
[Section 3.2, Lemma 5] Lemma 5 inherits the flaw of Lemma 3. Its proof says "use the encoding of Lemma 3 and utilize Rule 5 for constraint (3)". Since Lemma 3 does not currently establish a correct cost-preserving w3cnf encoding, Lemma 5 does not establish the claimed w2cnf output with itw(ψ) ≤ 3k. A repair of Lemma 3 must be carried through to Lemma 5 and to all incidence-treewidth consequences that depend on it.
[Section 3.1, Lemma 3 (treewidth argument)] Even apart from the correctness gap, the treewidth part of Lemma 3 is only sketched in the sentences describing chains between a node t and its children: "The first element of the chain contains χ(t) \ {c_t} ∪ {c_{t'}}" and "This process is repeated until we reach t'". It is not made precise how the multiple clauses added to the same chain interact, nor how the size of every bag is bounded by 2k after all additions. The reader needs a formal construction of the resulting tree decomposition, including coverage of every edge of the new incidence graph and connectedness of each vertex's bags. This is secondary to the correctness issue, but it would still need to be supplied in a revision.

minor comments (4)

[Section 5, Lemma 9] The phrase "fresh weighted variables w_i with weight 1" is ambiguous because MaxSAT weights are defined on clauses, not variables. Presumably each w_i is a fresh variable whose unit clause carries weight 1; please clarify the wording.
[Section 4, Lemma 8] The phrase "cannot increase the treewidth past 2" is unclear. Since contracting a vertex cannot increase treewidth, the cited almost-simplicial rule should be stated precisely so that the reader can verify the contraction argument.
[Section 5, Lemma 13] In the lexicographic-to-multiplicative translation, if the smallest weight is assigned 2^0 and the second-smallest 2^{|vars|+1}, then the n-th smallest weight should be 2^{(n-1)(|vars|+1)} rather than 2^{n(|vars|+1)}; check the indexing.
[Throughout] There are several typographical issues: "twidht" in Section 1.1, "it's" in Section 1.3, and some illegible arrow labels in Figure 2. Please proofread and reformat.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the MaxSAT/QUBO reductions are self-contained constructive proofs against external complexity definitions, and the sole self-citation is contextual rather than load-bearing.

full rationale

The derivation chain in the paper consists of explicit reduction rules (Rules 1-8), each accompanied by a construction of the output formula or Hamiltonian and by an argument that treewidth grows by at most the stated additive or multiplicative amount. The main theorems (Theorems 1-4) are proved from those rules, not by assuming the theorem statements. No parameter is fitted to data, and no target result is used as an input to its own proof. The only self-citation is reference [7], Bannach and Hecher, cited in the introduction with the motivating remark that 'treewidth-based approaches are competitive for maxsat [7]'; this remark does not support any theorem or reduction rule and is therefore not load-bearing. External results are cited where needed: Rule 5's correctness is attributed to Ansotegui and Levy [5], the incidence-treewidth-guided splitting of long clauses builds on Lampis et al. [27], and the #SAT upper bounds rely on Slivovsky and Szeider [44]. The proof of Lemma 3 is the most delicate step in the paper, and a skeptical reader could question whether equation (3) fully preserves cost for every rooted tree decomposition; however, even if that proof has a correctness gap, the concern would be soundness/completeness of a reduction, not circularity, because Lemma 3 does not define cost(phi) in terms of cost(psi) or import the desired equality from a self-citation. The paper also openly states limitations that further confirm non-circularity: Open Problem 1 asks for an additive-factor incidence-treewidth reduction to w2cnf, and Open Problem 2 asks whether a tree-decomposition-free reduction to w3cnf exists. These are genuine open questions about whether the stated constants can be improved, not hidden assumptions that the conclusions are already present in the premises. Consequently, no circular step can be exhibited with a quoted reduction from the paper's own equations, and the appropriate score is 0.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

There are no fitted free parameters in this theory paper. The reductions introduce many fresh auxiliary variables, but these are standard auxiliary variables in reduction proofs and are not postulated physical entities with independent evidence. The load-bearing assumptions are the complexity hypotheses ETH/SETH, the exact-solver idealization of the hardware, and the correctness of a cited Max3SAT-to-Max2SAT gadget.

assumptions (4)

domain assumption ETH and SETH hold
The lower bounds in Corollaries 2 and 3 are conditional on the Exponential Time Hypothesis and Strong Exponential Time Hypothesis; without these, the running-time lower bounds do not follow.
domain assumption The IPU is modeled as an exact solver
Footnote 2 states that real devices such as D-Wave output only heuristic solutions, so the formal QUBO equivalence and all exact bounds assume an idealized exact Ising machine.
domain assumption Hard clauses are simulated by a sufficiently large top weight h
Rule 4 defines h = 1 + sum of finite weights and uses theta as a threshold; this standard encoding is needed to make all clauses soft before the Max3SAT-to-Max2SAT step and assumes weights can be represented as integers.
standard math Ansotegui-Levy Max3SAT-to-Max2SAT gadget is correct
Rule 5 relies on [5, Lemma 3] for the correctness of the six-clause gadget; the paper gives only a brief counting argument and does not re-prove the gadget from first principles.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Strong Structural Bounds for MaxSAT: The Fine Details of Using Neuromorphic and Quantum Hardware Accelerators." pith.science (2026). https://pith.science/paper/CMEC75HY

@misc{pith2026241210289,
  author       = {Pith},
  title        = {Pith review of: Strong Structural Bounds for MaxSAT: The Fine Details of Using Neuromorphic and Quantum Hardware Accelerators},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CMEC75HY}},
  note         = {Machine review of arXiv:2412.10289}
}

read the original abstract

Hardware accelerators like quantum annealers or neuromorphic chips are capable of finding the ground state of a Hamiltonian. A promising route in utilizing these devices is via methods from automated reasoning: The problem at hand is first encoded into MaxSAT; then MaxSAT is reduced to Max2SAT; and finally, Max2SAT is translated into a Hamiltonian. It was observed that different encodings can dramatically affect the efficiency of the hardware accelerators. Yet, previous studies were only concerned with the size of the encodings rather than with syntactic or structural properties. We establish structure-aware reductions between MaxSAT, Max2SAT, and the quadratic unconstrained binary optimization problem (QUBO) that underlies such hardware accelerators. All these problems turn out to be equivalent under linear-time, treewidth-preserving reductions. As a consequence, we obtain tight lower bounds under ETH and SETH for Max2SAT and QUBO, as well as a new time-optimal fixed-parameter algorithm for QUBO. While our results are tight up to a constant additive factor for the primal treewidth, we require a constant multiplicative factor for the incidence treewidth. To close the emerging gap, we supplement our results with novel time-optimal algorithms for fragments of MaxSAT based on model counting.

Figures

Figures reproduced from arXiv: 2412.10289 by the authors.

**Figure 1.** Illustration of an ipu that operates on an n-variable Ising model H(x1, . . . , xn). The input are the weights of H given as n×n upper triangular matrix (n is fixed). The output is a vector ~x ∈ {0, 1} n that minimizes H(~x). ipu H(x1, . . . , xn) as W ∈ R n×n x1, . . . , xn ∈ {0, 1} n minimizing H(x1, . . . , xn) The Ising model approach gained momentum since it naturally appeared in various promising technologies… view at source ↗

**Figure 2.** An overview of our reductions between various variants of maxsat. All reductions in the picture are linear-time computable. An arrow A a tw +b → B means that if the instance of A has primal treewidth tw, the instance of B has primal treewidth at most a tw +b. If the label of an arrow is “max(tw, x)”, the reduction increases the treewidth to at most x. Finally, if the arrow is dashed, the reduction requires a tree… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

49 extracted references · 30 canonical work pages

[7]

Structure-Guided Cube-and -Conquer for MaxSAT

Max Bannach and Markus Hecher. Structure-Guided Cube-and -Conquer for MaxSAT. In NASA Formal Methods - 16th International Symposium, NFM 2024, Mo ﬀett Field, CA, USA, June 4-6, 2024, Proceedings, pages 3–20, 2024. doi:10.1007/978-3-031-60698-4_1

work page doi:10.1007/978-3-031-60698-4_1 2024
[1]

Arthur, Paul Merolla, Nabil Imam, Yutaka Y

Filipp Akopyan, Jun Sawada, Andrew Cassidy, Rodrigo Alvarez-Ic aza, John V. Arthur, Paul Merolla, Nabil Imam, Yutaka Y. Nakamura, Pallab Datta, Gi-Joon Nam, Brian T aba, Michael P. Beakes, Bernard Brezzo, Jente B. Kuang, Rajit Manohar, William P. Risk, Bry an L. Jackson, and Dhar- mendra S. Modha. TrueNorth: Design and Tool Flow of a 65 mW 1 Million N eur...

work page
[2]

Quantum Optimization Algo- rithm for LEO Satellite Communications Based on Cell-Free Massive MIM O

Hayder Al-Hraishawi, Junaid ur Rehman, and Symeon Chatzinotas . Quantum Optimization Algo- rithm for LEO Satellite Communications Based on Cell-Free Massive MIM O. In IEEE International Conference on Communications, ICC 2023 - Workshops, Rome, I taly, May 28 - June 1, 2023 , pages 1759–1764, 2023. doi:10.1109/ICCWORKSHOPS57953.2023.10283753

arXiv 2023
[3]

Zahangir Alom, Brian Van Essen, Adam T

Md. Zahangir Alom, Brian Van Essen, Adam T. Moody, David Peter W idemann, and Tarek M. Taha. Quadratic Unconstrained Binary Optimization (QUBO) on Neuromorp hic Computing System. In 2017 International Joint Conference on Neural Networks, IJ CNN 2017, Anchorage, AK, USA, May 14-19, 2017 , pages 3922–3929, 2017. doi:10.1109/IJCNN.2017.7966350

work page arXiv 2017
[4]

Satellite Adaptive Onboard Beamforming Using Neuromorphic Processors

Wallace Alves-Martins, Eva Lagunas, Nicolas Skatchkovsky, Flor de Guadalupe Ortiz Gomez, Ge- oﬀrey Eappen, Osvaldo Simeone, Bipin Rajendran, and Symeon Chat zinotas. Satellite Adaptive Onboard Beamforming Using Neuromorphic Processors. In IEEE International Symposium on Per- sonal, Indoor and Mobile Radio Communications . IEEE, Washington, United States, 2024

work page 2024
[5]

Reducing SAT to Max2SAT

Carlos Ans´ otegui and Jordi Levy. Reducing SAT to Max2SAT. I n Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence , IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021 , pages 1367–1373, 2021. doi:10.24963/IJCAI.2021/189

work page doi:10.24963/ijcai.2021/189 2021
[6]

SAT, Gadgets, Max2XOR, and Quantum Annealers

Carlos Ans´ otegui and Jordi Levy. SAT, Gadgets, Max2XOR, a nd Quantum Annealers. CoRR, abs/2403.00182, 2024. arXiv:2403.00182, doi:10.48550/ARXIV.2403.00182

work page Pith review arXiv doi:10.48550/arxiv.2403.00182 2024
[8]

Chudak, William G

Zhengbing Bian, Fabi´ an A. Chudak, William G. Macready, Aidan Roy, Roberto Sebastiani, and Stefano Varotti. Solving SAT and MaxSAT with a Quantum Anneale r: Foundations and a Preliminary Report. In Frontiers of Combining Systems - 11th International Sympo- sium, FroCoS 2017, Bras´ ılia, Brazil, September 27-29, 201 7, Proceedings, pages 153–171, 2017. do...

work page doi:10.1007/978-3-319-66167-4_9 2017

Show all 49 references

[9]

Bodlaender, Paul S

Hans L. Bodlaender, Paul S. Bonsma, and Daniel Lokshtanov. T he Fine Details of Fast Dynamic Programming over Tree Decompositions. In Parameterized and Exact Computation - 8th Inter- national Symposium, IPEC 2013, Sophia Antipolis, France, S eptember 4-6, 2013, Revised Selecte...

2013 doi
[10]

Bodlaender, Arie M

Hans L. Bodlaender, Arie M. C. A. Koster, Frank van den Eijkho f, and Linda C. van der Gaag. Pre-processing for Triangulation of Probabilistic Networks. In 17th Conference in Uncertainty in Artiﬁcial Intelligence (UAI 2001) , pages 32–39, 2001

2001
[11]

On Compiling CNFs into Structured Deterministic DNNFs

Simone Bova, Florent Capelli, Stefan Mengel, and Friedrich Slivovs ky. On Compiling CNFs into Structured Deterministic DNNFs. In Theory and Applications of Satisﬁability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings , p...

2015 doi
[12]

Tractable QBF by Knowledge C ompilation

Florent Capelli and Stefan Mengel. Tractable QBF by Knowledge C ompilation. In 36th International Symposium on Theoretical Aspects of Computer Science, STAC S 2019, March 13-16, 2019, Berlin, Germany, pages 18:1–18:16, 2019. doi:10.4230/LIPICS.STACS.2019.18

2019 doi
[13]

A Direct Mapping of Max k-SAT and High Order Parity Checks to a Chime ra Graph

Nicholas Chancellor, Stefan Zohren, Paul A Warburton, Simon C Benjamin, and Stephen Roberts. A Direct Mapping of Max k-SAT and High Order Parity Checks to a Chime ra Graph. Scientiﬁc reports, 6(1):37107, 2016

2016
[15]

Comparing QUBO Models for Quantum Annealing : Integer Encodings for Permutation Problems

Philippe Codognet. Comparing QUBO Models for Quantum Annealing : Integer Encodings for Permutation Problems. International Transactions in Operational Research , 2024. 13

2024
[16]

Evalua ting Ising Processing Units with Inte- ger Programming

Carleton Coﬀrin, Harsha Nagarajan, and Russell Bent. Evalua ting Ising Processing Units with Inte- ger Programming. In Integration of Constraint Programming, Artiﬁcial Intelli gence, and Operations Research - 16th International Conference, CPAIOR 2019, The ssaloniki, Greece, J...

2019 doi
[17]

Fomin, Lukasz Kowalik, Daniel Lokshtan ov, D´ aniel Marx, Marcin Pilipczuk, Michal Pilipczuk, and Saket Saurabh

Marek Cygan, Fedor V. Fomin, Lukasz Kowalik, Daniel Lokshtan ov, D´ aniel Marx, Marcin Pilipczuk, Michal Pilipczuk, and Saket Saurabh. Parameterized Algorithms . Springer, 2015. doi:10.1007/978-3-319-21275-3

2015 doi
[18]

Patton, Catherine D

Prasanna Date, Robert M. Patton, Catherine D. Schuman, an d Thomas E. Potok. Eﬃciently Em- bedding QUBO Problems on Adiabatic Quantum Computers. Quantum Inf. Process. , 18(4):117,
[19]

Fonseca Guerra, Prasad Joshi, Philipp Plank, and Sumedh R

Mike Davies, Andreas Wild, Garrick Orchard, Yulia Sandamirskaya , Gabriel A. Fonseca Guerra, Prasad Joshi, Philipp Plank, and Sumedh R. Risbud. Advancing Neurom orphic Comput- ing With Loihi: A Survey of Results and Outlook. Proc. IEEE , 109(5):911–934, 2021. doi:10.1109/JPROC...

2021
[20]

M. R. Garey, David S. Johnson, and Larry J. Stockmeyer. Som e Simpliﬁed NP-Complete Graph Problems. Theor. Comput. Sci. , 1(3):237–267, 1976. doi:10.1016/0304-3975(76)90059-1

1976 doi
[21]

Deep Space Network Scheduling Using Quan tum Annealing

Alexandre Guillaume, Edwin Y Goh, Mark D Johnston, Brian D Wilson, Anita Ramanan, Frances Tibble, and Brad Lackey. Deep Space Network Scheduling Using Quan tum Annealing. IEEE Trans- actions on Quantum Engineering , 3:1–13, 2022

2022
[22]

RC2: an Eﬃcient MaxSAT Solver

Alexey Ignatiev, Ant´ onio Morgado, and Jo˜ ao Marques-Silva. RC2: an Eﬃcient MaxSAT Solver. J. Satisf. Boolean Model. Comput. , 11(1):53–64, 2019. doi:10.3233/SAT190116

2019 doi
[23]

Quantum Annealing with Manufactured Spins

Mark W Johnson, Mohammad HS Amin, Suzanne Gildert, Trevor La nting, Firas Hamze, Neil Dick- son, Richard Harris, Andrew J Berkley, Jan Johansson, Paul Buny k, et al. Quantum Annealing with Manufactured Spins. Nature, 473(7346):194–198, 2011

2011
[24]

Eﬃcient and Scalable Architecture for Multiple-Chip Implementation of Simulated Bifurcat ion Machines

Tomoya Kashimata, Masaya Yamasaki, Ryo Hidaka, and Kosuke T atsumura. Eﬃcient and Scalable Architecture for Multiple-Chip Implementation of Simulated Bifurcat ion Machines. IEEE Access, 12:36606–36621, 2024. doi:10.1109/ACCESS.2024.3374089

2024
[25]

M. R. Krom. The Decision Problem for a Class of First-Order Form ulas in Which all Disjunctions are Binary. Mathematical Logic Quarterly , 13(1-2):15–20, 1967. doi:10.1002/malq.19670130104

1967 doi
[26]

Quantum Annealing-Based Software Components: An Exper- imental Case Study with SAT Solving

Tom Kr¨ uger and Wolfgang Mauerer. Quantum Annealing-Based Software Components: An Exper- imental Case Study with SAT Solving. In ICSE ’20: 42nd International Conference on Software Engineering, Workshops, Seoul, Republic of Korea, 27 June - 19 July, 2020 , pages 445–450, 2020...

2020
[27]

QBF as an Altern ative to Courcelle’s Theorem

Michael Lampis, Stefan Mengel, and Valia Mitsou. QBF as an Altern ative to Courcelle’s Theorem. In Theory and Applications of Satisﬁability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, Flo C 2018, Oxford, UK, Jul...

2018 doi
[28]

Lower bounds based on the Exponential Time Hypothesis

Daniel Lokshtanov, D´ aniel Marx, and Saket Saurabh. Lower bounds based on the Exponential Time Hypothesis. Bull. EATCS , 105:41–72, 2011

2011
[29]

Boolean Lexicographic Op- timization: Algorithms & Applications

Jo˜ ao Marques-Silva, Josep Argelich, Ana Gra¸ ca, and Inˆ es L ynce. Boolean Lexicographic Op- timization: Algorithms & Applications. Ann. Math. Artif. Intell. , 62(3-4):317–343, 2011. doi:10.1007/S10472-011-9233-2

2011 doi
[30]

In Progress in Artiﬁcial Intelligence - 18th EPIA Conference on Artiﬁcial Intelligence, EPIA 2017, Porto, Portugal, Sep tember 5-8, 2017, Proceedings , pages 681–694, 2017

Jo˜ ao Marques-Silva, Alexey Ignatiev, and Ant´ onio Morgado.Horn Maximum Satisﬁability: Reduc- tions, Algorithms and Applications. In Progress in Artiﬁcial Intelligence - 18th EPIA Conference on Artiﬁcial Intelligence, EPIA 2017, Porto, Portugal, Sep tember 5-8, 2017, Proceed...

2017 doi
[31]

Manquinho, and Inˆ es Lynce

Ruben Martins, Vasco M. Manquinho, and Inˆ es Lynce. Open-W BO: A Modular MaxSAT Solver. In Theory and Applications of Satisﬁability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austr ia, July 14-17, 2014. Pr...

2014 doi
[32]

Digital Annealer for High-Speed Solving of Combi- natorial Optimization Problems and its Applications

Satoshi Matsubara, Motomu Takatsu, Toshiyuki Miyazawa, T akayuki Shibasaki, Yasuhiro Watan- abe, Kazuya Takemoto, and Hirotaka Tamura. Digital Annealer for High-Speed Solving of Combi- natorial Optimization Problems and its Applications. In 25th Asia and South Paciﬁc Design Au...

2020
[33]

Mniszewski

Susan M. Mniszewski. Graph Partitioning as Quadratic Unconstr ained Binary Optimization (QUBO) on Spiking Neuromorphic Hardware. In Proceedings of the International Conference on Neuromor- phic Systems, ICONS 2019, Knoxville, Tennessee, USA, July 2 3-25, 2019 , pages 4:1–4:5, ...

2019
[35]

On Optimal QUBO Encoding of Boolean Logic, (Max-)3-SAT and (Max-)k-SAT with Integer Programming

Gregory Morse and Tam´ as Kozsik. On Optimal QUBO Encoding of Boolean Logic, (Max-)3-SAT and (Max-)k-SAT with Integer Programming. In Proceedings of the 7th International Conference on Algorithms, Computing and Systems, ICACS 2023, Larissa, Greece, October 19-21, 2023 , pages ...

2023
[36]

A Survey Examin ing Neuromorphic Architec- ture in Space and Challenges from Radiation

Jonathan Naoukin, Murat Isik, and Karn Tiwari. A Survey Examin ing Neuromorphic Architec- ture in Space and Challenges from Radiation. CoRR, abs/2311.15006, 2023. arXiv:2311.15006, doi:10.48550/ARXIV.2311.15006

2023 doi arXiv
[37]

Algorithmic QUBO Formulations for k-SAT and Hamiltonian Cycles

Jonas N¨ ußlein, Thomas Gabor, Claudia Linnhoﬀ-Popien, and Seb astian Feld. Algorithmic QUBO Formulations for k-SAT and Hamiltonian Cycles. In GECCO ’22: Genetic and Evolutionary Com- putation Conference, Companion Volume, Boston, Massachus etts, USA, July 9 - 13, 2022 , pages...

2022
[38]

Solving (Max) 3-SAT via Quadratic Unconstrained Binary Optimization

Jonas N¨ ußlein, Sebastian Zielinski, Thomas Gabor, Claudia Linnho ﬀ-Popien, and Sebastian Feld. Solving (Max) 3-SAT via Quadratic Unconstrained Binary Optimization . In Computational Science - ICCS 2023 - 23rd International Conference, Prague, Czech R epublic, July 3-5, 2023,...

2023 doi
[39]

Energ y-Eﬃcient On-Board Radio Re- source Management for Satellite Communications via Neuromorphic C omputing

Flor Ortiz, Nicolas Skatchkovsky, Eva Lagunas, Wallace A Martin s, Geoﬀrey Eappen, Saed Daoud, Osvaldo Simeone, Bipin Rajendran, and Symeon Chatzinotas. Energ y-Eﬃcient On-Board Radio Re- source Management for Satellite Communications via Neuromorphic C omputing. IEEE Transact...

2024
[40]

UWrMaxSat: Eﬃcient Solver for MaxSAT and Ps eudo-Boolean Problems

Marek Piotr´ ow. UWrMaxSat: Eﬃcient Solver for MaxSAT and Ps eudo-Boolean Problems. In 32nd IEEE International Conference on Tools with Artiﬁcial Inte lligence, ICTAI 2020, Baltimore, MD, USA, November 9-11, 2020 , pages 132–136, 2020. doi:10.1109/ICTAI50040.2020.00031

2020
[41]

Imple- menting 3-SAT Gadgets for Quantum Annealers with Random Instan ces

Pol Rodr ´ ıguez-Farr´ es, Rocco Ballester, Carlos Ans´ otegui, Jordi Levy, and Jes´ us Cerquides. Imple- menting 3-SAT Gadgets for Quantum Annealers with Random Instan ces. In Computational Science - ICCS 2024 - 24th International Conference, Malaga, Spain, July 2-4, 2024, Pr...

2024 doi
[42]

Max 2-SAT with up to 108 Qubits

Siddhartha Santra, Gregory Quiroz, Greg Ver Steeg, and Dan iel A Lidar. Max 2-SAT with up to 108 Qubits. New Journal of Physics , 16(4):045006, apr 2014. doi:10.1088/1367-2630/16/4/045006

2014 doi
[43]

Schuman, Shruti R

Catherine D. Schuman, Shruti R. Kulkarni, Maryam Parsa, J. P arker Mitchell, Prasanna Date, and Bill Kay. Opportunities for Neuromorphic Computing Algorithms and A pplications. Nat. Comput. Sci., 2(1):10–19, 2022. doi:10.1038/S43588-021-00184-Y . 15

2022 doi
[44]

A Faster Algorithm for P ropositional Model Counting Param- eterized by Incidence Treewidth

Friedrich Slivovsky and Stefan Szeider. A Faster Algorithm for P ropositional Model Counting Param- eterized by Incidence Treewidth. In Luca Pulina and Martina Seidl, ed itors, Theory and Applications of Satisﬁability Testing - SAT 2020 - 23rd International Con ference, Algher...

2020 doi
[45]

Sorkin, Madhu Sudan, and David P

Luca Trevisan, Gregory B. Sorkin, Madhu Sudan, and David P. W illiamson. Gad- gets, Approximation, and Linear Programming. SIAM J. Comput. , 29(6):2074–2097, 2000. doi:10.1137/S0097539797328847

doi
[46]

Quantum Annealing-Based Algorithm for Eﬃcient Coalition Format ion Among LEO Satellites

Supreeth Mysore Venkatesh, Antonio Macaluso, Marlon Nuske , Matthias Klusch, and Andreas Den- gel. Quantum Annealing-Based Algorithm for Eﬃcient Coalition Format ion Among LEO Satellites. CoRR, abs/2408.06007, 2024. arXiv:2408.06007, doi:10.48550/arXiv.2408.06007

2024 doi arXiv
[47]

Ollivier-Ricci Cu rvature and Fast Approxima- tion to Treewidth in Embeddability of QUBO Problems

Chi Wang, Edmond Jonckheere, and Todd Brun. Ollivier-Ricci Cu rvature and Fast Approxima- tion to Treewidth in Embeddability of QUBO Problems. In 2014 6th International Symposium on Communications, Control and Signal Processing (ISCCSP) , pages 598–601. IEEE, 2014

2014
[48]

SATQUBOLIB: A Python Framework for Creating and B enchmarking (Max- )3SAT QUBOs

Sebastian Zielinski, Magdalena Benkard, Jonas N¨ ußlein, Claudia L innhoﬀ-Popien, and Se- bastian Feld. SATQUBOLIB: A Python Framework for Creating and B enchmarking (Max- )3SAT QUBOs. In Innovations for Community Services - 24th International Co nference, I4CS 2024, Maastrich...

2024 doi
[49]

Inﬂuence of Diﬀerent 3SAT-to-QUBO Transformatio ns on the Solution Quality of Quantum Annealing: A Benchmark Study

Sebastian Zielinski, Jonas N¨ ußlein, Jonas Stein, Thomas Gabor, Claudia Linnhoﬀ-Popien, and Se- bastian Feld. Inﬂuence of Diﬀerent 3SAT-to-QUBO Transformatio ns on the Solution Quality of Quantum Annealing: A Benchmark Study. In Companion Proceedings of the Conference on Gene...

2023
[2015]

doi:10.1109/TCAD.2015.2474396. 12

2015
[2019]

doi:10.1007/S11128-019-2236-3

doi

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.

[1] [7]

Structure-Guided Cube-and -Conquer for MaxSAT

Max Bannach and Markus Hecher. Structure-Guided Cube-and -Conquer for MaxSAT. In NASA Formal Methods - 16th International Symposium, NFM 2024, Mo ﬀett Field, CA, USA, June 4-6, 2024, Proceedings, pages 3–20, 2024. doi:10.1007/978-3-031-60698-4_1

work page doi:10.1007/978-3-031-60698-4_1 2024

[2] [1]

Arthur, Paul Merolla, Nabil Imam, Yutaka Y

Filipp Akopyan, Jun Sawada, Andrew Cassidy, Rodrigo Alvarez-Ic aza, John V. Arthur, Paul Merolla, Nabil Imam, Yutaka Y. Nakamura, Pallab Datta, Gi-Joon Nam, Brian T aba, Michael P. Beakes, Bernard Brezzo, Jente B. Kuang, Rajit Manohar, William P. Risk, Bry an L. Jackson, and Dhar- mendra S. Modha. TrueNorth: Design and Tool Flow of a 65 mW 1 Million N eur...

work page

[3] [2]

Quantum Optimization Algo- rithm for LEO Satellite Communications Based on Cell-Free Massive MIM O

Hayder Al-Hraishawi, Junaid ur Rehman, and Symeon Chatzinotas . Quantum Optimization Algo- rithm for LEO Satellite Communications Based on Cell-Free Massive MIM O. In IEEE International Conference on Communications, ICC 2023 - Workshops, Rome, I taly, May 28 - June 1, 2023 , pages 1759–1764, 2023. doi:10.1109/ICCWORKSHOPS57953.2023.10283753

arXiv 2023

[4] [3]

Zahangir Alom, Brian Van Essen, Adam T

Md. Zahangir Alom, Brian Van Essen, Adam T. Moody, David Peter W idemann, and Tarek M. Taha. Quadratic Unconstrained Binary Optimization (QUBO) on Neuromorp hic Computing System. In 2017 International Joint Conference on Neural Networks, IJ CNN 2017, Anchorage, AK, USA, May 14-19, 2017 , pages 3922–3929, 2017. doi:10.1109/IJCNN.2017.7966350

work page arXiv 2017

[5] [4]

Satellite Adaptive Onboard Beamforming Using Neuromorphic Processors

Wallace Alves-Martins, Eva Lagunas, Nicolas Skatchkovsky, Flor de Guadalupe Ortiz Gomez, Ge- oﬀrey Eappen, Osvaldo Simeone, Bipin Rajendran, and Symeon Chat zinotas. Satellite Adaptive Onboard Beamforming Using Neuromorphic Processors. In IEEE International Symposium on Per- sonal, Indoor and Mobile Radio Communications . IEEE, Washington, United States, 2024

work page 2024

[6] [5]

Reducing SAT to Max2SAT

Carlos Ans´ otegui and Jordi Levy. Reducing SAT to Max2SAT. I n Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence , IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021 , pages 1367–1373, 2021. doi:10.24963/IJCAI.2021/189

work page doi:10.24963/ijcai.2021/189 2021

[7] [6]

SAT, Gadgets, Max2XOR, and Quantum Annealers

Carlos Ans´ otegui and Jordi Levy. SAT, Gadgets, Max2XOR, a nd Quantum Annealers. CoRR, abs/2403.00182, 2024. arXiv:2403.00182, doi:10.48550/ARXIV.2403.00182

work page Pith review arXiv doi:10.48550/arxiv.2403.00182 2024

[8] [8]

Chudak, William G

Zhengbing Bian, Fabi´ an A. Chudak, William G. Macready, Aidan Roy, Roberto Sebastiani, and Stefano Varotti. Solving SAT and MaxSAT with a Quantum Anneale r: Foundations and a Preliminary Report. In Frontiers of Combining Systems - 11th International Sympo- sium, FroCoS 2017, Bras´ ılia, Brazil, September 27-29, 201 7, Proceedings, pages 153–171, 2017. do...

work page doi:10.1007/978-3-319-66167-4_9 2017