Pith. sign in

REVIEW 1 major objections 7 minor 14 cited by

Autonomous Code Evolution Meets NP-Completeness

T0 review · 1 major / 7 minor · reviewed 2026-08-04 · deepseek-v4-flash

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

Pith's one-line read A self-evolving LLM coding agent modified full SAT solver repositories and produced solvers that outperformed the human-designed winners of the SAT Competition 2025, despite training only on 2024 code and benchmarks.

desk verdict A real and important repo-scale LLM evolution result, but the 'autonomous beating 2025 champions' claim is undercut by the paper's own admission of heavy human steering. read the letter →

arxiv 2509.07367 v1 pith:JUZXJEIK submitted 2025-09-09 cs.AI cs.LGcs.LO

Cunxi Yu , Rongjian Liang , Chia-Tung Ho , Haoxing Ren This is my paper
classification cs.AIcs.LGcs.LO
keywords LLMcodeevolutionBooleansatisfiabilitySATsolveragenticcodingself-evolvingrulesCompetitionrepository-scaleproofverification
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 claims that an LLM-driven coding agent can evolve a full-size SAT solver repository—hundreds of files and tens of thousands of lines of C/C++—rather than an isolated algorithm kernel, and that the resulting solvers outclass the human-designed winners of the SAT Competition 2025. The framework, SATLUTION, starts from five SAT Competition 2024 solver codebases and uses only 2024 benchmark instances as feedback, yet its evolved solvers achieve the lowest PAR-2 scores on the 2025 competition benchmark set and also beat both the 2024 and 2025 champions on the 2024 set. The authors argue this is the first demonstration of repository-scale, self-evolving LLM code evolution, with a rule base that updates itself alongside the code. If true, it would mean that designing champion SAT solvers—a domain that has required decades of expert hand-tuning—can be substantially automated, with correctness protected by proof-checking.

What carries the argument

The central mechanism is the closed loop of agent, verifier, and distributed evaluator, governed by a rulebase that is both static and self-evolving. The two-stage verification pipeline is load-bearing: Stage 1 compiles the solver and runs smoke tests; Stage 2 checks SAT assignments and validates UNSAT DRAT proofs, so an incorrect solver is pruned before it can receive reward. The rulebase encodes correctness constraints, forbidden patterns, repository-structure requirements, and champion/failure knowledge, and after each cycle a post-mortem analyzer proposes rule patches, making the evolution policy itself evolve with the code. The PAR-2 feedback plus fine-grained solved-instance time cutof

What would settle it

Run the entire evolution from the same five 2024 seed codebases with the same 2024 benchmark feedback and the same two-stage verifier, but with all human steering removed—no human-selected plan directions, no manually chosen 'best' variant per cycle, no human hand-picking the final submitted solver. If no fully autonomous run produces a solver that beats the official 2025 winner under the standard 5000-second PAR-2 evaluation, the paper's autonomy-and-generalization claim is falsified. A cheaper test: check whether the authors' choice of the 'SATLUTION Best' solver among the evolved variants w

Watch

Extended reading notes

Core claim

At the design's core is an iterative loop: a Planning agent proposes high-level solver changes, a Coding agent edits the repository, a two-stage verifier checks that every SAT answer comes with a satisfying assignment and every UNSAT answer comes with a valid DRAT proof (a machine-checkable unsatisfiability certificate), and a distributed evaluator on 800 CPU nodes scores the verified solver on all 400 SAT Competition 2024 instances. The reward is based mainly on PAR-2 plus finer runtime and memory metrics. Across about 70 evolution cycles, the best solver's PAR-2 dropped steadily, crossing the 2025 champion's level around iteration 50. Under competition-standard evaluation on the 2025 bench

Load-bearing premise

The load-bearing premise is that the human steering, the manually crafted verifier and evaluator, and the manual choice of final solver did not smuggle in knowledge of the 2025 benchmarks or of which heuristics win SAT competitions; the paper itself acknowledges that human intervention remained critical.

Editorial extensions

