at each N, then fit Eq. (3) only to N values where the total observed successes across all 250 instances is >= 10 (and similarly >= 10 within the hardest-quintile subset). Report b with confidence intervals for DOCSAT and WalkSAT, and also report fits excluding the largest-N data points. If the WalkSAT b changes by more than a factor of 2 from 2e-3, or if its confidence interval overlaps DOCSAT's, the claimed order-of-magnitude advantage is not established.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central quantitative claim is the exponential fit in Eq. (3) and Fig. 5: b ~ 3e-4 for DOCSAT versus b ~ 2e-3 for the best WalkSAT variant (pwalk=0.57). These b values are extracted from the ensemble-averaged success probability per run,
, over 250 instances with 1000 trials each per N. For WalkSAT, b ~ 2e-3 implies p ~ (1.002)^{-N}: at N=5000, p ~ 4.5e-5 and the expected total number of successes across the entire sample is ~11; at N=6000, p ~ 6e-6 and the expectation is ~1.5. The measured
at large N is therefore dominated by zero-success instances and a handful of rare successes, so the sample average has enormous relative error, and any exponential fit to log(
) versus N is highly sensitive to how zeros are handled and to Poisson fluctuations. The dashed hardest-quintile curves are even more fragile: at large N most instances have zero successes, so the 'hardest 50 instances' are effectively a random tie-break among uninformative zeros, and the quoted b ~ 3e-2 for WalkSAT's hard quintile is based on extremely few events. The paper reports no confidence intervals for b, no fitting range, and no count of nonzero-success instances per N. Since the headline 'drastically outperforms' is precisely the order-of-magnitude gap in b, this unresolved statistical fragility is the most load-bearing concern; it is not addressed by the TLC-desert mechanism, which motivates the heuristic but does not determine the measured success probabilities.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces DOCSAT, a stochastic local search (SLS) heuristic for 3-SAT that extends WalkSAT by adding a 'dissipate oversatisfied constraints' (DOC) term to the variable-selection score. The DOC term penalizes increases in the total number of true literals (TLC), based on the observation that for hard Weigt-protocol instances at critical clause density, low-energy local minima have substantially higher TLC than true solutions. The authors benchmark DOCSAT against WalkSAT, YalSAT, and Kissat on 250 Weigt-protocol instances per size for N from 100 to 15000, reporting a higher fraction of solved instances and a much slower exponential decay of the ensemble-averaged success probability
~ (1+b)^{-N}, with b ≈ 3e-4 for DOCSAT versus b ≈ 2e-3 for the best WalkSAT on the full sample. They also report an advantage on the hardest quintile of instances and present critical-clause statistics supporting the claimed mechanism.","tokens_in":10921,"tokens_out":6051,"duration_ms":70205,"significance":"If the reported scaling advantage is real, DOCSAT is a substantial advance for a notoriously hard random 3-SAT regime, and the TLC-based heuristic is a novel, potentially transferable idea for escaping local minima in SLS. The paper's strengths are direct empirical benchmarking on a well-defined instance distribution, a clear algorithmic description, and a falsifiable scaling claim. However, the headline quantitative claim rests on exponential fits to success probabilities that are statistically unresolved at large N, the DOCSAT parameters are not justified or swept, the benchmark family is restricted to one protocol, and no code or wall-time comparisons are provided. These gaps currently prevent independent verification and limit the generality of the 'drastically outperforms' conclusion.","major_comments":[{"comment":"The central order-of-magnitude gap in the scaling exponent b is not statistically supported as reported. With b ≈ 2e-3 for WalkSAT(0.57), the expected number of successes across the entire sample (250 instances × 1000 trials) is roughly 11 at N=5000 and 1.5 at N=6000; at larger N virtually all instances contribute zero successes, so the sample average
and its logarithm are dominated by a handful of rare events and by how zero-success instances are handled. The paper does not report the number of instances with at least one success, the fitting range, or confidence intervals for b. Please provide per-N counts of successful trials and nonzero-success instances, fit b with a maximum-likelihood method on the raw counts (or explicitly state the zero-handling rule), and report uncertainty intervals. Without this, the gap between b ≈ 3e-4 and b ≈ 2e-3 cannot be regarded as established.","section":"IV, Fig. 5, Eq. (3)"},{"comment":"The stated formula for the TLC change under a flip has the wrong sign. For a current assignment x_k, flipping the variable changes the TLC by (p - n)_k · (1 - 2x_k); the displayed (p - n)_k · (2x_k - 1) is the negative of that. Since Algorithm 1 minimizes the score b + rdoc · T, the written formula would select flips that increase TLC, contradicting the DOC principle and the behavior shown in Fig. 6. Please correct the sign, clarify whether the implemented heuristic uses the corrected expression, and re-verify the illustrative values in Fig. 3 accordingly.","section":"III, Eq. (1)"},{"comment":"The DOCSAT parameters pwalk = 0.4 and rdoc = 0.15 are introduced without a tuning protocol or sensitivity analysis. WalkSAT's noise parameter is justified by prior literature, but for DOCSAT it is not demonstrated that these values were not selected on the same benchmark instances that later serve as evidence of superiority. Please provide a parameter sweep (e.g., rdoc in {0, 0.05, 0.1, 0.15, 0.2} and pwalk in {0.3, 0.4, 0.5, 0.57}) or a principled a priori choice, ideally tuned on a separate training set, so that the comparison with WalkSAT is fair.","section":"IV, Algorithm 1 and parameter choice"},{"comment":"The TLC-desert mechanism is observed on 29 hard instances at N=200 (Fig. 2) and assumed to hold at the much larger N used in Section IV, while the entire benchmark suite is drawn from the Weigt protocol at α = 4.27. The claim that DOCSAT 'drastically outperforms existing solvers' should be restricted to this distribution, and the extrapolation to larger N should be supported by at least one intermediate check of the TLC gap (e.g., N=1000 or N=5000). Transferability to other hard 3-SAT families (uniform random clauses at the threshold, or structured industrial instances) is currently unsubstantiated and should be stated as future work rather than implied.","section":"II and IV, generality"},{"comment":"The comparison with Kissat uses a decision-count cutoff rather than wall-clock time, while the SLS solvers receive 1000 restarts with up to 300N flips each; without wall-time measurements or a per-trial time model, the practical claim of outperforming a complete solver is not demonstrated. Additionally, the manuscript provides no code, no random-seed specification, and no detailed description of the trial generation (beyond citing the Weigt protocol), which prevents independent reproduction of the reported numbers. Please make the implementation available or provide enough detail (including the exact clause-generation procedure and the handling of restarts) and add wall-time comparisons for the main benchmark sizes.","section":"Appendix A and reproducibility"}],"minor_comments":[{"comment":"Several typos appear in section headings and text: 'CA VEA TS' (Section II), 'OVERSATISFIED' (Section III), and 'oversatisified' in Section IV; these should be corrected.","section":"General typography"},{"comment":"The caption states that pwalk = 0.4 and rdoc = 0.15 are fixed for DOCSAT, but the legend reads 'WalkSAT(0.57)' etc.; please clarify that the values in parentheses refer to pwalk and that DOCSAT uses the stated fixed values.","section":"Fig. 1 caption"},{"comment":"When many instances have zero successes, the standard deviation of the mean is not an informative error measure; please show success counts or use binomial confidence intervals, and state how zero-success instances are included in
.","section":"Fig. 5 and error bars"},{"comment":"The text says the fit supports 'asymptotically exponential runtime', but the fit is to ensemble-averaged success probability, not runtime; please rephrase to avoid conflating
with expected runtime (which scales as 1/
only under additional assumptions).","section":"Eq. (3)"},{"comment":"The main text should state the number of instances per N (currently only in the Fig. 1 caption) and the exact meaning of 'solved' (a trial with E=0 within 300N flips, or the instance solved by at least one trial) to avoid ambiguity.","section":"Benchmark details"},{"comment":"Reference [32] cites 'Walksat project – version 57' without a URL or archive identifier; please provide a persistent link or repository DOI.","section":"Reference [32]"}],"recommendation":"major_revision","confidential_remarks":"The statistical fragility of the scaling fits is the main technical barrier: the headline b-values may be an artifact of unresolved small counts at large N, and the required fix (reporting raw success counts, fitting ranges, and confidence intervals) is straightforward but essential. The sign error in Eq. (1) is also serious because it makes the written algorithm inconsistent with the described mechanism, though it is likely a typo. The absence of code and the narrow benchmark family further reduce confidence in the 'drastically outperforms' claim. If the authors can provide the missing statistical support and a code release, the paper could be a solid contribution; in its current form I cannot recommend acceptance."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe paper introduces DOCSAT, a small modification to WalkSAT that adds a term to the variable-selection score to nudge the search toward fewer true literals (critical clauses rather than oversatisfied ones). The key observation is a true-literal-count (TLC) desert: on hard Weigt-protocol instances at N=200, the low-energy states found by WalkSAT have significantly higher TLC than the actual solutions. That is a clean, testable observation, and the paper does a nice job connecting it to the failure mode of WalkSAT.\n\nWhat's genuinely new is the DOC principle: treating the number of true literals as a secondary quantity to dissipate, rather than the make/break counts used in YalSAT or GWSAT. The authors show that on their benchmark, DOCSAT solves instances that WalkSAT and Kissat cannot, and they verify the mechanism by measuring critical-clause generation rates (Fig. 6). If the results hold up, it is a useful addition to the SLS toolbox.\n\nThe soft spots, in order of severity:\n\nFirst, the statistical basis for the headline exponential fit is shaky. For WalkSAT with b≈2e-3, the expected number of successes across the whole sample at N=6000 is about 1.5; at larger N it is effectively zero. The paper fits log(⟨p⟩) versus N without reporting confidence intervals, the fitting range, or how zero-success instances were handled. The hardest-quintile curves are even more fragile, since the 'hardest' instances at large N are essentially a random selection among instances with zero successes. This does not destroy the qualitative claim — at N=4000, WalkSAT already has enough successes to estimate p reliably and DOCSAT still wins by orders of magnitude — but the specific b values for WalkSAT in the hard quintile are not to be trusted.\n\nSecond, Eq. (1) has a sign error. The formula as written gives the negative of the change in TLC when x_k is flipped. If implemented as stated, the algorithm would increase TLC, the opposite of what is intended. The accompanying example in Fig. 3 suggests the implemented version uses the correct sign, but the text needs fixing.\n\nThird, the empirical basis is narrow. Only Weigt-protocol instances are used, and the TLC desert is verified on 29 hard instances at N=200. The hyperparameters rdoc=0.15 and pwalk=0.4 are not justified by tuning or sensitivity analysis, and the comparisons to YalSAT and Kissat are not representative of the best available SLS solvers (e.g., CCAnr, Sparrow). No code or data is released, which makes it hard to check the reproducibility.\n\nOverall, the paper is a solid candidate for peer review. The core idea is novel, clearly presented, and backed by a mechanism that is at least plausible. The statistical and technical issues should be addressed in revision, but they are fixable. I'd send it out.\n\n— [Your name]","headline":"A promising SLS heuristic built on a real TLC-desert observation, but the quantitative claims need better statistics and Eq. (1) has a sign error.","tokens_in":11478,"tokens_out":7710,"would_cite":true,"duration_ms":82951,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A stochastic local search solver for 3-SAT that actively reduces the number of oversatisfied clauses reports per-run success probabilities on critically hard random instances that are orders of magnitude higher than WalkSAT's.","keywords":["3-SAT","stochastic local search","WalkSAT","oversatisfied constraints","true literal count","critical clause density","Weigt protocol","satisfiability solver"],"falsifier":"Run DOCSAT on a fresh sample of hard satisfiable 3-SAT instances at the critical density while recording the true-literal counts of solutions and of the low-energy states the search visits; if any family of hard instances with $N\\ge 1000$ shows solutions with TLC equal to or above the typical low-energy states, the dissipation mechanism no longer separates solutions from traps and the claimed advantage should disappear.","tokens_in":10326,"feed_emoji":"🧩","tokens_out":7610,"duration_ms":71336,"temperature":0.7,"pith_summary":"This paper introduces DOCSAT, a stochastic local search solver for 3-SAT that deliberately reduces the number of oversatisfied clauses during search. The authors claim that DOCSAT outperforms existing solvers on critically hard satisfiable random instances, with success probability per run scaling as $\\langle p \\rangle \\sim (1+b)^{-N}$ with $b\\approx 3\\cdot 10^{-4}$ for DOCSAT versus $b\\approx 2\\cdot 10^{-3}$ for the best WalkSAT variant, and $b\\approx 6\\cdot 10^{-4}$ versus $3\\cdot 10^{-2}$ on the hardest quintile. If true, a simple modification of WalkSAT's variable-selection rule makes the hardest known random 3-SAT benchmark family tractable at problem sizes where both WalkSAT and the complete solver Kissat effectively stall.","feed_headline":"Dissipating oversatisfied clauses unlocks hard 3-SAT","feed_subtitle":"It outperforms WalkSAT and Kissat on hard random benchmarks up to 15000 variables.","key_machinery":"The central mechanism is the true-literal-count (TLC) desert as an auxiliary landscape coordinate. A clause with exactly one true literal is critical; one with more true literals is oversatisfied. DOCSAT adds a term proportional to the change in TLC to the usual breakcount score, so variable selection favors flips that reduce TLC and convert oversatisfied clauses into critical ones. The Weigt protocol supplies the benchmark family: random satisfiable 3-SAT formulas at the critical clause density $\\alpha_{\\rm crit}=4.27$.","core_discovery":"The paper's central claim is that hard random 3-SAT instances contain a statistical desert: low-energy states that stochastic search visits easily have many more true literals, hence many more oversatisfied clauses, than any actual solution. DOCSAT exploits this by replacing WalkSAT's pure breakcount minimization with the score $s=b+r_{\\rm doc}T$, where $b$ is the number of clauses a flip would break and $T$ is the change in the total true-literal count; minimizing the weighted sum pulls the search toward critical clauses and away from the high-true-literal traps. The authors report that this single change, with $r_{\\rm doc}=0.15$ and walk probability $0.4$, solves all their $N=200$ hard instances and outperforms WalkSAT, YalSAT, and Kissat on Weigt-protocol instances up to $N=15000$, including on the hardest quintile.","pith_inferences":["The TLC desert could be a general signature of hard satisfiable formulas rather than an artifact of the Weigt protocol, in which case DOCSAT's advantage might extend to other planted-solution and random constraint families.","Because $r_{\\rm doc}$ is held fixed in the paper, an annealed or adaptive schedule that strengthens the DOC term as search stalls might improve scaling further.","The method points to a broader principle: any cheaply computable statistic that separates solutions from local minima can be folded into a local-search score; true-literal count is one example."],"forward_implications":["On the benchmark family studied, per-trial success probability at fixed runtime no longer collapses exponentially as fast; the fitted exponent $b$ drops by roughly an order of magnitude, so expected runtime scales far more gently.","DOCSAT's hardest-quintile performance beats the average performance of WalkSAT, so the solver does not merely win on easy instances.","DOCSAT also surpasses the complete solver Kissat and the SLS solver YalSAT on these instances, despite their tuned heuristics.","Reducing oversatisfied clauses can be viewed as exploiting statistical structure beyond the primary cost function, suggesting the same trick may transfer to other combinatorial optimization problems."],"supporting_citations":[{"why":"Defines the WalkSAT heuristic with breakcount and walk probability that DOCSAT modifies and benchmarks against; the local-minima landscape analyzed is WalkSAT's.","marker":"[30]"},{"why":"Supplies the Weigt protocol used to generate the hard satisfiable 3-SAT benchmark instances at critical clause density.","marker":"[31]"},{"why":"Establishes the empirical optimal walk probability $p_{\\rm walk}\\approx 0.57$ for WalkSAT, the best-scaling baseline in the comparison.","marker":"[35, 36]"},{"why":"Describes the complete solver Kissat, the state-of-the-art competitor that DOCSAT outperforms on the benchmark family.","marker":"[37, 38]"},{"why":"Describes the SLS solver YalSAT, benchmarked in the appendix as a further competitor.","marker":"[39]"},{"why":"Describes Novelty and GWSAT, the WalkSAT variants benchmarked on the hard $N=1000$ instance to position DOCSAT's behavior.","marker":"[40, 41]"}],"fun_headline_variants":["DOCSAT dissipates oversatisfied constraints to crack hard 3-SAT","Oversatisfied clause abundance marks 3-SAT traps; DOCSAT fixes that","Hard 3-SAT: switch metric from broken to true literals","WalkSAT beaten: new heuristic exploits oversatisfied constraint signal"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole advantage rests on the claim that for hard random 3-SAT instances, every low-energy near-solution has substantially more true literals than every true solution, and that this gap keeps holding as instances grow from 200 to 15000 variables.","fun_headline_variants_meta":{"raw":{"variants":["DOCSAT dissipates oversatisfied constraints to crack hard 3-SAT","Oversatisfied clause abundance marks 3-SAT traps; DOCSAT fixes that","Hard 3-SAT: switch metric from broken to true literals","WalkSAT beaten: new heuristic exploits oversatisfied constraint signal"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000384,"raw_usage":{"total_tokens":2031,"prompt_tokens":945,"completion_tokens":1086,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":561,"completion_tokens_details":{"reasoning_tokens":1005}},"tokens_in":561,"tokens_out":1086,"duration_ms":11877,"temperature":1.0,"reasoning_tokens":1005,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T23:52:08.155604+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run DOCSAT on a fresh sample of hard satisfiable 3-SAT instances at the critical density while recording the true-literal counts of solutions and of the low-energy states the search visits; if any family of hard instances with $N\\ge 1000$ shows solutions with TLC equal to or above the typical low-energy states, the dissipation mechanism no longer separates solutions from traps and the claimed advantage should disappear.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines the WalkSAT heuristic with breakcount and walk probability that DOCSAT modifies and benchmarks against; the local-minima landscape analyzed is WalkSAT's."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the Weigt protocol used to generate the hard satisfiable 3-SAT benchmark instances at critical clause density."},{"cited_title":"Biere, T","cited_arxiv_id":null,"evidence_quote":"Describes the SLS solver YalSAT, benchmarked in the appendix as a further competitor."}],"review_version":1}