Pith. sign in

REVIEW 3 major objections 5 minor 46 references

Extracting Problem Structure with LLMs for Optimized SAT Local Search

T0 review · 3 major / 5 minor · reviewed 2026-08-10 · deepseek-v4-flash

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

Pith's one-line read The paper claims that LLMs can generate encoding-specific local search preprocessing that beats baseline CDCL seeding on hard structured SAT instances.

desk verdict A genuine proof-of-concept for LLM-generated SAT preprocessing, but the comparative claim needs a proper baseline and the structure-exploitation mechanism is only partially supported. read the letter →

arxiv 2501.14630 v2 pith:LGHK2AFR submitted 2025-01-24 cs.AI

André Schidler , Stefan Szeider This is my paper · ORCID
classification cs.AI
keywords SATsolvinglocalsearchpreprocessingCDCLsolverslargelanguagemodelsencodingstructurePyDirectedFeedbackVertexSetbounded-depthdecisiontrees
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

The paper claims that a large language model can read the Python code of a SAT encoding and turn it into a specialized local search routine that, when used as preprocessing for a CDCL (conflict-driven clause learning) solver, produces strong starting assignments for every instance of that encoding. The method is automatic: an LLM generates many candidate searches, a training-phase scorer ranks them, and a refinement loop with feedback improves them. On hard Directed Feedback Vertex Set instances the best generated function solves 12 instances that the solver alone could not; on graph coloring the best function solves more instances than the solver alone. The authors read the result as evidence that encoding-aware preprocessing can be synthesized rather than hand-crafted. They also report that the best DFVS function is a generic WalkSAT implementation, because the models misunderstood the DFVS encoding, which weakens the claim that structural understanding caused that particular gain.

What carries the argument

The load-bearing object is the local search function generated by the LLM from the PySAT encoding code, plus the two-phase pipeline that produces it. In the gathering phase the LLM is asked only for a local search routine with a fixed interface and is given the encoding program without its name or purpose; errors are repaired and successful functions are added to the prompt context to force diversity. In the refinement phase the top functions are iteratively varied and scored on training instances, with the LLM told whether a change improved average solver runtime by more than ten percent. The generated assignment enters the solver as the default phase, and the quality of an assignment is measured by how quickly the solver finishes from that starting point.

What would settle it

Run the pipeline a second time without showing the encoding code—prompt the LLM for generic local search functions that operate only on the CNF—and compare solved-instance counts on the same test sets; if the generic set matches the encoding-aware set on hard instances, the structure-extraction premise is false.

Watch

Extended reading notes

Core claim

In the paper's own framing, the discovery is that the structure of a SAT encoding is a reusable asset: an LLM that inspects the encoding program can generate local search algorithms that exploit that structure, and those algorithms apply to all instances produced by the same encoding, not just one instance. The generated algorithm produces an assignment that is fed into the solver as the default phase of every variable, so the solver's search starts from a promising point. The evaluation on three encodings of increasing complexity—graph coloring, directed feedback vertex set, bounded-depth decision trees—shows that such generated preprocessors can beat the solver alone on hard instances, but the benefit is uneven: it is clearest for directed feedback vertex set, absent in aggregate for bounded-depth decision trees, and the authors explicitly note that the best DFVS search was a standard WalkSAT because the models failed to grasp the encoding's intent.

Load-bearing premise

The load-bearing premise is that the speedups come from encoding-aware specialization, not simply from generating and testing dozens of generic local search heuristics; the paper's own Section 5.6.3 reports the best DFVS function was a plain WalkSAT because the models did not understand the DFVS encoding.

Editorial extensions

If this is right

  • A user who has a PySAT encoding can obtain a family of candidate local search preprocessors without manual algorithm design.
  • The same generated search applies to every future instance of that encoding, so the cost of generation is amortized over a benchmark family.
  • The refinement phase is necessary: the base versions from the gathering phase do not yield the best results.
  • Better LLM comprehension of the encoding correlates with better generated searches, so prompting that improves encoding understanding should improve the preprocessors.
  • The authors expect an efficient native implementation of the prototypes to be substantially faster than the Python versions they evaluated.