If this is right

  • Repository-scale code evolution works: the same planning/coding loop that previously improved isolated kernels can navigate build systems and hundreds of source files.
  • A benchmark gap does not prevent transfer: training only on 2024 instances produced solvers that beat 2025 winners, so the evolved changes generalize beyond the training distribution.
  • Correctness need not be sacrificed: because every UNSAT outcome carries a checked DRAT proof, no solver that passed verification produced a misclassification on the competition benchmarks.
  • Feedback design is a control knob: moving from 'instances solved' to PAR-2 with time-cutoff distributions shifted the evolved solvers' emphasis from UNSAT-heavy gains toward medium-hard SAT speed.
  • The evolution policies themselves can be learned: failure patterns become forbidden rules, champion strategies become preserved rules, and the rulebase is versioned and updated each cycle.

Reading between the lines

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

  • A fair reading of the paper's own discussion is that full autonomy is not yet demonstrated: the flow was semi-automated, with humans steering high-level strategy and constructing the verifier and evaluator. A fully hands-off replication is the natural next test of how much of the gain is genuinely agent-driven.
  • If the generalization result holds under the weak assumption above, it implies the evolved solvers found transferable structural heuristics rather than benchmark-specific tuning; that in turn suggests competition preparation may shift from hand-tuning toward agent-guided exploration.
  • The same loop is transferable to any problem with a fast, formal verifier—SAT, EDA, planning, or theorem proving—so the key bottleneck is automating verifier construction, which the paper explicitly identifies as the frontier.
  • The learned components such as multi-UIP clause learning, bandit-tuned vivification, and compressed watch lists are entangled in a repository diff of over 10,000 lines, so isolating their individual contributions would require ablation-friendly instrumentation and is a concrete extension of this work.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

1 major / 7 minor

Summary. The paper presents SATLUTION, an LLM-agent framework that evolves full SAT-solver repositories (hundreds of files, tens of thousands of lines) starting from five SAT Competition 2024 solvers, using the SAT Competition 2024 benchmark as the only explicit feedback plus a manually written static rulebase and evaluator. The central claim is that, after roughly 70 evolution cycles, the evolved solvers achieve lower PAR-2 than the winners of SAT Competition 2025 on the 2025 benchmark and also beat both the 2024 and 2025 champions on the 2024 benchmark. Additional claims include repository-scale generalization beyond AlphaEvolve's single-file scope, a self-evolving rulebase, strict SAT/UNSAT correctness guarantees via DRAT proof validation, and a smooth improvement trajectory. The paper includes a methods section describing the two-agent architecture, two-stage verification pipeline, distributed evaluation on 800 CPU nodes, and a discussion section with limitations.

Significance. If the headline performance claim holds with the stated autonomy, the result is significant for AI-driven code evolution and for the SAT community: it would be the first demonstration that an LLM agent can evolve a full competition-level solver repository beyond human-designed winners in an external competition year. The paper also ships a substantial engineering effort: a multi-stage verifier with DRAT checking, VBS-based oracle comparisons, distributed evaluation, and a rulebase that co-evolves. The use of an external 2025 benchmark is a genuine strength, as is the explicit correctness validation rather than relying on end-to-end performance only. The reported cost of under $20k and the detailed token/cost breakdown are useful reproducibility-oriented details.

major comments (1)
  1. [Discussion .2 and Section 3 (Verification pipeline)] The paper describes a two-stage verifier but sometimes refers to 'Stage 3' in Discussion .2 ('validating UNSAT proofs in Stage 3') while the methods describe Stage 1 (compile/smoke) and Stage 2 (full validation). This inconsistency is not merely cosmetic: the actual number of stages affects the reader's understanding of the correctness pipeline and of what 'manual' components were involved. The authors should harmonize the terminology and clarify whether DRAT proof validation is part of Stage 2 or a separate Stage 3, and whether the 'Stage 2 feedback flow is manually crafted' claim covers the DRAT checker and its feedback.
