{"id":"b7df0a51-538f-4737-9bc9-9b8fd3792053","arxiv_id":"2506.00674","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"A penalty-based unconstrained continuous formulation of hybrid SAT preserves the satisfiability reduction, and penalty terms can be omitted exactly for constraints like OR, XOR, and NAE, which are called rounding-friendly.","lead":"The paper replaces box-constrained SAT formulations with unconstrained continuous objectives, adding penalty terms to keep solutions Boolean. It then shows which hybrid constraint types can drop these penalties and reports that unconstrained optimizers such as Adam solve more random 3-CNF instances than the constrained baseline.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The empirical 'hybrid' claim rests on single-type random benchmarks with no CDCL or hybrid-solver baseline, so the advertised practical benefit is not established.","rationale":"The paper's theoretical core is sound: Proposition 9 is a direct sum-of-squares equivalence where the penalty term forces Boolean coordinates, and the rounding-friendly classification in Proposition 14 is a genuine conceptual contribution. However, the advertised practical benefit is the empirical headline, and the experiments do not test it: every benchmark family in Section 6.1 is single-constraint-type, and the solver comparison in RQ3 is internal to continuous optimizers within FourierSAT. The reader's weakest assumption correctly identifies this gap, and the conditional verdict is appropriate. Additional secondary issues that also support conditioning include: alpha is tuned on the same benchmark families used for later comparisons (RQ1), and Proposition 18's epsilon constants have a zero-coordinate boundary issue (e.g., an XOR constraint with l=(0,1,...,1) has |FE|=1/2 but sgn(l) violates the constraint under the paper's sgn convention), which affects Corollary 19's MaxSAT bounds though not the 0-rounding-friendly penalty-omission result. The proposed mixed-benchmark experiment would settle the main concern: if it passes, the paper's practical claim is strengthened; if not, the theoretical contribution stands alone and the empirical claims need severe qualification.","tokens_in":13661,"tokens_out":14106,"duration_ms":142159,"concrete_test":"Build mixed random formulas with n=200: 3-CNF clauses at m/n about 2.5 plus p in {0.1, 0.3} fraction of XOR clauses and q in {0.05, 0.1} fraction of random cardinality constraints. Run the paper's Adam-square formulation with alpha tuned on a separate set of mixed formulas, and compare against constrained FourierSAT and Kissat/CryptoMiniSat under the same 300-second limit. If Adam-square does not beat the best baseline on mixed formulas, or if alpha tuned on single-type benchmarks fails to transfer to mixed formulas, the advertised hybrid enhancement is unsupported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 6.1's benchmarks are homogeneous: random 3-CNF, random 2-XOR, and random cardinality formulas each contain only one constraint type. No formula mixes OR, XOR, NAE, or cardinality constraints, despite the abstract and conclusion claiming 'hybrid benchmarks' and 'hybrid SAT solving.' RQ3 compares only against other continuous optimizers (SLSQP, GD, HJ-PROX) inside the FourierSAT codebase; there is no comparison with CDCL solvers such as Kissat/MiniSat or with native hybrid solvers such as CryptoMiniSat. Therefore the central empirical claim — that unconstrained optimizers enhance hybrid SAT solving — requires an extrapolation from single-type random ensembles to mixed workloads, which is exactly the regime the title advertises. The soundness theory can be correct while the practical claim fails if constraint-type interactions change optimizer behavior, for example by making the penalty term for cardinality constraints interfere with the rounding-friendly behavior of XOR or OR clauses.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes to solve hybrid SAT formulas by minimizing unconstrained continuous relaxations of Fourier expansions of constraints. It introduces square and absolute-value formulations with box-domain penalty terms and proves soundness (Propositions 9 and 11). It then studies when penalty terms can be omitted: constraints are called ϵ-rounding-friendly if small absolute Fourier values force the sign-rounded vector to satisfy the constraint. The paper proves XOR, OR, and NAE are rounding-friendly and cardinality/pseudo-Boolean constraints are not, and bounds the number of violated constraints via a MaxSAT-style guarantee (Corollary 19). Empirically, the authors integrate unconstrained GD, SLSQP, Adam, and HJ-PROX into the FourierSAT codebase and report that the square formulation, unconstrained domains, and a nonzero penalty for cardinality help, and that Adam extends the solvable clause-to-variable range on random 3-CNF.","tokens_in":13879,"tokens_out":18171,"duration_ms":171341,"significance":"If the theoretical results were fully correct, the classification of rounding-friendly constraints and the unconstrained reduction would be a useful contribution to continuous-optimization approaches to SAT, giving solver designers a principled criterion for adding box penalties. The soundness reduction itself is direct and correct, and the paper honestly contrasts its approach with FourierSAT's box constraints. The empirical portfolio is broad (GD, SLSQP, Adam, HJ-PROX), and the observation that Adam improves performance on random 3-CNF is potentially interesting. However, the current manuscript has a false statement in Proposition 18, a flawed proof of Theorem 16, and an empirical evaluation that does not actually test hybrid formulas, so the advertised conclusions require substantial repair.","major_comments":[{"comment":"Definition 12 defines ϵ-rounding-friendly with the non-strict condition |FE_c(l)| ≤ ϵ, but Proposition 18's constants are false under that definition. For an OR clause of length k, FE_OR(0,...,0) = ∏_{i=1}^k (1+0)/2 = 1/2^k, so |FE| equals the claimed threshold; however sgn(0,...,0) = (1,...,1) is the all-false assignment and does not satisfy the clause. The proof in Appendix B.2 actually uses the strict inequality '< 1/2^k', and the same boundary failure occurs for NAE at l=(0,...,0) (FE=1/2^{k-1}) and for XOR at l=(0,...,0) (FE=1/2). The theorem and Corollary 19 must be restated with strict inequalities (e.g., OR is ϵ-rounding-friendly for every ϵ < 1/2^k) or with an explicit exclusion of the boundary point.","section":"Definition 12 / Proposition 18 / Corollary 19"},{"comment":"The proof's central algebraic step is not justified. After defining the partial-assignment chain, the paper asserts 'FE_{c_{k-1}} = (x_k+1)·g(x_{k+1},...,x_n)+1'. Under the paper's 0/1 false-indicator encoding, the Fourier expansion of a constraint of the form ¬x_k ∧ h is not of this form. For the simple constraint c = x1∧x2 with the common prefix b=(False), the expansion is FE_c = 3/4 + x1/4 + x2/4 - x1x2/4, which cannot be written as (x1+1)g(x2)+1. In addition, the 'without loss of generality, we assume b_k=True' does not cover the case b_k=False, which is the only case that occurs for c=x1∧x2. Since Theorem 16 is the necessary-condition half of the classification, the appendix needs a correct proof or a reference to one.","section":"Appendix B.1, proof of Theorem 16"},{"comment":"The empirical section does not evaluate hybrid instances. Each benchmark family is homogeneous: random 3-CNF, random 2-XOR, and random cardinality formulas are generated separately, and no formula mixes OR, XOR, NAE, or cardinality constraints. RQ3's portfolio comparison is also internal to the FourierSAT continuous-optimization codebase; there is no comparison with CDCL solvers (e.g., Kissat, MiniSat) or native hybrid solvers (e.g., CryptoMiniSat). Consequently, the conclusion that unconstrained optimizers 'can enhance hybrid SAT solving' extrapolates from single-type random ensembles to mixed workloads, which is precisely the regime advertised by the title. Either the claims should be narrowed to single-constraint-type continuous optimization, or the evaluation should include mixed-constraint benchmarks and a standard SAT/hybrid baseline.","section":"Section 6.1 and 6.2.3"},{"comment":"Corollary 13 uses 'min' for the α=0 objective, but Fsq_{C,0} is not coercive and the paper does not prove that the infimum is attained when the formula is unsatisfiable. If the infimum is 0 without being attained, the 'iff' statement is ill-posed. The reduction should be stated with the infimum, or attainment should be proved for the constraint classes considered.","section":"Corollary 13 / Section 3.2"}],"minor_comments":[{"comment":"There is a typo in the text: 'pseodu-Boolean' should be 'pseudo-Boolean'.","section":"Section 4"},{"comment":"The Fourier expansion of XOR is written as '(1−∏ x_i)/2', but Table 1 and Proposition 14 use '(1+∏ x_i)/2'. The subsequent inequality also appears reversed under the displayed formula; the proof should be reconciled with the table.","section":"Appendix B.2, proof of Proposition 18 (XOR case)"},{"comment":"The penalty coefficient α and the 'best formulation' per solver are selected after seeing benchmark results on the same data on which the gains are reported; a holdout set or a sensitivity analysis would strengthen the empirical claims.","section":"Section 6.2"},{"comment":"The statement that the unconstrained reduction 'does not extend to MaxSAT problems' is asserted without proof or illustration; a brief counterexample or reference would help the reader calibrate the scope of the soundness results.","section":"Section 3.2"}],"recommendation":"major_revision","confidential_remarks":"The paper has a solid core idea but is not yet in publishable form. The Proposition 18 boundary issue is a one-line fix, but the proof of Theorem 16 needs a genuine mathematical correction rather than a cosmetic edit. The empirical claim of hybrid solving is overreaching relative to the single-type benchmarks, and the paper would benefit from either mixed-constraint experiments with a standard baseline or a narrower statement of the practical contribution."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know: this paper has a genuinely useful theoretical core and an empirical wrapper that overclaims what it shows. The rounding-friendly notion (Definition 12) and the proof that isolated violations are necessary (Theorem 16) are the real contributions. That’s a clean, organizing way to think about when you can drop box constraints in Fourier-style SAT reductions. Propositions 9 and 11 are proved directly and correctly, and the reduction is sound. The epsilon bounds in Proposition 18 are off at a boundary case (equality at l = (0,...,0) doesn't round to a satisfying assignment), but that's a trivial fix to the statement.\n\nThe bigger problem is the gap between the title and the evidence. The paper advertises 'hybrid SAT solving,' but every benchmark is single-constraint-type: random 3-CNF, random 2-XOR, and random cardinality formulas, with no mix of constraint types. There's also no comparison against CDCL solvers like Kissat or MiniSat, nor against a native hybrid solver like CryptoMiniSat. So the claim that unconstrained optimizers enhance hybrid SAT solving is actually supported only for uniform random single-type formulas. The alpha tuning on the same benchmarks used for evaluation is a mild selection-on-data issue, though it doesn't affect the soundness theory.\n\nWho's this for? Researchers already working on continuous optimization for SAT, especially anyone building on FourierSAT or GradSAT. Sections 3 and 4 deserve careful reading; the experiments are a proof-of-concept, not a benchmark study.\n\nMy recommendation: send it to a serious venue with a request for revisions. Add at least one genuinely mixed-constraint benchmark family, include a CDCL or hybrid-solver baseline, and fix the epsilon boundary statements. The theory is solid enough that it deserves referee time, but the empirical claims need to be reined in.","headline":"Solid theory, modest experiments: the rounding-friendly classification is the real contribution; the hybrid-SAT empirical claim is oversold.","tokens_in":14367,"tokens_out":1669,"would_cite":true,"duration_ms":17887,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper proves that hybrid Boolean satisfiability can be decided by unconstrained continuous optimization: for any α>0, a formula is satisfiable exactly when the global minimum of the squared Fourier-expansion objective is zero, and…","keywords":["SAT solving","hybrid constraints","continuous optimization","Walsh-Fourier expansion","unconstrained penalty","rounding-friendly","cardinality constraints","pseudo-Boolean constraints"],"falsifier":"Run the proposed unconstrained square formulation, with the recommended penalty for cardinality constraints and $\\alpha=0$ for XOR/OR/NAE, on a satisfiable formula that mixes all three constraint types in one instance, and compare solve times against a CDCL solver using a standard CNF encoding. If the optimizer fails to find a satisfying assignment within the 300-second limit while the CDCL solver succeeds on a substantial fraction of the instances, the paper's practical enhancement claim would be refuted on that representative workload.","tokens_in":13469,"feed_emoji":"🧮","tokens_out":10312,"duration_ms":91231,"temperature":0.7,"pith_summary":"The paper aims to show that hybrid SAT formulas—conjunctions of XOR, cardinality, Not-All-Equal, and OR constraints—can be solved by unconstrained continuous optimization, extending the earlier box-constrained FourierSAT approach. Its main theoretical result is that the squared Fourier expansions of the constraints plus a quadratic penalty toward ±1 give a sound reduction: a formula is satisfiable exactly when this objective's global minimum over R^n is zero, and any minimizer rounded by sign is a satisfying assignment. It further proves that the penalty is unnecessary for XOR, OR, and NAE constraints because they are 'rounding-friendly', while cardinality and pseudo-Boolean constraints require it. The paper reports that unconstrained optimizers, especially Adam, outperform the constrained versions on the tested random CNF, XOR, and cardinality benchmarks, suggesting this formulation can harness machine-learning optimization techniques for SAT.","feed_headline":"Penalty provably removable for XOR, OR, NAE in SAT","feed_subtitle":"Unconstrained optimizers like Adam can then handle XOR, cardinality, and NAE constraints more quickly.","key_machinery":"The machinery is the square formulation $F^\\mathrm{sq}_{C,\\alpha}(x)$ constructed from Walsh-Fourier expansions of constraints, together with the sign function $\\mathrm{sgn}$ as the rounding map and the notion of an $\\epsilon$-rounding-friendly constraint, which characterizes when the penalty term can be dropped. The Fourier expansion converts each Boolean constraint into a multilinear polynomial whose zero set over the discrete cube is exactly the set of satisfying assignments; squaring makes the objective nonnegative, and the penalty $\\alpha\\sum_i(x_i^2-1)^2$ forces minimizers to the cube corners. The classification theorem (Proposition 14) and the isolated-violations necessary condition (Theorem 16) are what let the paper say when the penalty is actually needed.","core_discovery":"The paper's central claim is a soundness theorem for an unconstrained reduction. Define the square formulation $F^\\mathrm{sq}_{C,\\alpha}(x) = \\sum_{c\\in C} \\mathrm{FE}_c(x)^2 + \\alpha \\sum_{i=1}^n (x_i^2-1)^2$, where $\\mathrm{FE}_c$ is the Walsh-Fourier expansion of constraint $c$ taking value 0 when satisfied and 1 when violated. Proposition 9 states that for any $\\alpha>0$, a hybrid formula $f$ with constraint set $C$ is satisfiable iff $\\min_{x\\in\\mathbb{R}^n} F^\\mathrm{sq}_{C,\\alpha}(x)=0$, and if the minimum is attained at $l$, then $\\mathrm{sgn}(l)$ satisfies $f$. Proposition 14 sharpens this: XOR, OR clauses, and NAE are 0-rounding-friendly, meaning the penalty can be omitted for them (Corollary 13) without losing this equivalence, whereas cardinality and pseudo-Boolean constraints are not rounding-friendly for any $\\epsilon\\ge 0$ and thus require the penalty. The paper also proves that being rounding-friendly implies having only isolated violations (Theorem 16), though the converse fails (Example 17), and gives explicit $\\epsilon$-rounding-friendly constants that yield violation-count bounds via Corollary 19.","pith_inferences":["The paper tests only pure constraint families; a natural next step is to evaluate the formulation on formulas that actually mix XOR, cardinality, and CNF constraints, since the title's 'hybrid' promise is otherwise unverified.","The rounding-friendly criterion could guide constraint design: if engineers can encode a constraint in a form with isolated violations and rounding-friendly Fourier coefficients, they might remove penalty terms and speed up optimization.","Because the unconstrained reduction is polynomial-based, it may combine naturally with GPU acceleration and learned optimizers, but the paper does not demonstrate scaling beyond 1000 variables.","The authors note the reduction does not extend to MaxSAT; for counting or optimization variants, a separate treatment would be needed, suggesting a boundary on the approach's scope."],"forward_implications":["Any zero of $F^\\mathrm{sq}_{C,\\alpha}$ with $\\alpha>0$ gives a satisfying assignment by sign-rounding, so satisfying assignments are certifiable from continuous optima.","For XOR, OR, and NAE formulas, the penalty can be set to zero without sacrificing soundness, giving a smoother objective that unconstrained optimizers can handle directly.","Corollary 19 turns objective values into violation-count certificates: small $F^\\mathrm{sq}_{C,0}(l)$ implies that $\\mathrm{sgn}(l)$ violates few constraints, which is useful for MaxSAT-style approximations.","Allowing unconstrained optimizers such as Adam broadens the solver portfolio and, per the reported experiments, improves the virtual best solver on random 3-CNF, 2-XOR, and cardinality benchmarks."],"supporting_citations":[{"why":"Provides the constrained box-constrained formulation and polynomial encoding of hybrid constraints that this work extends to the unconstrained setting.","marker":"[31]"},{"why":"Establishes the Walsh-Fourier expansion theorem used to represent every Boolean constraint as a multilinear polynomial.","marker":"[41]"},{"why":"Shows an unconstrained formulation for CNF formulas without penalty, posing the question of when penalties are necessary.","marker":"[19]"},{"why":"Supplies the O(k^2) gradient computation routines for CNF, XOR, NAE, and cardinality constraints used in the implementation.","marker":"[32]"},{"why":"Adam is the unconstrained optimizer whose improved performance on random 3-CNF is a central empirical result.","marker":"[29]"}],"fun_headline_variants":["Unconstrained hybrid SAT: penalty-free for XOR, OR, NAE","Hybrid SAT theorem: rounding-friendly constraints need no penalty","Box-free SAT: only cardinality and pseudo-Boolean require penalty","Adam-optimized hybrid SAT drops penalty for key constraint classes"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The empirical claim that unconstrained optimizers improve hybrid SAT solving is supported only on pure random 3-CNF, pure random 2-XOR, and pure random cardinality benchmarks; if those do not represent the mixed constraint workloads that appear in practice, the practical benefit may not transfer, even though the theoretical reduction remains valid.","fun_headline_variants_meta":{"raw":{"variants":["Unconstrained hybrid SAT: penalty-free for XOR, OR, NAE","Hybrid SAT theorem: rounding-friendly constraints need no penalty","Box-free SAT: only cardinality and pseudo-Boolean require penalty","Adam-optimized hybrid SAT drops penalty for key constraint classes"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000414,"raw_usage":{"total_tokens":2159,"prompt_tokens":985,"completion_tokens":1174,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":601,"completion_tokens_details":{"reasoning_tokens":1101}},"tokens_in":601,"tokens_out":1174,"duration_ms":11508,"temperature":1.0,"reasoning_tokens":1101,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T12:00:28.328730+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the proposed unconstrained square formulation, with the recommended penalty for cardinality constraints and $\\alpha=0$ for XOR/OR/NAE, on a satisfiable formula that mixes all three constraint types in one instance, and compare solve times against a CDCL solver using a standard CNF encoding. If the optimizer fails to find a satisfying assignment within the 300-second limit while the CDCL solver succeeds on a substantial fraction of the instances, the paper's practical enhancement claim would be refuted on that representative workload.","supporting_citations":[],"review_version":1}