Data

Tools

Indexes

Applications

Experiments

Open Source Science

https://github.com/alexeyev/graphqsat-cuda-11.3

Using GNN and DQN to find a baetter branching heuristic for a CDCL Solver

https://github.com/alexeyev/graphqsat-cuda-11.3

Science Score: 10.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • ○
    CITATION.cff file
  • ○
    codemeta.json file
  • ○
    .zenodo.json file
  • ○
    DOI references
  • ✓
    Academic publication links
    Links to: arxiv.org
  • ○
    Academic email domains
  • ○
    Institutional organization owner
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (9.2%) to scientific vocabulary
Last synced: 9 months ago · JSON representation

Repository

Using GNN and DQN to find a baetter branching heuristic for a CDCL Solver

Basic Info
  • Host: GitHub
  • Owner: alexeyev
  • License: other
  • Language: C++
  • Default Branch: main
  • Size: 223 KB
Statistics
  • Stars: 0
  • Watchers: 0
  • Forks: 0
  • Open Issues: 0
  • Releases: 0
Fork of NVIDIA/GraphQSat
Created over 3 years ago · Last pushed over 3 years ago

https://github.com/alexeyev/GraphQSat-CUDA-11.3/blob/main/ 

# GQSAT 

Can Q-learning with Graph Networks learn a Generalizable Branching Heuristic for a SAT solver?

## Why another fork?

To make stuff work with fresher versions of... everything.

## How to add metadata for evaluation

```python3 add_metadata.py --eval-problems-paths ```

## How to train

```./train.sh```

## How to evaluate 

* add the path to the model to the script first
* choose the evaluation dataset
* ```./evaluate.sh```


## How to build a solver (you need this only if you changed the c++ code)

Run `make && make python-wrap` in the minisat folder.

## How to build swig code (if you changed minisat-python interface, e.g. in GymSolver.i)

Go to minisat/minisat/gym, run `swig -fastdispatch -c++ -python3 GymSolver.i` and then repeat the building procedure from the previous step.

## Individual Contributor License Agreement

Please fill out the following CLA and email to sgodil@nvidia.com:  https://www.apache.org/licenses/icla.pdf

## Cite

```
@inproceedings{kurin2019improving,
  title={Can Q-Learning with Graph Networks Learn a Generalizable Branching Heuristic for a SAT Solver?},
  author={Kurin, Vitaly and Godil, Saad and Whiteson, Shimon and Catanzaro, Bryan},
  booktitle = {Advances in Neural Information Processing Systems 32},
  year={2020}
}
```

## Acknowledgements

We would like to thank [Fei Wang](https://github.com/feiwang3311/minisat) whose initial implementation of the environment we used as a start, and the creators of [Minisat](https://github.com/niklasso/minisat) on which it is based on.
We would also like to thank the creators of [Pytorch Geometric](https://github.com/rusty1s/pytorch_geometric) whose 
MetaLayer and [Graph Nets](https://arxiv.org/abs/1806.01261) implementation we built upon.

Owner

  • Name: Anton Alekseev
  • Login: alexeyev
  • Kind: user

GitHub Events

Total
Last Year