minor comments (7)
  1. [Abstract] The abstract contains a sentence fragment: 'Targeting Boolean Satisfiability (SAT), the canonical NP-complete problem and a cornerstone of both theory and applications.' This should be merged with the preceding sentence or turned into a full clause.
  2. [Fig. 2 caption] The caption says 'top-3 solvers solved 347, 345, and 344 instances' but the figure labels show three SATLUTION solvers; it is unclear which specific solver names correspond to these counts. Please label the curves with solver IDs (e.g., S_68, S_70) as done in Fig. 8.
  3. [Fig. 8] The figure shows 'SATLUTION Best' and 'SATLUTION Accumulated Mean' but the main text does not define how 'accumulated mean' is computed (e.g., moving average over iterations, average of all evaluated variants). This should be stated in the caption or text.
  4. [Section 3, Performance Evaluation and Feedback Metrics] The sentence 'The primary metric driving evolution is the PAR-2 score' is followed later by 'PAR-2 score feedback is used only in the later evolution cycles (after 33 cycle)'. This is internally inconsistent. Clarify whether PAR-2 was used from the start or only after cycle 33, and how the earlier cycles were rewarded.
  5. [Section 3, Rule System] The rulebase is described as 'self-evolving' but the description of automatic rule evolution in .6 relies heavily on bash scripts and manual 'next step' checklists. Some of the code snippets in .6 appear to be illustrative rather than actually executed (e.g., 'TEST on Cycle 27 completion (NEXT STEP)'). The paper should distinguish implemented automation from proposed workflow, otherwise the 'self-evolving rules' claim is stronger than the evidence.
  6. [Discussion .3] The sentence 'the evaluator attains near-instantaneous fitness assessment at cluster scale' is hyperbolic given that feedback turnaround is stated as 5,000 seconds (the timeout). Consider rewording to 'minimal feedback turnaround' or similar.
  7. [Global] The paper has several typographical and formatting issues: 'SA T' instead of 'SAT' in figure captions (e.g., Fig. 3, Fig. 4, Fig. 6, Fig. 7), 'Mandantory' in Listing 1, 'T able' in Table captions, and inconsistent spacing around citations. A careful proofread is needed.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the 2025 competition evaluation is an external test set, and the paper's admissions of human intervention are limitations on autonomy rather than circular inputs.

full rationale

This paper presents an empirical evolutionary system rather than a formal derivation, and its central comparison is not circular. The headline claim—that solvers evolved from SAT Competition 2024 codebases and benchmark outperform SAT Competition 2025 winners—is an out-of-sample evaluation: the 2025 benchmark is not used as feedback, as stated in Section 2 ('all evolutionary training of SATLUTION was conducted exclusively on solver codebases and benchmark instances from SAT Competition 2024') and in the Methods. No fitted parameter is renamed as a prediction, no uniqueness theorem is imported from the authors' prior work, and no ansatz is smuggled in via citation. The only overlapping-author citation (ref. [26], HeuriGym) appears in a background list of LLM coding capabilities and is not load-bearing. The paper's own Discussion .1 does acknowledge that the flow 'proved most effective in a semi-automated setup with targeted human intervention' and that the evaluator and reward processor were 'manually crafted by the authors'; these passages are genuine limitations on the 'autonomous' claim and on attribution of the discovered strategies, but they do not make the 2025 result an input to the evolution. The 2025 benchmark remains an external test set, so the performance comparison is not equivalent to the training objective by construction. The slight hardware-induced differences in solved-instance counts noted in Figure 2 are a reproducibility caveat, not a circularity.

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

The paper introduces no new physical or mathematical entities. The framework is a software system that combines existing LLMs, SAT solvers, and proof checkers. The main unstated assumptions are about the validity of the evaluation infrastructure and about the degree to which human involvement shaped the evolved results. There are no fitted numerical constants in the conventional sense, but the reward design, the choice to enable PAR-2 feedback only after cycle 33, and the selection of five seed solvers are hand-chosen engineering decisions that bias the evolutionary search.