Reading between the lines

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

  • The DFVS result is consistent with a weaker hypothesis: that most of the gain comes from cheaply sampling many plausible local search heuristics and keeping the best, rather than from extracting encoding structure. The paper's own report that the winning DFVS function is generic WalkSAT supports this reading.
  • A direct test would be to run the same pipeline with the encoding program withheld, or replaced by a generic 'SAT formula' description, and compare solved-instance counts; if generic search matches structure-aware search, the structural explanation is not needed.
  • The comments in LLM-generated code often did not match what the code did, so diversity claims based on self-description are unreliable; measuring code behavior or edit distance would be a safer diversity signal.
  • The correlation between training and test scores was strong for DFVS but weak for coloring, implying that training-instance selection, not just the LLM, determines how well refinement generalizes.
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

3 major / 5 minor

Summary. The paper proposes an automated pipeline in which LLMs read PySAT-based SAT encoding schemes and generate specialized local search functions; the best functions, selected on training instances, are used to set default phases in the CDCL solver CaDiCaL. The pipeline has a gathering phase, a scoring phase on training instances, and a refinement phase. It is evaluated on three families of benchmarks: Graph Coloring, Directed Feedback Vertex Set (DFVS), and Bounded Depth Decision Trees (BDDT), with the headline result being that the best DFVS function solves 12 instances that the vanilla solver alone cannot solve. The authors claim that the method exploits encoding structure and achieves faster solving times compared to baseline preprocessing systems.

Significance. If the claims were fully supported, the paper would make a useful contribution: it proposes a reproducible, automated way to generate encoding-specific local search heuristics, and it ships code and data on Zenodo. The idea of using LLMs to analyze encodings rather than instances is original and could be of interest to the SAT/AI community. However, the current experimental validation does not establish the central comparative and mechanistic claims: no existing preprocessing or rephasing baseline is evaluated, and the paper's own analysis shows that the best DFVS function is a generic WalkSAT implementation, that the LLMs failed to understand the DFVS encoding, and that even incorrect implementations can score well. The significance therefore rests on plausible promise rather than demonstrated effect.

major comments (3)
  1. [§5.5, Table 1] The evaluation compares only against 'the SAT solver without any local search' run for one hour. The abstract claims 'faster solving times compared to baseline preprocessing systems,' and §2.3 identifies CaDiCaL's ProbSAT-based rephasing and CryptoMiniSat's preprocessing as the relevant baseline systems, yet none of these is run or reported. To support the comparative claim, the authors should add these baselines (or a standard local-search phase injection such as ProbSAT/WalkSAT) under identical time and hardware conditions, and report runtime distributions, not only solved/new counts.
  2. [§5.6.3, §5.2, §5.6.2] The mechanism claim—that gains come from extracting and exploiting encoding structure—is not established. The paper itself states that the best DFVS function is 'a straightforward WalkSAT implementation' (§5.6.3), that all LLMs 'fail to identify its overall purpose' for the DFVS encoding (§5.2), and that 'even wrong implementations can sometimes deliver good results' (§5.6.2). Consequently, the 12 additional DFVS instances may reflect the general benefit of any local-search starting point, or of sampling many heuristics in the gathering phase, rather than encoding-aware specialization. A generic local-search control (e.g., WalkSAT/ProbSAT with default-phase injection on the same instances) is needed to attribute the improvement to structure extraction; alternatively, the conclusions should be substantially weakened.
  3. [Table 1] Table 1 as printed appears internally inconsistent, which prevents interpretation of the quantitative results. For example, the Coloring benchmark is stated to have 38 test instances, yet the GPT 4o row reports 49 solved instances; in the DFVS block, the GPT o1-mini Base entry reports New=60 while Solved=30, which is impossible under the stated definitions. The table structure seems misaligned or the numbers contain errors. The authors should provide a corrected, clearly labeled table with per-variant Solved and New counts that are consistent with the benchmark sizes.
