Using deep learning to construct stochastic local search SAT solvers with performance bounds

Jens Eisert; Maximilian J. Kramer; Paul Boes

arxiv: 2309.11452 · v3 · submitted 2023-09-20 · 💻 cs.AI · math.OC

Using deep learning to construct stochastic local search SAT solvers with performance bounds

Maximilian J. Kramer , Paul Boes , Jens Eisert This is my paper

Pith reviewed 2026-05-24 06:21 UTC · model grok-4.3

classification 💻 cs.AI math.OC

keywords Boolean satisfiabilitystochastic local searchgraph neural networksmachine learning oraclesSAT solversperformance guaranteesdeep learning

0 comments

The pith

Graph neural networks can serve as oracles to improve stochastic local search SAT solvers with performance guarantees.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper aims to link recent theoretical conditions for efficient stochastic local search SAT solving with machine learning by training graph neural networks to act as the required oracles. These oracles supply instance-specific distribution samples that the theory needs for fast solving. The resulting solvers are evaluated on random and pseudo-industrial SAT instances and show reductions in step counts plus higher numbers of solved problems. A sympathetic reader would care because the work offers a concrete route to SAT solvers that carry both practical speed and theoretical performance bounds.

Core claim

Training graph neural networks to generate instance-specific distributions lets stochastic local search algorithms solve SAT instances more efficiently while retaining the performance guarantees from prior oracle-based theoretical results.

What carries the argument

Graph neural networks trained to output distributions that serve as oracles for guiding variable flips in stochastic local search.

If this is right

SLS solvers equipped with GNN oracles require fewer steps to reach solutions on the tested instances.
A higher fraction of random and pseudo-industrial SAT instances are solved compared with standard SLS baselines.
The method directly imports prior theoretical efficiency conditions into a learned solver without manual heuristic design.
Purpose-trained solvers can combine practical performance with explicit performance bounds.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same oracle-learning pattern could be applied to other NP-complete problems that possess comparable theoretical oracle conditions.
One could directly audit whether the learned distributions satisfy the precise probabilistic requirements of the underlying theory.
Replacing the GNN with other model families might preserve the performance gains while changing training cost.

Load-bearing premise

The distributions produced by the trained graph neural network meet the exact conditions specified in the theoretical results for efficient SLS solving.

What would settle it

A measurement showing that the GNN-sampled distributions deviate from the mathematical requirements of the cited oracle theorems, with the performance gains disappearing as a result.

Figures

Figures reproduced from arXiv: 2309.11452 by Jens Eisert, Maximilian J. Kramer, Paul Boes.