assumptions (4)
  • domain assumption The VBS (Virtual Best Solver) oracle provides correct ground-truth SAT/UNSAT outcomes for all 2024 benchmark instances.
    The evaluation and reward loop rely on VBS outcomes to detect misclassifications and to compute 'match with VBS' metrics (Table 3 in the paper). If VBS outcomes are incorrect, the correctness gate and the reward signal are corrupted.
  • standard math DRAT proofs are accepted as definitive certificates of unsatisfiability, and the external DRAT checker is sound.
    The Stage 2 verification requires validating UNSAT results with an external DRAT proof checker. This is a reasonable and standard assumption in the SAT community, but the paper does not identify the specific checker binary or version.
  • domain assumption PAR-2 on the 400-instance SAT Competition 2024 benchmark, with a 5000-second timeout, is a valid objective for evolving solvers that generalize to the 2025 competition.
    The entire evolution loop optimizes this objective and the headline result is measured the same way. If the 2024 benchmark is not representative of 2025, or if PAR-2 under the chosen hardware is a misleading metric, the central claim weakens.
  • domain assumption The human interventions in the semi-automated loop did not inject 2025-specific knowledge or solver-design expertise that the agents would not have discovered on their own.
    The discussion explicitly states that humans manually directed high-level strategies and that the verifier/evaluator were handcrafted by the authors. The autonomy claim depends on this assumption, and the paper does not quantify how much of the final improvement came from human steering.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Autonomous Code Evolution Meets NP-Completeness." pith.science (2026). https://pith.science/paper/JUZXJEIK

@misc{pith2026250907367,
  author       = {Pith},
  title        = {Pith review of: Autonomous Code Evolution Meets NP-Completeness},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/JUZXJEIK}},
  note         = {Machine review of arXiv:2509.07367}
}
read the original abstract

Large language models (LLMs) have recently shown strong coding abilities, enabling not only static code generation but also iterative code self-evolving through agentic frameworks. Recently, AlphaEvolve \cite{novikov2025alphaevolve} demonstrated that LLM-based coding agents can autonomously improve algorithms and surpass human experts, with scopes limited to isolated kernels spanning hundreds of lines of code. Inspired by AlphaEvolve, we present SATLUTION, the first framework to extend LLM-based code evolution to the full repository scale, encompassing hundreds of files and tens of thousands of lines of C/C++ code. Targeting Boolean Satisfiability (SAT), the canonical NP-complete problem and a cornerstone of both theory and applications. SATLUTION orchestrates LLM agents to directly evolve solver repositories under strict correctness guarantees and distributed runtime feedback, while simultaneously self-evolving its own evolution policies and rules. Starting from SAT Competition 2024 codebases and benchmark, SATLUTION evolved solvers that decisively outperformed the human-designed winners of the SAT Competition 2025, and also surpassed both 2024 and 2025 champions on the 2024 benchmarks.

Discussion (0). Sign in to comment.

Forward citations

