Pith. sign in

REVIEW 5 major objections 6 minor 43 references

Advancing Stochastic 3-SAT Solvers by Dissipating Oversatisfied Constraints

T0 review · 5 major / 6 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 2506.15774 v1 pith:FYZNHLZY submitted 2025-06-18 cs.AI cond-mat.stat-mechcs.DSmath.CO

J. Schwardt , J. C. Budich This is my paper · ORCID
classification cs.AIcond-mat.stat-mechcs.DSmath.CO
keywords 3-SATstochasticlocalsearchWalkSAToversatisfiedconstraintstrueliteralcountcriticalclausedensityWeigtprotocolsatisfiabilitysolver
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

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.

What carries the argument

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$.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

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

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

5 major / 6 minor

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 <p> ~ (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.

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 (5)
  1. [IV, Fig. 5, Eq. (3)] 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 <p> 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.
  2. [III, Eq. (1)] 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.
  3. [IV, Algorithm 1 and parameter choice] 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.
  4. [II and IV, generality] 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.
  5. [Appendix A and reproducibility] 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.
minor comments (6)
  1. [General typography] 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.
  2. [Fig. 1 caption] 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.
  3. [Fig. 5 and error bars] 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 <p>.
  4. [Eq. (3)] 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 <p> with expected runtime (which scales as 1/<p> only under additional assumptions).
  5. [Benchmark details] 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.
  6. [Reference [32]] Reference [32] cites 'Walksat project – version 57' without a URL or archive identifier; please provide a persistent link or repository DOI.

Circularity Check

1 steps flagged · score 2.0 of 10

Benchmark comparisons are direct and non-circular; one design-consistency check restates the DOCSAT objective.

  1. self definitional [Section IV, paragraph beginning 'Finally, we find it interesting to analyze...' and Figure 6]
    "Finally, we find it interesting to analyze the generation of critical clauses at the expense of oversatisfied ones in DOCSAT, which was the main intuition behind its construction (cf. Section II and Section III). Indeed, the rate Γc at which critical clauses are increased by the non-random step (see line 8 in Algorithm 1) for DOCSAT is about a factor of 4 higher than for WalkSAT."

    The DOCSAT selection rule is defined in Eq. (2) as s = b + rdoc·T, where T (Eq. (1)) is the change in the total true literal count. The heuristic is therefore explicitly constructed to penalize high TLC, i.e. to dissipate oversatisfied clauses by design. The 'verification' in Figure 6 that DOCSAT maintains more critical clauses than WalkSAT at fixed energy is a consistency check of this built-in objective, not an independent prediction of the heuristic. It does not support the headline performance claims, which rest on the direct solved-fraction measurements in Figures 1 and 5.

full rationale

The central performance claims (Figures 1, 5, 7) are direct empirical comparisons against WalkSAT, Kissat, and YalSAT on independently generated Weigt-protocol instances; no fitted parameter or derived quantity is reused to construct those benchmarks. The exponential form in Eq. (3) is presented as a fit to measured average success probabilities, not as a prediction derived from the TLC-desert observation, so the quoted b-values are fitted descriptions rather than circular derivations. The TLC-desert observation in Section II is an empirical correlation on hard instances, and using it to motivate DOCSAT is a legitimate design step, though it is made on the same instance distribution used for benchmarking. The only self-definitional element is the Section IV/Figure 6 'verification' that DOCSAT creates more critical clauses: this follows from the TLC penalty explicitly added to the score in Eq. (2), so it confirms the construction rather than testing it. Because that check is not load-bearing for the headline benchmark result and there are no load-bearing self-citations or imported uniqueness theorems, the circularity is minor.

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

The central empirical claim rests on the choice of rdoc and pwalk, the assumption that the Weigt-protocol distribution is the right testbed, the extrapolation of the TLC-desert observation, and the exponential fit. No new physical or mathematical entities are introduced.

free parameters (4)
  • rdoc = 0.15
    Relative weight of the true-literal-count term in Eq. (2). Chosen without reporting a tuning or sensitivity analysis; WalkSAT is recovered for rdoc=0.
  • pwalk (DOCSAT) = 0.4
    Walk probability for DOCSAT, fixed at 0.4. The paper shows WalkSAT at several pwalk values but does not explore the pwalk-rdoc interaction for DOCSAT.
  • b (DOCSAT) = ~3e-4
    Fit of Eq. (3) to benchmark success probabilities; no error bars provided. Used to quantify the central scaling claim.
  • b (WalkSAT best) = ~2e-3
    Fit of Eq. (3) to benchmark success probabilities; no error bars provided. Used as the comparison baseline.
assumptions (4)
  • domain assumption The Weigt protocol at alpha=4.27 generates random satisfiable 3-SAT instances that are representative of critically hard instances.
    Used for all benchmarks (Section IV); if this distribution is atypical, the superiority claim is narrower than stated.
  • domain assumption The true-literal-count desert observed for 29 hard N=200 instances extends to larger system sizes and to other instances from the same distribution.
    The motivation and mechanism rest on this extrapolation (Section II, Fig. 2).
  • domain assumption An equal iteration budget (300N flips per trial) is a fair basis for comparing solvers.
    Section IV; wall-clock runtimes are not reported, and DOCSAT's per-flip cost is not analyzed.
  • ad hoc to paper The exponential scaling form ⟨p⟩ ∼ (1+b)^{-N} describes the success probabilities over the tested N range.
    Used to quantify the improvement via b; no derivation is given, and error bars are not reported (Eq. (3)).

how reviews work

0 comments
Cite this review

Pith. "Pith review of Advancing Stochastic 3-SAT Solvers by Dissipating Oversatisfied Constraints." pith.science (2026). https://pith.science/paper/FYZNHLZY

@misc{pith2026250615774,
  author       = {Pith},
  title        = {Pith review of: Advancing Stochastic 3-SAT Solvers by Dissipating Oversatisfied Constraints},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FYZNHLZY}},
  note         = {Machine review of arXiv:2506.15774}
}
read the original abstract

