{"id":"e71e7868-7ac9-4e94-98a8-f174ac12f0b1","arxiv_id":"2412.10289","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"MaxSAT, Max2SAT, and QUBO are mutually reducible in linear time with treewidth preserved up to small constants, giving ETH- and SETH-tight bounds and a 2^treewidth algorithm for QUBO.","lead":"This paper proves that MaxSAT, Max2SAT, and the QUBO problem behind quantum annealers and neuromorphic chips are equivalent under linear-time reductions that nearly preserve treewidth. This yields new tight complexity bounds for QUBO and Max2SAT, including a time-optimal fixed-parameter algorithm for QUBO.","discovery_kind":"unification","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 3's Eq. (3) is false as stated: a valid rooted TD for a single hard clause can make the output unsatisfiable; the incidence-treewidth chain lacks a necessary witness-bag condition.","rationale":"The reader's weakest assumption named Lemma 3 and the rooting of the tree decomposition; I agree and sharpen it to a concrete counterexample. The condition in Eq. (3) excluding literals that occur in child bags is not merely hard to prove; as stated it is false. A parent bag {c,x} with child {x} is a valid tree decomposition of the incidence graph of the hard unit clause, yet the reason clause at the root becomes vacuously impossible while the hard unit c_root demands truth. Since Lemma 3 feeds Theorem 1 item 2, the O(3*itw) reductions and the resulting SETH/ETH lower bounds for max2sat and QUBO under incidence treewidth lose their support. The primal-treewidth results (Theorem 1 item 1), the 2^tw QUBO algorithm, Lemma 8/Theorem 2, and the #SAT-based Theorem 3 may remain defensible, so I am not rejecting the entire research program. But the manuscript's central claim of incidence-treewidth equivalence is not established: a corrected lemma would need either to remove or modify the child-exclusion while still bounding clause sizes, or to state and prove a normalization/rooting rule guaranteeing a witness bag for every satisfied literal. Because the counterexample is small and the missing condition is structural, the appropriate verdict for the current version is REJECT rather than CONDITIONAL: the stated Lemma 3 cannot stand as written.","tokens_in":18380,"tokens_out":25188,"duration_ms":736092,"concrete_test":"Implement Lemma 3 literally on phi = {(x)^infinity} with the rooted TD: root bag {c,x}, unique child {x}, and check satisfiability of the output w3cnf. The output should be unsatisfiable (hard clause c_root and Eq. (3) gives c_root -> false), while cost(phi)=0, refuting Lemma 3. As a control, re-run with the same tree rooted at {x} so that {c,x} is the child; if the output becomes satisfiable, the failure is exactly the missing rooting/bag-choice condition. This single instance isolates the issue: deriving c_root -> false and c_root from the encoding is a two-line resolution, so no SAT solver is required.","verdict_should_be":"REJECT","load_bearing_attack":"Lemma 3 is the load-bearing step for the incidence-treewidth half of Theorem 1 and for Corollaries 2-3. Its Eq. (3) allows c_t to be explained by a literal only when that literal's variable is in chi(t) and absent from every child bag of t. The proof of cost-preservation must therefore find, for every satisfied clause c and chosen true literal l, a bag t with {c, |l|} in chi(t) and |l| absent from all children of t. The lemma never proves this, and the claim is not true for arbitrary rooted tree decompositions. Counterexample: let phi = {(x)^infinity} and take the valid width-1 TD of I_phi consisting of root bag {c,x} with one child {x}. The encoding of Lemma 3 produces the hard unit (c_root)^infinity plus sync clauses and Eq. (3) at the root. Since x occurs in the only child and no child contains c, Eq. (3) becomes c_root -> false. Hence the output is unsatisfiable, while cost(phi)=0. Re-rooting at {x} removes the problem, so the lemma silently depends on a rooting or normalization condition that is neither stated nor proved. The same obstruction arises whenever a clause's true literals are all introduced in child subtrees that do not contain the clause; no witness bag exists.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":18559,"tokens_out":12878,"duration_ms":136319,"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":[{"comment":"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":"Section 3.1, Lemma 3"},{"comment":"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":"Section 3.2, Lemma 5"},{"comment":"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.","section":"Section 3.1, Lemma 3 (treewidth argument)"}],"minor_comments":[{"comment":"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":"Section 5, Lemma 9"},{"comment":"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":"Section 4, Lemma 8"},{"comment":"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.","section":"Section 5, Lemma 13"},{"comment":"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.","section":"Throughout"}],"recommendation":"major_revision","confidential_remarks":"The paper's core idea is attractive and the primal-treewidth results, the model-counting reductions, and Theorem 2 appear substantially correct. The decisive issue is the correctness of Lemma 3, which is load-bearing for the incidence-treewidth equivalence and the associated lower bounds. The counterexample with a single hard unit clause is simple and conclusive, so this is not a matter of presentation. If the authors can repair Lemma 3 — perhaps by adopting a normal form for the supplied tree decomposition or by adjusting the reason-clause construction — the paper may be publishable after the necessary revisions. The self-citation [7] is not load-bearing and does not raise a concern."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","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.\n\nSecond, 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.\n\nThis 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.\n\nWho 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.","headline":"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.","tokens_in":787,"tokens_out":794,"would_cite":true,"duration_ms":136702,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q17","68Q25","68Q27","05C85"],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["MaxSAT","Max2SAT","QUBO","treewidth","incidence treewidth","fixed-parameter algorithms","ETH and SETH","model counting"],"falsifier":"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.","tokens_in":18101,"feed_emoji":"🔄","tokens_out":14485,"duration_ms":139194,"temperature":0.7,"pith_summary":"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.","feed_headline":"MaxSAT and QUBO interconvert with structure nearly intact","feed_subtitle":"Small-treewidth instances stay small when mapped to quantum and neuromorphic hardware.","key_machinery":"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$.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Establishes that Max2SAT is NP-hard, the classical reduction target and the starting point for the encoding chain.","marker":"[20]"},{"why":"Supplies the correctness lemma for Rule 5, the gadget that turns a 3-clause into six 2-clauses while preserving cost and top-value handling.","marker":"[5]"},{"why":"Provides the earlier structural clause-splitting result that Lemma 3 improves, setting the baseline for incidence-treewidth-aware encodings.","marker":"[27]"},{"why":"Gives the standard normalization of tree decompositions used to keep the reason clauses of Lemma 3 ternary.","marker":"[17]"},{"why":"Provides the refined dynamic programming over tree decompositions that yields the Fact 1 upper bounds the paper builds on.","marker":"[9]"},{"why":"Gives the $O(2^{\\mathrm{itw}}|\\phi|)$ #SAT algorithm that the Theorem 3 reductions call as a subroutine.","marker":"[44]"},{"why":"Provides the almost-simplicial contraction rule used to show clause vertices in binary formulas do not increase treewidth, giving tw <= itw for Max2SAT.","marker":"[10]"},{"why":"Survey used to state the exponential-time hypotheses and their lower-bound consequences.","marker":"[28]"}],"fun_headline_variants":["Treewidth survives: MaxSAT to QUBO in linear time","MaxSAT and QUBO share treewidth-bounded reductions","Tight lower bounds for MaxSAT from structure-aware maps","Small constants: MaxSAT and QUBO share treewidth bounds"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Treewidth survives: MaxSAT to QUBO in linear time","MaxSAT and QUBO share treewidth-bounded reductions","Tight lower bounds for MaxSAT from structure-aware maps","Small constants: MaxSAT and QUBO share treewidth bounds"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001143,"raw_usage":{"total_tokens":4802,"prompt_tokens":1063,"completion_tokens":3739,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":679,"completion_tokens_details":{"reasoning_tokens":3676}},"tokens_in":679,"tokens_out":3739,"duration_ms":29766,"temperature":1.0,"reasoning_tokens":3676,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T16:02:25.750087+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Reducing SAT to Max2SAT","cited_arxiv_id":null,"evidence_quote":"Supplies the correctness lemma for Rule 5, the gadget that turns a 3-clause into six 2-clauses while preserving cost and top-value handling."},{"cited_title":"QBF as an Altern ative to Courcelle’s Theorem","cited_arxiv_id":null,"evidence_quote":"Provides the earlier structural clause-splitting result that Lemma 3 improves, setting the baseline for incidence-treewidth-aware encodings."},{"cited_title":"Bodlaender, Paul S","cited_arxiv_id":null,"evidence_quote":"Provides the refined dynamic programming over tree decompositions that yields the Fact 1 upper bounds the paper builds on."},{"cited_title":"A Faster Algorithm for P ropositional Model Counting Param- eterized by Incidence Treewidth","cited_arxiv_id":null,"evidence_quote":"Gives the $O(2^{\\mathrm{itw}}|\\phi|)$ #SAT algorithm that the Theorem 3 reductions call as a subroutine."},{"cited_title":"Bodlaender, Arie M","cited_arxiv_id":null,"evidence_quote":"Provides the almost-simplicial contraction rule used to show clause vertices in binary formulas do not increase treewidth, giving tw <= itw for Max2SAT."},{"cited_title":"Lower bounds based on the Exponential Time Hypothesis","cited_arxiv_id":null,"evidence_quote":"Survey used to state the exponential-time hypotheses and their lower-bound consequences."}],"review_version":1}