dselsam / neurocore-public

NeuroCore: Guiding CDCL with Unsat-Core Predictions

NeuroCore

We train a simplified NeuroSAT architecture to directly predict the unsatisfiable cores of real problems, and modify MiniSat to periodically replace its variable activity scores with NeuroSAT's prediction of how likely they are to appear in an unsatisfiable core. Our modified MiniSat solves 10% more problems on SAT-COMP 2018 than the original does. Although MiniSat is no longer considered a state-of-the-art solver, our results nonetheless demonstrate the potential for NeuroSAT (and in particular, NeuroCore) to provide useful guidance to CDCL solvers on real problems.

More information can be found in the paper https://arxiv.org/abs/1903.04671.

Overview of repository

1. solver/: pybind11 module wrapping Z3, for generating training data.
2. python/gen_data.py: ray script to generate training data.
3. python/neurosat.py: simplified reimplementation of NeuroSAT.
4. python/train.py: distributed tensorflow script to train NeuroCore.
5. hybrids/glucose/: code to extend glucose with NeuroCore.
6. python/evaluate_cdcl.py: ray script for evaluating solvers on benchmarks.
7. weights/: the trained weights used for the experiments in the paper.

Dependencies

There are several dependencies. For now, we list the ones that cannot be easily installed with apt-get or pip3:

1. z3 (we used commit 773c61369480b6f031eb8fa98a7eb24bd52c7070)
2. drat-trim
3. eigen
4. pybind11
5. minisat
6. grpc

The code also uses a MariaDB database and an Azure storage account. Replace the fake credentials in auth.json.

Team

• Daniel Selsam, Microsoft Research, Stanford University
• Nikolaj Bjørner, Microsoft Research

neurocore-public's Issues

interact with solvers

Can you advise how to interact with the solvers to replace the EVSIDS score with the probability produced by neuroCore model?

gen_data.py assumes that sql table exist, no code to create them?

It looks like python/gen_data.py is assuming that a number of tables exist in the SQL database - events, gd_runs and there is no code to create them, and one is left trying to guess what the schema for those tables is supposed to be and then creating them manually.

No `python/neurosat.py` in the repo.