minor comments (5)
  1. [Abstract and §5.5] The abstract promises 'faster solving times,' but the test evaluation reports only solved-instance counts and new-instance counts, not runtimes. If the authors wish to keep this claim, they should report actual solving-time comparisons or speedups.
  2. [§5.5] The sentence 'we expect a good native implementation, e.g., in C++, would run orders of magnitudes faster than the Python prototypes' is speculative and should be moved to a limitations or future-work paragraph rather than appearing in the results section.
  3. [§5.4 and §4.4] The refinement phase uses a 10% average-runtime threshold to decide whether a change is significant, but no statistical testing or variance information is reported. Given that the selection of 'best' versions is based on training scores, some measure of stability across repeated runs would strengthen the ranking procedure.
  4. [Throughout] There are typographical issues, including 'Anthropnic' for Anthropic and 'Cadical' for CaDiCaL, and several author names appear with spacing artifacts (e.g., 'V oboril'). These should be corrected in a final version.
  5. [§5.3 and §5.6.1] The evaluation uses a single run per LLM model, but the generation process is stochastic. Reporting the variance across multiple pipeline runs, or at least explicitly noting the single-run limitation, would improve the reproducibility assessment.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the pipeline's train/test separation keeps function selection independent of test outcomes, and the WalkSAT-attribution issue is an experimental-support concern, not a self-referential derivation.

full rationale

The paper's derivation chain is not circular. Local search functions are generated in the Gathering Phase, ranked on training instances via the Section 4.3 scoring criteria, and only then evaluated on held-out test instances; test outcomes are not fed back into the selection process. The final test metrics therefore measure out-of-sample performance rather than restating the training objective. The claim that the best DFVS function is 'a straightforward WalkSAT implementation' and that the LLMs failed to identify the DFVS encoding's purpose weakens the paper's attribution of gains to LLM-extracted structure, but that is a correctness and experimental-support concern, not a circularity. Self-citations, such as the BDDT instance 'objectivity' reported unsolved in Schidler and Szeider [2024] and the DAGer oracle from Kiesel and Schidler [2022, 2023], are used as external benchmarks or benchmark-construction tools; they do not define the target result or encode the paper's conclusions by construction. No equation-level or definition-level reduction is present, so the paper is self-contained with respect to circularity.

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

The paper introduces no new theoretical entities; its contributions are empirical pipeline choices and domain assumptions about LLM reliability, benchmark selection, and evaluation fairness. The free parameters are engineering budgets and thresholds, not constants fitted to test outcomes, but they shape which functions are selected and therefore influence the reported results.

free parameters (5)
  • gathering pool size = 50
    Number of local search functions generated per LLM in the Gathering Phase (Section 5.4); hand-chosen budget.
  • refinement count = 19
    Each of the top five functions refined 19 times, producing 20 versions per base function (Section 5.4).
  • training selection window = 10-60 s
    Training instances are those solved by CDCL alone in 10-60 seconds; test instances take longer than one minute (Section 5.1). This split drives the ranking procedure.
  • significance threshold = 10%
    Runtime changes below 10% are treated as insignificant when giving refinement feedback to the LLM (Section 4.4).
  • top-k selection = 5
    Top five functions per LLM advance to the Refinement Phase (Section 5.4).
assumptions (4)
  • domain assumption LLM-generated functions that pass the half-minute smoke test are correct enough to use
    Section 4.2 verifies only that the function runs once on an easy instance within a short timeout; Section 5.6.2 later admits that even wrong implementations can achieve good results, so correctness is not actually guaranteed.
  • domain assumption Training score ranking predicts test performance
    The whole selection procedure assumes top training functions are top test functions; Section 5.6.1 reports almost no training-test correlation for Coloring and weak correlation for BDDT.
  • domain assumption PySAT encodings are representative of how structured problems are encoded
    The method takes the PySAT encoding scheme as input and assumes the encoding's structure carries across all instances produced by the same scheme (Sections 4.1 and 1).
  • domain assumption Setting CDCL default phases to the local search assignment is a valid measure of preprocessing benefit
    Section 3 defines the evaluation this way; no comparison is made to other phase-injection mechanisms or to the solver's own rephasing heuristics.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Extracting Problem Structure with LLMs for Optimized SAT Local Search." pith.science (2026). https://pith.science/paper/LGHK2AFR