Cited by 14 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Autonomous Evolution of EDA Tools: Multi-Agent Self-Evolved ABC

    cs.AR 2026-04 unverdicted novelty 8.0 of 10

    LLM agents autonomously evolve the ABC logic synthesis tool by iteratively rewriting its source code to achieve better quality-of-results on standard benchmarks while preserving the original interface.

  2. IC3-Evolve: Proof-/Witness-Gated Offline LLM-Driven Heuristic Evolution for IC3 Hardware Model Checking

    cs.AI 2026-01 unverdicted novelty 7.0 of 10

    IC3-Evolve evolves IC3 heuristics via offline LLM patches that are admitted only after passing proof or witness validation, yielding standalone improved checkers evaluated on HWMCC and unseen benchmarks.

  3. VPR-Evolve: Multi-Agent-Driven Algorithm Evolution for FPGA Place and Route

    cs.AR 2026-07 conditional novelty 6.5 of 10

    Multi-agent LLM evolution of VPR source code improves FPGA place-and-route QoR over stock VPR and AutoTuner on five VTR-9 benchmarks.

  4. From Tool Invocation to Source-Mechanism Exploration: Protected White-Box DSE for Open-Source EDA

    cs.AR 2026-07 unverdicted novelty 6.0 of 10

    Protected white-box DSE over OpenROAD detailed-placement source mechanisms cuts average post-DPL HPWL by 1.78% under a 2× runtime gate versus 0.38% for public-knob black-box DSE.

  5. From Tool Invocation to Source-Mechanism Exploration: Protected White-Box DSE for Open-Source EDA

    cs.AR 2026-07 conditional novelty 6.0 of 10

    LLM agents editing OpenROAD's detailed-placement source under a protected evaluator improve post-placement wirelength by 1.78% on average, far more than public-knob Bayesian optimization.

  6. From Tool Invocation to Source-Mechanism Exploration: Protected White-Box DSE for Open-Source EDA

    cs.AR 2026-07 unverdicted novelty 6.0 of 10

    Protected white-box DSE over OpenROAD detailed-placement source mechanisms cuts post-DPL HPWL by 1.78% on average versus 0.38% for public-knob black-box DSE under a 2× runtime gate.

  7. An Information-Theoretic Criterion for Efficient Data Synthesis

    cs.LG 2026-05 unverdicted novelty 6.0 of 10

    Synthetic data improves models only in information-open generation-training loops with external signals, and coarser signals like binary correctness enable better generalization by converging to the most information-e...

  8. GR-Evolve: Design-Adaptive Global Routing via LLM-Driven Algorithm Evolution

    cs.AR 2026-04 unverdicted novelty 6.0 of 10

    GR-Evolve applies LLM-driven code evolution to global routing, reporting up to 8.72% post-detailed-routing wirelength reduction on seven benchmarks across three technology nodes.

  9. TOPCELL: Topology Optimization of Standard Cell via LLMs

    cs.LG 2026-04 unverdicted novelty 6.0 of 10

    TOPCELL reformulates standard cell topology optimization as an LLM generative task with GRPO fine-tuning, outperforming base models and matching exhaustive solvers with 85.91x speedup in 2nm/7nm industrial flows.

  10. AIRA_2: Overcoming Bottlenecks in AI Research Agents

    cs.AI 2026-03 conditional novelty 6.0 of 10

    AIRA₂ improves AI research agents via asynchronous multi-GPU workers, hidden consistent evaluation, and interactive ReAct agents, reaching 81.5-83.1% percentile rank on MLE-bench-30 and exceeding human SOTA on 6 of 20...

  11. Scientific discovery as meta-optimization: a combinatorial optimization case study

    cs.AI 2026-06 unverdicted novelty 5.0 of 10

    Introduces consensus objective aggregation for meta-optimization of scientific discovery and reports improved scaling and speedup for 3-SAT algorithm discovery using digital MemComputing machines.

  12. Learning to Solve and Optimize by Evolving Code

    cs.LG 2026-05 unverdicted novelty 5.0 of 10

    CHECKMATE evolves correct high-performing solvers from formal specs and natural language descriptions, outperforming SOTA on configuration and scheduling problems.

  13. Agentic Hardware Design as Repository-Level Code Evolution

    cs.AR 2026-06 unverdicted novelty 4.0 of 10

    HORIZON applies repository-level self-evolution to hardware design artifacts and reports 100% completion on ChipBench, RTLLM, Verilog-Eval, and nine CVDP categories using a hands-free agent loop.

  14. From Heuristic Selection to Automated Algorithm Design: LLMs Benefit from Strong Priors

    cs.LG 2026-03 conditional novelty 4.0 of 10

    Prompting LLMs with strong benchmark algorithm code, rather than relying on linguistic instructions, improves LLM-driven black-box optimization; the proposed BAG method outperforms five baselines on pbo and bbob.

Reference graph

Works this paper leans on

