Learning Local Search Heuristics for Boolean Satisfiability
Authors: Emre Yolcu, Barnabas Poczos
NeurIPS 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We present an approach to learn SAT solver heuristics from scratch through deep reinforcement learning with a curriculum. Although we do not aim to compete with the state-of-the-art SAT solvers in run time, we demonstrate that the learned heuristics allow us to find satisfying assignments in fewer steps compared to a generic heuristic, and we provide analysis of our results through experiments. |
| Researcher Affiliation | Academia | Emre Yolcu Carnegie Mellon University eyolcu@cs.cmu.edu Barnabás Póczos Carnegie Mellon University bapoczos@cs.cmu.edu |
| Pseudocode | Yes | Algorithm 1 Local search for SAT; Algorithm 2 Policy gradient training for local search |
| Open Source Code | Yes | Our implementation is available at https://github.com/emreyolcu/sat. |
| Open Datasets | No | The paper describes generating problem instances from various distributions (e.g., random 3-SAT, clique detection) using tools like CNFgen [30] and Minisat [15]. However, it does not provide direct access (URL, DOI, repository) to specific pre-generated datasets or cite them as established public benchmarks. |
| Dataset Splits | No | The paper describes sampling formulas and initial assignments for training and evaluation within a curriculum learning setup. While it distinguishes between training on smaller distributions and evaluating on larger ones, it does not provide specific dataset split percentages or sample counts (e.g., '80/10/10 split') for validation purposes. |
| Hardware Specification | No | The paper does not specify any hardware details such as CPU, GPU models, or cloud computing instances used for running the experiments. |
| Software Dependencies | No | The paper mentions software tools like CNFgen [30] and Minisat [15] that were used to create problem instances. However, it does not provide specific version numbers for these or any other software dependencies, such as libraries or programming languages, necessary for reproducibility. |
| Experiment Setup | No | The paper states, 'Remaining hyperparameters are described in Appendix A.' Since Appendix A is not part of the main text, the specific experimental setup details are not provided within the main body of the paper. |