@misc{pith2026250114630,
  author       = {Pith},
  title        = {Pith review of: Extracting Problem Structure with LLMs for Optimized SAT Local Search},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/LGHK2AFR}},
  note         = {Machine review of arXiv:2501.14630}
}
read the original abstract

Local search preprocessing makes Conflict-Driven Clause Learning (CDCL) solvers faster by providing high-quality starting points and modern SAT solvers have incorporated this technique into their preprocessing steps. However, these tools rely on basic strategies that miss the structural patterns in problems. We present a method that applies Large Language Models (LLMs) to analyze Python-based encoding code. This reveals hidden structural patterns in how problems convert into SAT. Our method automatically generates specialized local search algorithms that find these patterns and use them to create strong initial assignments. This works for any problem instance from the same encoding type. Our tests show encouraging results, achieving faster solving times compared to baseline preprocessing systems.

Figures

Figures reproduced from arXiv: 2501.14630 by the authors.

Figure 1
Figure 1. Schematic of the whole approach from the encoding scheme to pool of refined local search functions. [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. The top five local search functions for different problems over different refinement iterations. [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. Local search function scores on the training instances and test instances. Each marker represents one [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

46 extracted references · 29 canonical work pages

  1. [1]

    Efficient inference of optimal decision trees

    Florent Avellaneda. Efficient inference of optimal decision trees. In Proceedings of AAAI 2020 . AAAI Press, 2020

    work page 2020

  2. [2]

    Boosting the performance of SLS and CDCL solvers by preprocessor tuning

    Adrian Balint and Norbert Manthey. Boosting the performance of SLS and CDCL solvers by preprocessor tuning. In POS@SAT , volume 29 of EPiC Series in Computing , pages 1--14. EasyChair, 2013. DOI: https://doi.org/10.29007/28WW

    work page doi:10.29007/28ww 2013

  3. [4]

    Minimising decision tree size as combinatorial optimisation

    Christian Bessiere, Emmanuel Hebrard, and Barry O'Sullivan. Minimising decision tree size as combinatorial optimisation. In Proceedings of CP 2009 , pages 173--187, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg

    work page 2009

  4. [5]

    CaDiCaL , Kissat , Paracooba , Plingeling , and Treengeling entering the SAT competition 2020

    Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximilian Heisinger. CaDiCaL , Kissat , Paracooba , Plingeling , and Treengeling entering the SAT competition 2020. In Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions , pages 51--53, 2020

    work page 2020

  5. [6]

    Cadical 2.0

    Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. Cadical 2.0. In Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I , volume 14681 of Lecture Notes in Computer Science , pages 133--152. Springer, 2024. DOI: https://doi.org/10.100...

    doi:10.1007/978-3-031-65627-9 2024

  6. [7]

    Yet another local search solver and Lingeling and friends entering the SAT Competition 2014

    Armin Biere. Yet another local search solver and Lingeling and friends entering the SAT Competition 2014 . In Proc. of SAT Competition 2014 -- Solver and Benchmark Descriptions , volume B-2014-2 of Department of Computer Science Series of Publications B , pages 39--40. University of Helsinki, 2014

    work page 2014

  7. [8]

    CaDiCaL at the SAT race 2019

    Armin Biere. CaDiCaL at the SAT race 2019. In Proceedings of SAT Race 2019: Solver and Benchmark Descriptions , pages 8--9, 2019

    work page 2019

  8. [9]

    New methods to color the vertices of a graph

    Daniel Br\' e laz. New methods to color the vertices of a graph. Commun. ACM , 22(4):251–256, apr 1979. URL: https://dl.acm.org/doi/10.1145/359094.359101

    arXiv 1979

Show all 46 references
  1. [10]

    Deep cooperation of CDCL and local search for SAT

    Shaowei Cai and Xindi Zhang. Deep cooperation of CDCL and local search for SAT . In Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings , volume 12831 of Lecture Notes in Computer Science ,...

    2021 doi

  2. [11]

    Better decision heuristics in CDCL through local search and target phases

    Shaowei Cai, Xindi Zhang, Mathias Fleury, and Armin Biere. Better decision heuristics in CDCL through local search and target phases. J. Artif. Intell. Res. , 74:1515--1563, 2022. DOI: https://doi.org/10.1613/JAIR.1.13666

    2022 doi

  3. [12]

    Hazelwood, Gabriel Synnaeve, and Hugh Leather

    Chris Cummins, Volker Seeker, Dejan Grubisic, Mostafa Elhoushi, Youwei Liang, Baptiste Rozi \` e re, Jonas Gehring, Fabian Gloeckle, Kim M. Hazelwood, Gabriel Synnaeve, and Hugh Leather. Large language models for compiler optimization. CoRR , abs/2309.07062, 2023. DOI: https:/...

    2023 doi arXiv

  4. [13]

    SAT -based local improvement for finding tree decompositions of small width

    Johannes Klaus Fichte, Neha Lodha, and Stefan Szeider. SAT -based local improvement for finding tree decompositions of small width. In Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September...

    2017 doi

  5. [14]

    The silent (r)evolution of SAT

    Johannes Klaus Fichte, Daniel Le Berre, Markus Hecher, and Stefan Szeider. The silent (r)evolution of SAT . Commun. ACM , 66(6):64--72, 2023. DOI: https://doi.org/10.1145/3560469

    2023 doi

  6. [15]

    Another look at graph coloring via propositional satisfiability

    Allen Van Gelder. Another look at graph coloring via propositional satisfiability. Discret. Appl. Math. , 156(2):230--243, 2008. DOI: https://doi.org/10.1016/J.DAM.2006.07.016

    2008 doi

  7. [16]

    The PACE 2022 parameterized algorithms and computational experiments challenge: Directed feedback vertex set

    Ernestine Gro mann, Tobias Heuer, Christian Schulz, and Darren Strash. The PACE 2022 parameterized algorithms and computational experiments challenge: Directed feedback vertex set. In Proceedings of IPEC 2022 , volume 249 of LIPIcs , pages 26:1--26:18. Schloss Dagstuhl - Leibn...

    2022 doi

  8. [17]

    Holger H. Hoos. An adaptive noise mechanism for walksat. In Proceedings of the Eighteenth National Conference on Artificial Intelligence and Fourteenth Conference on Innovative Applications of Artificial Intelligence, July 28 - August 1, 2002, Edmonton, Alberta, Canada , pages...

    2002

  9. [18]

    PySAT: A Python toolkit for prototyping with SAT oracles

    Alexey Ignatiev, Antonio Morgado, and Joao Marques - Silva. PySAT: A Python toolkit for prototyping with SAT oracles. In SAT , pages 428--437, 2018. DOI: https://doi.org/10.1007/978-3-319-94144-8_26

    2018 doi

  10. [19]

    Towards universally accessible SAT technology

    Alexey Ignatiev, Zi Li Tan, and Christos Karamanos. Towards universally accessible SAT technology. In 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024, August 21-24, 2024, Pune, India , volume 305 of LIPIcs , pages 16:1--16:11. Schlo...

    2024 doi

  11. [20]

    On the quest for an acyclic graph

    Mikol \' a s Janota, Radu Grigore, and Vasco Manquinho. On the quest for an acyclic graph. In Proceedings of the 24th RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion 2017, Bari, Italy, November 14-15, 2017 ...

    2017

  12. [21]

    A survey on large language models for code generation

    Juyong Jiang, Fan Wang, Jiasi Shen, Sungju Kim, and Sunghun Kim. A survey on large language models for code generation. CoRR , abs/2406.00515, 2024. DOI: https://doi.org/10.48550/ARXIV.2406.00515

    2024 doi arXiv

  13. [22]

    Richard M. Karp. Reducibility among combinatorial problems. In Complexity of Computer Computations 1972 , The IBM Research Symposia Series, pages 85--103. Plenum Press, New York, 1972. DOI: https://doi.org/10.1007/978-1-4684-2001-2\_9

    1972 doi

  14. [23]

    PACE solver description: Dager - cutting out cycles with maxsat

    Rafael Kiesel and Andr \' e Schidler. PACE solver description: Dager - cutting out cycles with maxsat. In Proceedings of IPEC 2022 , volume 249 of LIPIcs , pages 32:1--32:4. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2022. DOI: https://doi.org/10.4230/LIPICS.IPEC.2022.32

    2022 doi

  15. [24]

    A dynamic MaxSAT -based approach to directed feedback vertex sets

    Rafael Kiesel and Andr \' e Schidler. A dynamic MaxSAT -based approach to directed feedback vertex sets. In Proceedings of the Symposium on Algorithm Engineering and Experiments, ALENEX 2023, Florence, Italy, January 22-23, 2023 , pages 39--52. SIAM , 2023. DOI: https://doi.or...

    2023 doi

  16. [25]

    Satisfying versus falsifying in local search for satisfiability - (poster presentation)

    Chu Min Li and Yu Li. Satisfying versus falsifying in local search for satisfiability - (poster presentation). In Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings , volume 7317 of Lecture...

    2012 doi

  17. [26]

    Yujia Li, David H. Choi, Junyoung Chung, Nate Kushman, Julian Schrittwieser, R \' e mi Leblond, Tom Eccles, James Keeling, Felix Gimeno, Agustin Dal Lago, Thomas Hubert, Peter Choy, Cyprien de Masson d'Autume, Igor Babuschkin, Xinyun Chen, Po - Sen Huang, Johannes Welbl, Sven ...

    2022 doi arXiv

  18. [27]

    Conflict-driven clause learning SAT solvers

    Jo \ a o Marques - Silva, In \^ e s Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers. In Handbook of Satisfiability - Second Edition , volume 336 of Frontiers in Artificial Intelligence and Applications , pages 133--182. IOS Press, 2021. DOI: https://doi.or...

    2021 doi

  19. [28]

    McAllester, Bart Selman, and Henry A

    David A. McAllester, Bart Selman, and Henry A. Kautz. Evidence for invariants in local search. In Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, AAAI 97, IAAI 97, July 27-31,...

    1997

  20. [29]

    Learning optimal decision trees with SAT

    Nina Narodytska, Alexey Ignatiev, Filipe Pereira, and Joao Marques-Silva. Learning optimal decision trees with SAT . In Proceedings of IJCAI 2018 , pages 1362--1368. ijcai.org, 7 2018. DOI: https://doi.org/10.24963/ijcai.2018/189

    2018 doi

  21. [30]

    Codegen: An open large language model for code with multi-turn program synthesis

    Erik Nijkamp, Bo Pang, Hiroaki Hayashi, Lifu Tu, Huan Wang, Yingbo Zhou, Silvio Savarese, and Caiming Xiong. Codegen: An open large language model for code with multi-turn program synthesis. In ICLR . OpenReview.net, 2023

    2023

  22. [31]

    Olson, William La Cava, Patryk Orzechowski, Ryan J

    Randal S. Olson, William La Cava, Patryk Orzechowski, Ryan J. Urbanowicz, and Jason H. Moore. PMLB : a large benchmark suite for machine learning evaluation and comparison. BioData Mining , 10(1):36, Dec 2017. DOI: https://doi.org/10.1186/s13040-017-0154-4

    2017 doi

  23. [32]

    SAT -based decision tree learning for large data sets

    Andr \' e Schidler and Stefan Szeider. SAT -based decision tree learning for large data sets. J. Artif. Intell. Res. , 80:875--918, 2024. DOI: https://doi.org/10.1613/JAIR.1.15956

    2024 doi

  24. [33]

    Extracting problem structure with LLMs for optimized SAT local search, January 2025

    André Schidler and Stefan Szeider. Extracting problem structure with LLMs for optimized SAT local search, January 2025. DOI: https://doi.org/10.5281/zenodo.14732109

    2025 doi

  25. [34]

    Levesque, and David G

    Bart Selman, Hector J. Levesque, and David G. Mitchell. A new method for solving hard satisfiability problems. In Proceedings of the 10th National Conference on Artificial Intelligence, San Jose, CA, USA, July 12-16, 1992 , pages 440--446. AAAI Press / The MIT Press, 1992. URL...

    1992

  26. [35]

    Kautz, and Bram Cohen

    Bart Selman, Henry A. Kautz, and Bram Cohen. Noise strategies for improving local search. In Proceedings of the 12th National Conference on Artificial Intelligence, Seattle, WA, USA, July 31 - August 4, 1994, Volume 1 , pages 337--343. AAAI Press / The MIT Press, 1994. URL: ht...

    1994

  27. [36]

    Daniel Selsam and Nikolaj S. Bj rner. Guiding high-performance SAT solvers with unsat-core predictions. In Mikol \' a s Janota and In \^ e s Lynce, editors, Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal...

    2019 doi

  28. [37]

    McIlraith

    Pouya Shati, Eldan Cohen, and Sheila A. McIlraith. SAT -based approach for learning optimal decision trees with non-binary features. In CP , volume 210 of LIPIcs , pages 50:1--50:16. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2021. DOI: https://doi.org/10.4230/LIP...

    2021 doi

  29. [38]

    Marques Silva and Karem A

    Jo \ a o P. Marques Silva and Karem A. Sakallah. GRASP - a new search algorithm for satisfiability. In Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 1996, San Jose, CA, USA, November 10-14, 1996 , pages 220--227. IEEE Computer Societ...

    1996

  30. [39]

    Cryptominisat 5.6.8

    Mate Soos. Cryptominisat 5.6.8. In Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions , pages 37--38, 2020

    2020

  31. [40]

    A solution-driven multilevel approach for graph coloring

    Wen Sun, Jin - Kao Hao, Yuhao Zang, and Xiangjing Lai. A solution-driven multilevel approach for graph coloring. Appl. Soft Comput. , 104:107174, 2021. DOI: https://doi.org/10.1016/J.ASOC.2021.107174

    2021

  32. [41]

    MCP -solver: Integrating language models with constraint programming systems

    Stefan Szeider. MCP -solver: Integrating language models with constraint programming systems. CoRR , abs/2501.00539, 2024. DOI: https://doi.org/10.48550/ARXIV.2501.00539

    2024 doi arXiv

  33. [42]

    Learning optimal classification trees using a binary linear program formulation

    Sicco Verwer and Yingqian Zhang. Learning optimal classification trees using a binary linear program formulation. In Proceedings of AAAI 2019 , pages 1625--1632. AAAI Press, 2019. DOI: https://doi.org/10.1609/aaai.v33i01.33011624

    2019 doi

  34. [43]

    Generating streamlining constraints with large language models

    Florentina Voboril, Vaidyanathan Peruvemba Ramaswamy, and Stefan Szeider. Generating streamlining constraints with large language models. CoRR , abs/2408.10268, 2024. DOI: https://doi.org/10.48550/ARXIV.2408.10268

    2024 doi

  35. [44]

    Realtime generation of streamliners with large language models

    Florentina Voboril, Vaidyanathan Peruvemba Ramaswamy, and Stefan Szeider. Realtime generation of streamliners with large language models. NSE 2025, the First International Workshop on Neuro-Symbolic Software Engineering (May 3, 2025), affiliated with ICSE 2025, the IEEE/ACM In...

    2025

  36. [45]

    Learning local search heuristics for boolean satisfiability

    Emre Yolcu and Barnab \' a s P \' o czos. Learning local search heuristics for boolean satisfiability. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d'Alch \' e - Buc, Emily B. Fox, and Roman Garnett, editors, Advances in Neural Information Processing Syste...

    2019

  37. [46]

    A spin glass approach to the directed feedback vertex set problem

    Hai-Jun Zhou. A spin glass approach to the directed feedback vertex set problem. Journal of Statistical Mechanics: Theory and Experiment , 2016(7):073303, 2016. URL: https://doi.org/10.1088/1742-5468/2016/07/073303

    2016 doi

  38. [47]

    write newline

    " write newline "" before.all 'output.state := FUNCTION format.doi doi empty "" " DOI: https://doi.org/" doi * "" * if FUNCTION format.url url empty "" " URL: " url * "" * if FUNCTION fin.entry doi empty url empty add.period write add.period write newline format.url write if a...

Pith tools

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