51 extracted references · 44 canonical work pages · cited by 12 Pith papers

  1. [1]

    arXiv preprint arXiv:2506.13131 (2025)

    Novikov, A., V˜ u, N., Eisenberger, M., Dupont, E., Huang, P.-S., Wagner, A.Z., Shirobokov, S., Kozlovskii, B., Ruiz, F.J., Mehrabian, A., et al.: Alphae- volve: A coding agent for scientific and algorithmic discovery. arXiv preprint arXiv:2506.13131 (2025)

    arXiv 2025

  2. [2]

    In: Proceedings of the 38th Annual Design Automation Conference, pp

    Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineer- ing an efficient sat solver. In: Proceedings of the 38th Annual Design Automation Conference, pp. 530–535 (2001)

    work page 2001

  3. [3]

    variable coverage

    S¨ orensson, N., E´ en, N.: Minisat 2.1 and minisat++ 1.0-sat race 2008 editions. SAT, 31 (2009) 18 T able 4Distilled solver-design insights and techniques, ordered by development flow. T echnique / Lesson Core Idea Impact / Observation Multi-UIP Clause Learning Generate several UIP candidates (e.g., 1-UIP, 2-UIP, last-UIP) and choose by clause-quality me...

    work page 2008

  4. [4]

    International Journal on 19 Artificial Intelligence Tools27(01), 1840001 (2018)

    Audemard, G., Simon, L.: On the glucose sat solver. International Journal on 19 Artificial Intelligence Tools27(01), 1840001 (2018)

    work page 2018

  5. [5]

    Biere, A.,et al.: Lingeling, plingeling and treengeling entering the sat competition

    work page

  6. [6]

    Sat Competition2020, 50 (2020)

    Fleury, A., Heisinger, M.: Cadical, kissat, paracooba, plingeling and treengeling entering the sat competition 2020. Sat Competition2020, 50 (2020)

    work page 2020

  7. [7]

    In: International Conference on Computer Aided Verification, pp

    Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: Cadical 2.0. In: International Conference on Computer Aided Verification, pp. 133–152 (2024). Springer

    work page 2024

  8. [8]

    SAT COMPETITION2021, 15 (2021)

    Cherif, M.S., Habet, D., Terrioux, C.: Kissat mab: Combining vsids and chb through multi-armed bandit. SAT COMPETITION2021, 15 (2021)

    work page 2021

