Learning Branching Heuristics for Propositional Model Counting
Authors: Pashootan Vaezipoor, Gil Lederman, Yuhuai Wu, Chris Maddison, Roger B Grosse, Sanjit A. Seshia, Fahiem Bacchus12427-12435
AAAI 2021 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We experimentally show that our method reduces the step count on similarly distributed held-out instances and generalizes to much larger instances from the same problem family. It is able to achieve these results on a number of different problem families having very different structures. In addition to step count improvements, Neuro# can also achieve orders of magnitude wall-clock speedups over the vanilla solver on larger instances in some problem families, despite the runtime overhead of querying the model. |
| Researcher Affiliation | Academia | 1 University of Toronto 2 UC Berkeley 3 Vector Institute |
| Pseudocode | Yes | Algorithm 1 Component Caching DPLL |
| Open Source Code | Yes | Our code and the extended version of the paper (with the appendix) are available at: github.com/NeuroSharp. |
| Open Datasets | No | The paper describes the generation process for the datasets used in experiments and mentions sampling instances for training ('For each dataset, we sampled 1,800 instances for training...'). However, it does not provide concrete access (link, DOI, specific repository) to the generated training datasets themselves, only descriptions of their generation process (which is further detailed in Appendix B). |
| Dataset Splits | No | The paper states 'For each dataset, we sampled 1,800 instances for training and 200 for testing.' It does not mention a separate validation split. |
| Hardware Specification | No | The paper does not provide specific hardware details such as GPU or CPU models, memory, or specific cloud computing instance types used for running the experiments. |
| Software Dependencies | No | The paper mentions software components like 'Adam optimizer' and types of neural networks (GNNs, MLP, GIN) but does not provide specific version numbers for any libraries, frameworks (e.g., PyTorch, TensorFlow), or programming languages used. |
| Experiment Setup | Yes | We trained for 1000 ES iterations. At each iteration, we sampled 8 formulas and 48 perturbations (σ = 0.02)... All episodes, unless otherwise mentioned, were capped at 1k steps during training and 100k during testing. The agent received a negative reward of rpenalty = 10 4 at each step. We used the Adam optimizer (Kingma and Ba 2015) with default hyperparameters, a learning rate of η = 0.01 and a weight decay of 0.005. GNN messages were implemented by an MLP with Re LU non-linearity. The size of literal and clause embeddings were 32 and the dimensionality of C2L (resp. L2C) messages was 32 32 32 (resp. 64 32 32). We used T = 2 message passing iterations and final literal embeddings were passed through the MLP policy network of dimensions 32 256 64 1 to get the final score. When using the extra time feature, the first dimension of the decision layer was 33 instead of 32. The initial (T = 0) embeddings of both literals and clauses were trainable model parameters. |