**Figure 2.** Figure 2: Example for the encoding of a single clause into LCG representation. [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗

**Figure 3.** Figure 3: Simple illustration of the “hardness regimes” for [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗

**Figure 4.** Figure 4: Benchmark of three different variants of the oracle-based MT algorithm, namely the uniform version, the [PITH_FULL_IMAGE:figures/full_fig_p009_4.png] view at source ↗

**Figure 5.** Figure 5: Benchmark of three different variants of the oracle-based WalkSAT, using the same plots as in Fig. 4 [PITH_FULL_IMAGE:figures/full_fig_p009_5.png] view at source ↗

**Figure 6.** Figure 6: Comparison of the MT algorithm when switching on and off the individual loss terms in the training of the [PITH_FULL_IMAGE:figures/full_fig_p010_6.png] view at source ↗

**Figure 7.** Figure 7: Comparison of the WalkSAT algorithm when switching on and off the individual loss terms in the training of [PITH_FULL_IMAGE:figures/full_fig_p010_7.png] view at source ↗

**Figure 8.** Figure 8: Benchmark of our ml-boosted version of the Moser-Tardos Resample algorithm (orange) against its uniform [PITH_FULL_IMAGE:figures/full_fig_p014_8.png] view at source ↗

**Figure 9.** Figure 9: Benchmark of our ml-boosted version of WalkSAT algorithm (green) against its uniform version (orange) a) + [PITH_FULL_IMAGE:figures/full_fig_p015_9.png] view at source ↗

read the original abstract

The Boolean Satisfiability problem (SAT), as the prototypical $\mathsf{NP}$-complete problem, is crucial in both theoretical computer science and practical applications. To address this problem, stochastic local search (SLS) algorithms, which iteratively and randomly update candidate assignments, present an important and theoretically well-studied class of solvers. Recent theoretical advancements have identified conditions under which SLS solvers efficiently solve SAT instances, provided they have access to suitable ``oracles'', i.e., instance-specific distribution samples. We propose leveraging machine learning models, particularly graph neural networks (GNN), as oracles to enhance the performance of SLS solvers. Our approach, evaluated on random and pseudo-industrial SAT instances, demonstrates a significant performance improvement regarding step counts and solved instances. Our work bridges theoretical results and practical applications, highlighting the potential of purpose-trained SAT solvers with performance guarantees.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper trains GNNs to serve as distribution oracles inside SLS SAT solvers so that existing theoretical runtime bounds might still apply, but the manuscript does not verify that the learned distributions meet the precise conditions those bounds require.

read the letter

The core move is to take prior oracle-based SLS results that guarantee efficient solving under certain distributional conditions and replace the oracle with a GNN trained on SAT instances. The authors then run the resulting hybrid on random and pseudo-industrial formulas and report fewer steps and more solved instances than the baselines they compare against. That specific combination of learned oracle plus retained theoretical framing is not in the earlier literature they cite, so the proposal itself is new.

Referee Report

2 major / 1 minor

Summary. The paper proposes training graph neural networks (GNNs) to serve as oracles that supply instance-specific distribution samples for stochastic local search (SLS) SAT solvers. It invokes prior theoretical results establishing conditions under which such oracles yield efficient SLS solving, reports empirical gains in step counts and solved instances on random and pseudo-industrial benchmarks, and claims to bridge theory and practice by producing purpose-trained solvers with performance guarantees.

Significance. If the GNN outputs were shown to satisfy the precise distributional conditions required by the cited oracle-based SLS theory, the result would be significant: it would supply the first practical, learned oracles that inherit formal performance bounds rather than relying on heuristics. The use of standard supervised training on external theoretical results (rather than circular fitting) and the evaluation across both random and pseudo-industrial instances are positive features.

major comments (2)

[Abstract and theoretical background sections] The central claim of 'purpose-trained SAT solvers with performance guarantees' (abstract) rests on the GNN satisfying the exact oracle conditions (sufficient bias toward satisfying assignments, coverage properties, etc.) from the cited SLS theory for the performance bounds to transfer. No analysis, verification procedure, or empirical check is supplied showing that the learned sampling distribution meets those conditions rather than functioning as an effective heuristic; this gap is load-bearing for the theoretical bridge.
[Evaluation section] The empirical evaluation reports gains in step counts and solved instances but supplies no quantitative metrics, baseline comparisons with error bars, or description of how the learned distribution was checked against the oracle conditions invoked in the theory sections. This leaves the practical improvement unevaluated relative to the claimed guarantees.

minor comments (1)

[Method] Notation for the GNN output distribution and its relation to the oracle sampling process should be made explicit with an equation or pseudocode block.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments and for recognizing the positive aspects of the approach. Below we respond point-by-point to the major comments.

read point-by-point responses

Referee: [Abstract and theoretical background sections] The central claim of 'purpose-trained SAT solvers with performance guarantees' (abstract) rests on the GNN satisfying the exact oracle conditions (sufficient bias toward satisfying assignments, coverage properties, etc.) from the cited SLS theory for the performance bounds to transfer. No analysis, verification procedure, or empirical check is supplied showing that the learned sampling distribution meets those conditions rather than functioning as an effective heuristic; this gap is load-bearing for the theoretical bridge.

Authors: We agree that strict transfer of the performance bounds requires the learned distribution to satisfy the precise conditions stated in the cited oracle-based SLS theory. Our GNN training procedure is explicitly motivated by those conditions: it uses supervised labels derived from satisfying assignments to induce the necessary bias and coverage. Nevertheless, the manuscript does not contain an explicit verification procedure or empirical diagnostic confirming that the output distribution meets the conditions exactly (as opposed to providing a useful heuristic). This is a substantive gap. We will revise the theoretical background and evaluation sections to add (i) a clearer statement of which conditions the training targets and (ii) post-training diagnostics measuring the empirical bias of the GNN samples toward satisfying assignments on held-out instances. A fully rigorous proof that every output distribution satisfies the conditions exactly would require additional theoretical work beyond the present scope. revision: partial
Referee: [Evaluation section] The empirical evaluation reports gains in step counts and solved instances but supplies no quantitative metrics, baseline comparisons with error bars, or description of how the learned distribution was checked against the oracle conditions invoked in the theory sections. This leaves the practical improvement unevaluated relative to the claimed guarantees.

Authors: The current manuscript presents aggregate improvements but indeed omits detailed quantitative reporting (means, standard deviations, error bars) and explicit baseline comparisons with statistical detail. We will revise the evaluation section to include: average step counts and solved-instance percentages with standard errors over repeated runs, direct comparisons against standard SLS solvers (e.g., WalkSAT, probSAT) with error bars, and a short subsection describing the bias diagnostics mentioned above. These additions will allow readers to assess the practical gains relative to the theoretical claims. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation relies on external theory and empirical evaluation

full rationale

The paper trains GNNs to act as oracles supplying instance-specific distributions for SLS solvers, then reports empirical gains in step counts and solved instances on random and pseudo-industrial benchmarks. It invokes prior (non-self) theoretical results on oracle conditions for performance bounds but does not reduce any claimed prediction or bound to a fitted parameter, self-definition, or self-citation chain by construction. No equations or steps equate outputs to inputs via renaming or ansatz smuggling; the work is self-contained as standard supervised learning plus external citations, yielding a normal non-circular finding.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the existence of prior theoretical conditions under which an SLS solver is efficient given suitable oracles; the paper adds a learned approximation to those oracles but does not introduce new free parameters, axioms, or invented entities beyond standard GNN training.

axioms (1)

domain assumption Prior theoretical results establish that SLS solvers solve SAT instances efficiently when supplied with suitable instance-specific distribution samples (the oracle).
Invoked in the abstract when the authors state that SLS solvers are efficient given suitable oracles.

pith-pipeline@v0.9.0 · 5676 in / 1221 out tokens · 16565 ms · 2026-05-24T06:21:32.691853+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We propose leveraging machine learning models, particularly graph neural networks (GNN), as oracles to enhance the performance of SLS solvers... Lovász Local loss... cross entropy... thermal distribution γ_β,ϕ
IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

if there exists a map μ : [m] → [0, ∞) such that... PO(j|ϕ) · Πj′∈Γ+(j)(1 + μ(j′)) ≤ μ(j)

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

35 extracted references · 35 canonical work pages · 1 internal anchor

[1]

Stephen A. Cook. The complexity of theorem-proving procedures. In Proceedings of the Third Annual ACM Symposium on Theory of Computing, STOC ’71, pages 151–158, New York, NY , USA, 1971. Association for Computing Machinery

work page 1971
[2]

L. A. Levin. Problems of information transmission. 1973

work page 1973
[3]

Machine learning methods in solving the boolean satisfiability problem, 2022

Wenxuan Guo, Junchi Yan, Hui-Ling Zhen, Xijun Li, Mingxuan Yuan, and Yaohui Jin. Machine learning methods in solving the boolean satisfiability problem, 2022

work page 2022
[4]

Graph neural networks and boolean satisfiability, 2017

Benedikt Bünz and Matthew Lamm. Graph neural networks and boolean satisfiability, 2017

work page 2017
[5]

Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. Learning a sat solver from single-bit supervision, 2019

work page 2019
[6]

Goal- aware neural SAT solver

Emils Ozolins, Karlis Freivalds, Andis Draguns, Eliza Gaile, Ronalds Zakovskis, and Sergejs Kozlovics. Goal- aware neural SAT solver. In 2022 International Joint Conference on Neural Networks (IJCNN) . IEEE, jul 2022

work page 2022
[7]

Guiding high-performance sat solvers with unsat-core predictions, 2019

Daniel Selsam and Nikolaj Bjørner. Guiding high-performance sat solvers with unsat-core predictions, 2019

work page 2019
[8]

Neural heuristics for sat solving, 2020

Sebastian Jaszczur, Michał Łuszczyk, and Henryk Michalewski. Neural heuristics for sat solving, 2020

work page 2020
[9]

Enhancing sat solvers with glue variable predictions, 2020

Jesse Michael Han. Enhancing sat solvers with glue variable predictions, 2020

work page 2020
[10]

Learning local search heuristics for boolean satisfiability

Emre Yolcu and Barnabas Poczos. Learning local search heuristics for boolean satisfiability. In H. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alché-Buc, E. Fox, and R. Garnett, editors, Advances in Neural Information Processing Systems, volume 32. Curran Associates, Inc., 2019

work page 2019
[11]

NLocalSAT: Boosting local search with solution prediction

Wenjie Zhang, Zeyu Sun, Qihao Zhu, Ge Li, Shaowei Cai, Yingfei Xiong, and Lu Zhang. NLocalSAT: Boosting local search with solution prediction. In Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence. International Joint Conferences on Artificial Intelligence Organization, jul 2020

work page 2020
[12]

Robin A. Moser. A constructive proof of the lovasz local lemma, 2008

work page 2008
[13]

Moser and Gábor Tardos

Robin A. Moser and Gábor Tardos. A constructive proof of the general lovasz local lemma, 2009

work page 2009
[14]

Harris and Aravind Srinivasan

David G. Harris and Aravind Srinivasan. Algorithmic and enumerative aspects of the moser-tardos distribution, 2017

work page 2017
[15]

Beyond the lovasz local lemma: Point to set correlations and their algorithmic applications, 2020

Dimitris Achlioptas, Fotis Iliopoulos, and Alistair Sinclair. Beyond the lovasz local lemma: Point to set correlations and their algorithmic applications, 2020. 11 Using deep learning to construct Stochastic Local Search SAT solvers with performance bounds

work page 2020
[16]

Battaglia, Razvan Pascanu, Matthew Lai, Danilo Rezende, and Koray Kavukcuoglu

Peter W. Battaglia, Razvan Pascanu, Matthew Lai, Danilo Rezende, and Koray Kavukcuoglu. Interaction networks for learning about objects, relations and physics, 2016

work page 2016
[17]

Solving mixed integer programs using neural networks, 2020

Vinod Nair, Sergey Bartunov, Felix Gimeno, Ingrid von Glehn, Pawel Lichocki, Ivan Lobov, Brendan O’Donoghue, Nicolas Sonnerat, Christian Tjandraatmadja, Pengming Wang, Ravichandra Addanki, Tharindi Hapuarachchi, Thomas Keck, James Keeling, Pushmeet Kohli, Ira Ktena, Yujia Li, Oriol Vinyals, and Yori Zwols. Solving mixed integer programs using neural netwo...

work page 2020
[18]

Erd˝os and L

P. Erd˝os and L. Lovász. Problems and results on 3-chromatic hypergraphs and some related questions. Infinite and finite sets, 2:609–627, 1975

work page 1975
[19]

An algorithmic proof of the lovasz local lemma via resampling oracles, 2015

Nicholas Harvey and Jan V ondrak. An algorithmic proof of the lovasz local lemma via resampling oracles, 2015

work page 2015
[20]

Schöning

T. Schöning. A probabilistic algorithm for k-sat and constraint satisfaction problems. In 40th Annual Symposium on Foundations of Computer Science (Cat. No.99CB37039), pages 410–414, 1999

work page 1999
[21]

Papadimitriou

C.H. Papadimitriou. On selecting a satisfying truth assignment. In [1991] Proceedings 32nd Annual Symposium of Foundations of Computer Science, pages 163–169, 1991

work page 1991
[22]

Selman, H

B. Selman, H. Kautz, and B. Cohen. Local search strategies for satisfiability testing. In D. S. Johnson and M. A. Trick, editors, Cliques, Coloring, and Satisfiability: the Second DIMACS Implementation Challenge in Discrete Mathemathics and Theoretical Computer Science, volume 26, pages 521–532. American Mathematical Society, 1996

work page 1996
[23]

Choosing probability distributions for stochastic local search and the role of make versus break

Adrian Balint and Uwe Schöning. Choosing probability distributions for stochastic local search and the role of make versus break. volume 7317, pages 16–29, 06 2012

work page 2012
[24]

Battaglia, Jessica B

Peter W. Battaglia, Jessica B. Hamrick, Victor Bapst, Alvaro Sanchez-Gonzalez, Vinicius Zambaldi, Mateusz Malinowski, Andrea Tacchetti, David Raposo, Adam Santoro, Ryan Faulkner, Caglar Gulcehre, Francis Song, Andrew Ballard, Justin Gilmer, George Dahl, Ashish Vaswani, Kelsey Allen, Charles Nash, Victoria Langston, Chris Dyer, Nicolas Heess, Daan Wierstra...

work page 2018
[25]

Jimmy Lei Ba, Jamie Ryan Kiros, and Geoffrey E. Hinton. Layer normalization, 2016

work page 2016
[26]

Deep Learning using Rectified Linear Units (ReLU)

Abien Fred Agarap. Deep learning using rectified linear units (relu). arXiv preprint arXiv:1803.08375, 2018

work page internal anchor Pith review Pith/arXiv arXiv 2018
[27]

Robin A. Moser. Exact Algorithms for Constraint Satisfaction Problems. PhD thesis, 2012

work page 2012
[28]

The Moser- Tardos Resample algorithm: Where is the limit? (an experimental inquiry), pages 159–171

Jan Dean Catarata, Scott Corbett, Harry Stern, Mario Szegedy, Tomas Vyskocil, and Zheng Zhang. The Moser- Tardos Resample algorithm: Where is the limit? (an experimental inquiry), pages 159–171

work page
[29]

Critical behavior in the satisfiability of random boolean expressions

Scott Kirkpatrick and Bart Selman. Critical behavior in the satisfiability of random boolean expressions. Science, 264(5163):1297–1301, 1994

work page 1994
[30]

MassimoLauria/cnfgen: CNFgen registered with Zenodo, November 2019

Massimo Lauria, Jan Elffers, Jakob Nordström, and Marc Vinyals. MassimoLauria/cnfgen: CNFgen registered with Zenodo, November 2019

work page 2019
[31]

On the glucose sat solver

Gilles Audemard and Laurent Simon. On the glucose sat solver. International Journal on Artificial Intelligence Tools, 27:1840001, 02 2018

work page 2018
[32]

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

work page 2018
[33]

Satenstein: Automatically building local search sat solvers from components

Ashiqur Khudabukhsh, Lin Xu, Holger Hoos, and Kevin Leyton-Brown. Satenstein: Automatically building local search sat solvers from components. volume 232, pages 517–524, 01 2009

work page 2009
[34]

JAX: composable transforma- tions of Python+NumPy programs, 2018

James Bradbury, Roy Frostig, Peter Hawkins, Matthew James Johnson, Chris Leary, Dougal Maclaurin, George Necula, Adam Paszke, Jake VanderPlas, Skye Wanderman-Milne, and Qiao Zhang. JAX: composable transforma- tions of Python+NumPy programs, 2018

work page 2018
[35]

Jraph: A library for graph neural networks in jax., 2020

Jonathan Godwin*, Thomas Keck*, Peter Battaglia, Victor Bapst, Thomas Kipf, Yujia Li, Kimberly Stachenfeld, Petar Veliˇckovi´c, and Alvaro Sanchez-Gonzalez. Jraph: A library for graph neural networks in jax., 2020. 12 Using deep learning to construct Stochastic Local Search SAT solvers with performance bounds A Appendix A.1 Evaluating the loss in practice...

work page 2020

[1] [1]

Stephen A. Cook. The complexity of theorem-proving procedures. In Proceedings of the Third Annual ACM Symposium on Theory of Computing, STOC ’71, pages 151–158, New York, NY , USA, 1971. Association for Computing Machinery

work page 1971

[2] [2]

L. A. Levin. Problems of information transmission. 1973

work page 1973

[3] [3]

Machine learning methods in solving the boolean satisfiability problem, 2022

Wenxuan Guo, Junchi Yan, Hui-Ling Zhen, Xijun Li, Mingxuan Yuan, and Yaohui Jin. Machine learning methods in solving the boolean satisfiability problem, 2022

work page 2022

[4] [4]

Graph neural networks and boolean satisfiability, 2017

Benedikt Bünz and Matthew Lamm. Graph neural networks and boolean satisfiability, 2017

work page 2017

[5] [5]

Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. Learning a sat solver from single-bit supervision, 2019

work page 2019

[6] [6]

Goal- aware neural SAT solver

Emils Ozolins, Karlis Freivalds, Andis Draguns, Eliza Gaile, Ronalds Zakovskis, and Sergejs Kozlovics. Goal- aware neural SAT solver. In 2022 International Joint Conference on Neural Networks (IJCNN) . IEEE, jul 2022

work page 2022

[7] [7]

Guiding high-performance sat solvers with unsat-core predictions, 2019

Daniel Selsam and Nikolaj Bjørner. Guiding high-performance sat solvers with unsat-core predictions, 2019

work page 2019

[8] [8]

Neural heuristics for sat solving, 2020

Sebastian Jaszczur, Michał Łuszczyk, and Henryk Michalewski. Neural heuristics for sat solving, 2020

work page 2020

[9] [9]

Enhancing sat solvers with glue variable predictions, 2020

Jesse Michael Han. Enhancing sat solvers with glue variable predictions, 2020

work page 2020

[10] [10]

Learning local search heuristics for boolean satisfiability

Emre Yolcu and Barnabas Poczos. Learning local search heuristics for boolean satisfiability. In H. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alché-Buc, E. Fox, and R. Garnett, editors, Advances in Neural Information Processing Systems, volume 32. Curran Associates, Inc., 2019

work page 2019

[11] [11]

NLocalSAT: Boosting local search with solution prediction

Wenjie Zhang, Zeyu Sun, Qihao Zhu, Ge Li, Shaowei Cai, Yingfei Xiong, and Lu Zhang. NLocalSAT: Boosting local search with solution prediction. In Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence. International Joint Conferences on Artificial Intelligence Organization, jul 2020

work page 2020

[12] [12]

Robin A. Moser. A constructive proof of the lovasz local lemma, 2008

work page 2008

[13] [13]

Moser and Gábor Tardos

Robin A. Moser and Gábor Tardos. A constructive proof of the general lovasz local lemma, 2009

work page 2009

[14] [14]

Harris and Aravind Srinivasan

David G. Harris and Aravind Srinivasan. Algorithmic and enumerative aspects of the moser-tardos distribution, 2017

work page 2017

[15] [15]

Beyond the lovasz local lemma: Point to set correlations and their algorithmic applications, 2020

Dimitris Achlioptas, Fotis Iliopoulos, and Alistair Sinclair. Beyond the lovasz local lemma: Point to set correlations and their algorithmic applications, 2020. 11 Using deep learning to construct Stochastic Local Search SAT solvers with performance bounds

work page 2020

[16] [16]

Battaglia, Razvan Pascanu, Matthew Lai, Danilo Rezende, and Koray Kavukcuoglu

Peter W. Battaglia, Razvan Pascanu, Matthew Lai, Danilo Rezende, and Koray Kavukcuoglu. Interaction networks for learning about objects, relations and physics, 2016

work page 2016

[17] [17]

Solving mixed integer programs using neural networks, 2020

Vinod Nair, Sergey Bartunov, Felix Gimeno, Ingrid von Glehn, Pawel Lichocki, Ivan Lobov, Brendan O’Donoghue, Nicolas Sonnerat, Christian Tjandraatmadja, Pengming Wang, Ravichandra Addanki, Tharindi Hapuarachchi, Thomas Keck, James Keeling, Pushmeet Kohli, Ira Ktena, Yujia Li, Oriol Vinyals, and Yori Zwols. Solving mixed integer programs using neural netwo...

work page 2020

[18] [18]

Erd˝os and L

P. Erd˝os and L. Lovász. Problems and results on 3-chromatic hypergraphs and some related questions. Infinite and finite sets, 2:609–627, 1975

work page 1975

[19] [19]

An algorithmic proof of the lovasz local lemma via resampling oracles, 2015

Nicholas Harvey and Jan V ondrak. An algorithmic proof of the lovasz local lemma via resampling oracles, 2015

work page 2015

[20] [20]

Schöning

T. Schöning. A probabilistic algorithm for k-sat and constraint satisfaction problems. In 40th Annual Symposium on Foundations of Computer Science (Cat. No.99CB37039), pages 410–414, 1999

work page 1999

[21] [21]

Papadimitriou

C.H. Papadimitriou. On selecting a satisfying truth assignment. In [1991] Proceedings 32nd Annual Symposium of Foundations of Computer Science, pages 163–169, 1991

work page 1991

[22] [22]

Selman, H

B. Selman, H. Kautz, and B. Cohen. Local search strategies for satisfiability testing. In D. S. Johnson and M. A. Trick, editors, Cliques, Coloring, and Satisfiability: the Second DIMACS Implementation Challenge in Discrete Mathemathics and Theoretical Computer Science, volume 26, pages 521–532. American Mathematical Society, 1996

work page 1996

[23] [23]

Choosing probability distributions for stochastic local search and the role of make versus break

Adrian Balint and Uwe Schöning. Choosing probability distributions for stochastic local search and the role of make versus break. volume 7317, pages 16–29, 06 2012

work page 2012

[24] [24]

Battaglia, Jessica B

Peter W. Battaglia, Jessica B. Hamrick, Victor Bapst, Alvaro Sanchez-Gonzalez, Vinicius Zambaldi, Mateusz Malinowski, Andrea Tacchetti, David Raposo, Adam Santoro, Ryan Faulkner, Caglar Gulcehre, Francis Song, Andrew Ballard, Justin Gilmer, George Dahl, Ashish Vaswani, Kelsey Allen, Charles Nash, Victoria Langston, Chris Dyer, Nicolas Heess, Daan Wierstra...

work page 2018

[25] [25]

Jimmy Lei Ba, Jamie Ryan Kiros, and Geoffrey E. Hinton. Layer normalization, 2016

work page 2016

[26] [26]

Deep Learning using Rectified Linear Units (ReLU)

Abien Fred Agarap. Deep learning using rectified linear units (relu). arXiv preprint arXiv:1803.08375, 2018

work page internal anchor Pith review Pith/arXiv arXiv 2018

[27] [27]

Robin A. Moser. Exact Algorithms for Constraint Satisfaction Problems. PhD thesis, 2012

work page 2012

[28] [28]

The Moser- Tardos Resample algorithm: Where is the limit? (an experimental inquiry), pages 159–171

Jan Dean Catarata, Scott Corbett, Harry Stern, Mario Szegedy, Tomas Vyskocil, and Zheng Zhang. The Moser- Tardos Resample algorithm: Where is the limit? (an experimental inquiry), pages 159–171

work page

[29] [29]

Critical behavior in the satisfiability of random boolean expressions

Scott Kirkpatrick and Bart Selman. Critical behavior in the satisfiability of random boolean expressions. Science, 264(5163):1297–1301, 1994

work page 1994

[30] [30]

MassimoLauria/cnfgen: CNFgen registered with Zenodo, November 2019

Massimo Lauria, Jan Elffers, Jakob Nordström, and Marc Vinyals. MassimoLauria/cnfgen: CNFgen registered with Zenodo, November 2019

work page 2019

[31] [31]

On the glucose sat solver

Gilles Audemard and Laurent Simon. On the glucose sat solver. International Journal on Artificial Intelligence Tools, 27:1840001, 02 2018

work page 2018

[32] [32]

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

work page 2018

[33] [33]

Satenstein: Automatically building local search sat solvers from components

Ashiqur Khudabukhsh, Lin Xu, Holger Hoos, and Kevin Leyton-Brown. Satenstein: Automatically building local search sat solvers from components. volume 232, pages 517–524, 01 2009

work page 2009

[34] [34]

JAX: composable transforma- tions of Python+NumPy programs, 2018

James Bradbury, Roy Frostig, Peter Hawkins, Matthew James Johnson, Chris Leary, Dougal Maclaurin, George Necula, Adam Paszke, Jake VanderPlas, Skye Wanderman-Milne, and Qiao Zhang. JAX: composable transforma- tions of Python+NumPy programs, 2018

work page 2018

[35] [35]

Jraph: A library for graph neural networks in jax., 2020

Jonathan Godwin*, Thomas Keck*, Peter Battaglia, Victor Bapst, Thomas Kipf, Yujia Li, Kimberly Stachenfeld, Petar Veliˇckovi´c, and Alvaro Sanchez-Gonzalez. Jraph: A library for graph neural networks in jax., 2020. 12 Using deep learning to construct Stochastic Local Search SAT solvers with performance bounds A Appendix A.1 Evaluating the loss in practice...

work page 2020