We introduce and benchmark a stochastic local search heuristic for the NP-complete satisfiability problem 3-SAT that drastically outperforms existing solvers in the notoriously difficult realm of critically hard instances. Our construction is based on the crucial observation that well established previous approaches such as WalkSAT are prone to get stuck in local minima that are distinguished from true solutions by a larger number of oversatisfied combinatorial constraints. To address this issue, the proposed algorithm, coined DOCSAT, dissipates oversatisfied constraints (DOC), i.e. reduces their unfavorable abundance so as to render them critical. We analyze and benchmark our algorithm on a randomly generated sample of hard but satisfiable 3-SAT instances with varying problem sizes up to N=15000. Quite remarkably, we find that DOCSAT outperforms both WalkSAT and other well known algorithms including the complete solver Kissat, even when comparing its ability to solve the hardest quintile of the sample to the average performance of its competitors. The essence of DOCSAT may be seen as a way of harnessing statistical structure beyond the primary cost function of a combinatorial problem to avoid or escape local minima traps in stochastic local search, which opens avenues for generalization to other optimization problems.

Figures

Figures reproduced from arXiv: 2506.15774 by the authors.

Figure 1
Figure 1. Upper panel: Illustration of two competing processes [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. Density of configurations #x at a fixed energy E as a function of TLC for 104 runs of WalkSAT with 104 flips per run and pwalk = 0.5. Out of 250 instances with N = 200, those with success probability p > 90% (easy) and p < 1% (hard) are compared. The black vertical stilts correspond to individual solutions for the hardest (for WalkSAT) four instances. For easy instances, differences between the E = 5 bulk states and… view at source ↗
Figure 4
Figure 4. Logarithmic plot of the number of states [PITH_FULL_IMAGE:figures/full_fig_p004_4.png] view at source ↗
Figures from the paper (3 more)
Figure 5
Figure 5. Figure 5: Average success probability ⟨p⟩ for the same dataset as in [PITH_FULL_IMAGE:figures/full_fig_p004_5.png]
Figure 6
Figure 6. Figure 6: Average number of critical clauses #crit in states [PITH_FULL_IMAGE:figures/full_fig_p005_6.png]
Figure 8
Figure 8. Figure 8: WalkSAT and related SLS algorithms for a hard [PITH_FULL_IMAGE:figures/full_fig_p006_8.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

43 extracted references · 38 canonical work pages

  1. [1]

    S. A. Cook, The complexity of theorem-proving proce- dures, inProceedings of the Third Annual ACM Sympo- sium on Theory of Computing, STOC ’71 (Association for Computing Machinery, New York, NY, USA, 1971) p. 151–158

    1971

  2. [2]

    By contrast, for the hard problems, all of the (few) solutions found have significantly lower TLC

    is clearly correlated withp: For easy problems, the distribution of solution states (E = 0) has TLCs similar to that of the low-energy sector (exemplified byE = 5). By contrast, for the hard problems, all of the (few) solutions found have significantly lower TLC. This quantitatively substantiates the quite natural picture that solutions to hard instances ...

    work page 2000

  3. [3]

    M. R. Garey and D. S. Johnson, Computers and In- tractability; A Guide to the Theory of NP-Completeness (W. H. Freeman & Co., USA, 1990)

    1990

  4. [4]

    R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations: Proceedings of a symposium on the Complexity of Computer Compu- tations, held March 20–22, 1972, at the IBM Thomas J. Watson Research Center, Yorktown Heights, New York, and sponsored by the Office of Naval Research, Mathe- matics Program, IBM World Trade Corpor...

    work page 1972

  5. [5]

    Mukherjee and S

    S. Mukherjee and S. Roy, Sat based solutions for detailed routing of island style fpga architectures, Microelectronics Journal 46, 706 (2015)

    work page 2015

  6. [6]

    G.-J. Nam, K. A. Sakallah, and R. A. Rutenbar, Satisfiability-Based Layout Revisited: Detailed Routing of Complex FPGAs Via Search-Based Boolean SAT , in Field-Programmable Gate Arrays, International ACM 7 Symposium on(IEEE Computer Society, Los Alamitos, CA, USA, 1999) pp. 167–175

    work page 1999

  7. [7]

    Gupta, M

    A. Gupta, M. K. Ganai, and C. Wang, Sat-based verifica- tion methods and applications in hardware verification, in Formal Methods for Hardware Verification, edited by M. Bernardo and A. Cimatti (Springer Berlin Heidelberg, Berlin, Heidelberg, 2006) pp. 108–143

    work page 2006

  8. [8]

    M. R. Prasad, A. Biere, and A. Gupta, A survey of recent advances in sat-based formal verification, International Journal on Software Tools for Technology Transfer7, 156 (2005)

    work page 2005

Show all 43 references
  1. [9]

    P.-H. Yuh, C. C.-Y. Lin, T.-W. Huang, T.-Y. Ho, C.-L. Yang, and Y.-W. Chang, A sat-based routing algorithm for cross-referencing biochips, inInternational Workshop on System Level Interconnect Prediction(2011) pp. 1–7

    2011

  2. [10]

    G. P. Matos, L. M. Albino, R. L. Saldanha, and E. M. Morgado, Solving periodic timetabling problems with sat and machine learning, Public Transport13, 625 (2021)

    2021

  3. [11]

    Barahona, On the computational complexity of ising spin glass models, Journal of Physics A: Mathematical and General 15, 3241 (1982)

    F. Barahona, On the computational complexity of ising spin glass models, Journal of Physics A: Mathematical and General 15, 3241 (1982)

    1982

  4. [12]

    D. V. Zhukov, D. A. Zheleznikov, and M. A. Zapletina, The iterative sat based approach to detailed routing for reconfigurable system-on-a-chip, in2020 IEEE Conference of Russian Young Researchers in Electrical and Electronic Engineering (EIConRus)(2020) pp. 1905–1910

    2020

  5. [13]

    Allouche, I

    D. Allouche, I. André, S. Barbe, J. Davies, S. de Givry, G. Katsirelos, B. O’Sullivan, S. Prestwich, T. Schiex, and S. Traoré, Computational protein design as an optimiza- tion problem, Artificial Intelligence212, 59 (2014)

    2014

  6. [14]

    Lucas, Ising formulations of many np problems, Fron- tiers in Physics2, 5 (2014)

    A. Lucas, Ising formulations of many np problems, Fron- tiers in Physics2, 5 (2014)

    2014

  7. [15]

    J. D. Park, Using weighted max-sat engines to solve mpe, in Eighteenth National Conference on Artificial Intelli- gence (American Association for Artificial Intelligence, USA, 2002) p. 682–687

    2002

  8. [16]

    Ollikainen, E

    N. Ollikainen, E. Sentovich, C. Coelho, A. Kuehlmann, and T. Kortemme, Sat-based protein design, in 2009 IEEE/ACM International Conference on Computer-Aided Design - Digest of Technical Papers(2009) pp. 128–135

    2009

  9. [17]

    Xing and W

    Z. Xing and W. Zhang, Maxsolver: An efficient exact algorithm for (weighted) maximum satisfiability, Artificial Intelligence 164, 47 (2005)

    2005

  10. [18]

    Dechter,Constraint Processing(Morgan Kaufmann, 2003)

    R. Dechter,Constraint Processing(Morgan Kaufmann, 2003)

    2003

  11. [19]

    Preskill, Quantum computing 40 years later, inThe Feynman Lectures on Computation, edited by A

    J. Preskill, Quantum computing 40 years later, inThe Feynman Lectures on Computation, edited by A. J. G. Hey (Taylor & Francis, 2021) 2nd ed., to appear; preprint available as arXiv:2106.10522

    2021 arXiv

  12. [20]

    Marques-Silva, M

    J. Marques-Silva, M. Janota, and A. Belov, Minimal sets over monotone predicates in boolean formulae, inProceed- ings of the 25th International Conference on Computer Aided Verification - Volume 8044, CAV 2013 (Springer- Verlag, Berlin, Heidelberg, 2013) p. 592–607

    2013

  13. [21]

    Kullmann, Present and future of practical sat solving, in Complexity of Constraints: An Overview of Current Research Themes, edited by N

    O. Kullmann, Present and future of practical sat solving, in Complexity of Constraints: An Overview of Current Research Themes, edited by N. Creignou, P. G. Kolaitis, and H. Vollmer (Springer Berlin Heidelberg, Berlin, Hei- delberg, 2008) pp. 283–319

    2008

  14. [22]

    Aaronson, Quantum Computing since Democritus (Cambridge University Press, 2013)

    S. Aaronson, Quantum Computing since Democritus (Cambridge University Press, 2013)

    2013

  15. [23]

    Eén and A

    N. Eén and A. Biere, Effective preprocessing in sat through variable and clause elimination, inTheory and Applications of Satisfiability Testing, edited by F. Bac- chus and T. Walsh (Springer Berlin Heidelberg, Berlin, Heidelberg, 2005) pp. 61–75

    2005

  16. [24]

    Biere, M

    A. Biere, M. Heule, H. van Maaren, and T. Walsh, eds., Handbook of Satisfiability, Frontiers in Artificial Intelli- gence and Applications, Vol. 185 (IOS Press, 2009)

    2009

  17. [25]

    J. K. Fichte, D. L. Berre, M. Hecher, and S. Szeider, The silent (r)evolution of sat, Commun. ACM66, 64–72 (2023)

    2023

  18. [26]

    Marques-Silva, I

    J. Marques-Silva, I. Lynce, and S. Malik, Conflict-driven clause learning sat solvers, inHandbook of Satisfiability, Frontiers in Artificial Intelligence and Applications No. 1 (IOS Press, Netherlands, 2009) pp. 131–153, 1st ed

    2009

  19. [27]

    H. H. Hoos and T. Stützle, Local search algorithms for sat: An empirical evaluation, Journal of Automated Reasoning 24, 421 (2000)

    2000

  20. [28]

    Alouneh, S

    S. Alouneh, S. Abed, M. H. Al Shayeji, and R. Mesleh, A comprehensive study and analysis on sat-solvers: ad- vances, usages and achievements, Artif. Intell. Rev.52, 2575–2601 (2019)

    2019

  21. [29]

    H. Fu, Y. Xu, S. Chen, and J. Liu, Improving walksat for random 3-sat problems, JUCS - Jour- nal of Universal Computer Science 26, 220 (2020), https://doi.org/10.3897/jucs.2020.013

    2020 doi

  22. [30]

    H. H. Hoos and T. Stützle, Stochastic local search algo- rithms: An overview, inSpringer Handbook of Computa- tional Intelligence, edited by J. Kacprzyk and W. Pedrycz (Springer Berlin Heidelberg, Berlin, Heidelberg, 2015) pp. 1085–1105

    2015

  23. [31]

    in the critical regime, we demonstrate that DOCSAT performs stronger even on this unfavorable selection than WalkSAT does on the entire sample (see Fig. 5). Finally, we verify with benchmark data that the DOCSAT heuris- tic indeed generates critical clauses at the expense of o...

  24. [32]

    Selman, H

    B. Selman, H. A. Kautz, and B. Cohen, Noise strategies for improving local search, inProceedings of the Twelfth National Conference on Artificial Intelligence (Vol. 1), AAAI ’94 (American Association for Artificial Intelligence, USA, 1994) p. 337–343

    1994

  25. [33]

    M. Weigt, The random 3-satisfiability problem: From the phase transition to the efficient generation of hard, but satisfiable problem instances, inNew Optimization Algorithms in Physics(John Wiley & Sons, Ltd, 2004) Chap. 7, pp. 119–137

    2004

  26. [34]

    Kautz, Walksat project – version 57 (2023)

    H. Kautz, Walksat project – version 57 (2023)

    2023

  27. [35]

    Cheeseman, B

    P. Cheeseman, B. Kanefsky, and W. M. Taylor, Where the really hard problems are, inProceedings of the 12th International Joint Conference on Artificial Intelligence - Volume 1, IJCAI’91 (Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1991) p. 331–337

    1991

  28. [36]

    Mitchell, B

    D. Mitchell, B. Selman, and H. Levesque, Hard and easy distributions of sat problems, inProceedings of the Tenth National Conference on Artificial Intelligence, AAAI’92 (AAAI Press, 1992) p. 459–465

    1992

  29. [37]

    L. Kroc, A. Sabharwal, and B. Selman, An empirical study of optimal noise and runtime distributions in local search, in Theory and Applications of Satisfiability Testing – SAT 2010, edited by O. Strichman and S. Szeider (Springer Berlin Heidelberg, Berlin, Heidelberg, 2010) pp...

    2010

  30. [38]

    Balint and U

    A. Balint and U. Schöning, Choosing probability distri- butions for stochastic local search and the role of make versus break, inTheory and Applications of Satisfiability Testing – SAT 2012, edited by A. Cimatti and R. Se- bastiani (Springer Berlin Heidelberg, Berlin, Heidelberg,

    2012

  31. [39]

    Biere, T

    A. Biere, T. Faller, K. Fazekas, M. Fleury, N. Froleyks, and F. Pollitt, CaDiCaL, Gimsatul, IsaSAT and Kissat 8 entering the SAT Competition 2024, inProc. of SAT Competition 2024 – Solver, Benchmark and Proof Checker Descriptions, Department of Computer Science Report Series B...

    2024

  32. [40]

    Biere, T

    A. Biere, T. Faller, K. Fazekas, M. Fleury, N. Froleyks, andF.Pollitt,Cadical2.0,in Computer Aided Verification, edited by A. Gurfinkel and V. Ganesh (Springer Nature Switzerland, Cham, 2024) pp. 133–152

    2024

  33. [41]

    A. Biere, Cadical, lingeling, plingeling, treengeling, yalsat entering the sat competition 2017, inProceedings of SAT Competition 2017 - Solver and Benchmark Descriptions, Department of Computer Science Series of Publications B, Vol. B-2017-1, edited by Tomas Tomáš, Marijn Heu...

    2017

  34. [42]

    C. M. Li, W. Wei, and H. Zhang, Combining adaptive noise and look-ahead in local search for sat, inTheory and Applications of Satisfiability Testing – SAT 2007, edited by J. Marques-Silva and K. A. Sakallah (Springer Berlin Heidelberg, Berlin, Heidelberg, 2007) pp. 121–133

    2007

  35. [43]

    D. N. Pham, J. Thornton, C. Gretton, and A. Sattar, Advances in local search for satisfiability, inAI 2007: Ad- vances in Artificial Intelligence, edited by M. A. Orgun and J. Thornton (Springer Berlin Heidelberg, Berlin, Hei- delberg, 2007) pp. 213–222

    2007

Pith tools

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