Show all 51 references
  1. [9]

    SAT COMPETITION2022, 20 (2022)

    Zheng, J., He, K., Chen, Z., Zhou, J., Li, C.-M.: Combining hybrid walking strat- egy with kissat mab, cadical, and lstech-maple. SAT COMPETITION2022, 20 (2022)

    2022

  2. [10]

    SAT COMPETITION 2025, 13

    Chen, S., Sun, Y., Zhang, J., Li, T., Liu, J.: Kissat corephase coreward and kissat mab corephase solvers in sat competition 2025. SAT COMPETITION 2025, 13

    2025

  3. [11]

    Proceedings of the Third Annual ACM Symposium on Theory of Computing (1971)

    Cook, S.A.: The complexity of theorem-proving procedures. Proceedings of the Third Annual ACM Symposium on Theory of Computing (1971)

    1971

  4. [12]

    Clay Mathematics Institute2(6), 3 (2000)

    Cook, S.: The p versus np problem. Clay Mathematics Institute2(6), 3 (2000)

    2000

  5. [13]

    Handbook of satisfiability, 131–153 (2009)

    Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning sat solvers. Handbook of satisfiability, 131–153 (2009)

    2009

  6. [14]

    Journal of the ACM (JACM)7(3), 201–215 (1960)

    Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM (JACM)7(3), 201–215 (1960)

    1960

  7. [15]

    Artificial Intelligence279, 103197 (2020)

    Li, C.-M., Xiao, F., Luo, M., Many` a, F., L¨ u, Z., Li, Y.: Clause vivification by unit propagation in cdcl sat solvers. Artificial Intelligence279, 103197 (2020)

    2020

  8. [16]

    Artificial Intelligence301, 103572 (2021)

    Froleyks, N., Heule, M., Iser, M., J¨ arvisalo, M., Suda, M.: Sat competition 2020. Artificial Intelligence301, 103572 (2021)

    2020

  9. [17]

    In: Proceedings of the AAAI Conference on Artificial Intelligence, vol

    Balyo, T., Heule, M., Jarvisalo, M.: Sat competition 2016: Recent developments. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 31 (2017)

    2016

  10. [18]

    Biere, A., Heule, M., Maaren, H.: Handbook of Satisfiability vol. 185. IOS press, ??? (2009)

    2009

  11. [19]

    https://satcompetition.github.io/

    International SAT Competition Organizers: The International SAT Competition Web Page. https://satcompetition.github.io/. Accessed: 2025-08-29 (2025) 20

    2025

  12. [20]

    In: SAT COMPETITION 2022, p

    Chen, X., Guo, W., Luo, W., Zhen, H.L., Li, X., Yuan, M., Yan, J.: Kissat-mab- rephasing and kissat relaxed. In: SAT COMPETITION 2022, p. 35 (2022)

    2022

  13. [21]

    In: 27th International Conference on Principles and Practice of Constraint Programming (2021)

    Cherif, M.S., Habet, D., Terrioux, C.: Combining vsids and chb using restarts in sat. In: 27th International Conference on Principles and Practice of Constraint Programming (2021)

    2021

  14. [22]

    In: SAT COMPETITION 2023, p

    Zheng, J., Jin, M., He, K., Chen, Z., Xue, J.: New rephasing strategies and their combinations. In: SAT COMPETITION 2023, p. 27 (2023)

    2023

  15. [23]

    In: 31st International Conference on Principles and Practice of Constraint Programming (CP 2025), pp

    Shi, Z., Jiang, W., Zhang, X., Luo, J., Liang, Y., Chu, Z., Xu, Q.: Dynamicsat: Dynamic configuration tuning for sat solving. In: 31st International Conference on Principles and Practice of Constraint Programming (CP 2025), pp. 34–1 (2025). Schloss Dagstuhl–Leibniz-Zentrum f¨ ...

    2025

  16. [24]

    In: 2023 60th ACM/IEEE Design Automation Conference (DAC), pp

    Li, M., Shi, Z., Lai, Q., Khan, S., Cai, S., Xu, Q.: On eda-driven learning for sat solving. In: 2023 60th ACM/IEEE Design Automation Conference (DAC), pp. 1–6 (2023). IEEE

    2023

  17. [25]

    arXiv preprint arXiv:2507.06261 (2025)

    Comanici, G., Bieber, E., Schaekermann, M., Pasupat, I., Sachdeva, N., Dhillon, I., Blistein, M., Ram, O., Zhang, D., Rosen, E., et al.: Gemini 2.5: Pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities. arXiv prepr...

    2025 arXiv

  18. [26]

    arXiv preprint arXiv:2506.07972 (2025)

    Chen, H., Wang, Y., Cai, Y., Hu, H., Li, J., Huang, S., Deng, C., Liang, R., Kong, S., Ren, H., et al.: Heurigym: An agentic benchmark for llm-crafted heuristics in combinatorial optimization. arXiv preprint arXiv:2506.07972 (2025)

    2025

  19. [27]

    arXiv preprint arXiv:2304.13187 (2023)

    Poldrack, R.A., Lu, T., Beguˇ s, G.: Ai-assisted coding: Experiments with gpt-4. arXiv preprint arXiv:2304.13187 (2023)

    2023 arXiv

  20. [28]

    Claude-3 Model Card1(1), 4 (2024)

    Anthropic, A.: The claude 3 model family: Opus, sonnet, haiku. Claude-3 Model Card1(1), 4 (2024)

    2024

  21. [29]

    Advances in Neural Information Processing Systems37, 44678–44709 (2024)

    Grayeli, A., Sehgal, A., Costilla Reyes, O., Cranmer, M., Chaudhuri, S.: Sym- bolic regression with a learned concept library. Advances in Neural Information Processing Systems37, 44678–44709 (2024)

    2024

  22. [30]

    arXiv preprint arXiv:2404.18400 (2024)

    Shojaee, P., Meidani, K., Gupta, S., Farimani, A.B., Reddy, C.K.: Llm-sr: Sci- entific equation discovery via programming with large language models. arXiv preprint arXiv:2404.18400 (2024)

    2024 arXiv

  23. [31]

    Nature625(7995), 468–475 (2024) 21

    Romera-Paredes, B., Barekatain, M., Novikov, A., Balog, M., Kumar, M.P., Dupont, E., Ruiz, F.J., Ellenberg, J.S., Wang, P., Fawzi, O.,et al.: Mathematical discoveries from program search with large language models. Nature625(7995), 468–475 (2024) 21

    2024

  24. [32]

    arXiv preprint arXiv:2507.22876 (2025)

    Sun, Y., Ye, F., Chen, Z., Wei, K., Cai, S.: Automatically discovering heuristics in a complex sat solver with large language models. arXiv preprint arXiv:2507.22876 (2025)

    2025 arXiv

  25. [33]

    🔍 Checking rule compliance for $SOLVER

    Devriendt, J., Bogaerts, B., Bruynooghe, M., Denecker, M.: Improved static sym- metry breaking for sat. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 104–122 (2016). Springer Discussion .1 SATLUTION flow interactions and limitations A c...

    2016

  26. [35]

    What should I check before starting SATLUTION_28?

    "What should I check before starting SATLUTION_28?" - **Expected**: Reference to Rule 01 (pre-evaluation testing)

  27. [36]

    Can I use malloc() in my new solver?

    "Can I use malloc() in my new solver?" - **Expected**: Reference to Rule 04 (forbidden patterns)

  28. [37]

    What documentation do I need for SATLUTION_28?

    "What documentation do I need for SATLUTION_28?" - **Expected**: Reference to Rule 03 (mandatory logging) ### **Cursor Behavior Indicators:** - **Proactive Rule Enforcement**: Cursor stops you from forbidden patterns - **Rule-Based Guidance**: Cursor references specific rules ...

  29. [38]

    **Identify Need**: New failure or process gap

  30. [39]

    **Document Pattern**: Add specific example to appropriate rule

  31. [40]

    **Update Verification**: Add check to compliance scripts

  32. [41]

    **Test Integration**: Verify Cursor follows updated rules

  33. [42]

    cursor/log/cycle_${CYCLE}_rule_analysis.md

    **Announce Change**: Log rule update in session documentation # Automatic Rule Evolution System ## SELF-IMPROVING RULE SYSTEM BASED ON CYCLE LEARNINGS ### ** 🔄 AUTOMATIC RULE REVISION FOR CONTINUOUS IMPROVEMENT** ## **1. CYCLE-BY-CYCLE RULE EVOLUTION FRAMEWORK** ### **Post-Cyc...

  34. [43]

    Execute: bash .cursor/rules/cycle_learning_pipeline.sh CYCLE_NUMBER

  35. [44]

    Review generated rule evolution summary

  36. [45]

    Apply updated rules to ALL future development

  37. [46]

    Reference new patterns in guidance and error prevention

  38. [47]

    $CURRENT_VERSION

    Update .cursorrules if major process changes detected This creates a SELF-IMPROVING rule system that learns from every cycle. ``` ### **Automatic Rule Version Management:** ```bash #!/bin/bash # rule_version_manager.sh CURRENT_VERSION=$(date +%Y%m%d)-cycle-$(ls SATLUTION_* | t...

  39. [48]

    **MANDATORY**: Run cycle learning pipeline

  40. [49]

    **AUTOMATIC**: Update rules based on new failure patterns

  41. [50]

    **INTEGRATION**: Apply updated rules to all future guidance

  42. [51]

    **VERIFICATION**: Test rule compliance on next solver ### **Continuous Improvement Cycle:** ``` New Failure → Pattern Analysis → Rule Update → Cursor Integration → Prevention ↑ ↓ Learning ←─────────────────────────────────────────────── Application ``` ### **Rule Evolution Tri...

  43. [2013]

    Proceedings of SAT competition2013, 1 (2013)

    2013

Pith tools

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