Code accompanying the NeurIPS 2019 paper Learning local search heuristics for Boolean satisfiability.
Make sure to have minisat in your path. It is available here: http://minisat.se/MiniSat.html
Run the following sequence of commands to clone the repository and create the required conda environments.
git clone --recursive https://github.com/emreyolcu/sat.git
cd sat
conda env create -f sat.yaml
conda env create -f cnfgen.yaml
(cd code/PyMiniSolvers && make)
scripts directory includes bash scripts to generate the data used for training. As an example, to generate the coloring formulas, run the following commands.
conda activate cnfgen
scripts/generate_kcolor.sh
When generating the SR formulas, activate the sat environment instead of cnfgen before running the script.
configs/search directory includes training configurations for each set of formulas. Run the following commands to train models on sets of coloring formulas of increasing size.
conda activate sat
python code/train_search.py --config_path configs/search/kcolor/5.yaml
python code/train_search.py --config_path configs/search/kcolor/10.yaml
python code/train_search.py --config_path configs/search/kcolor/15.yaml
python code/train_search.py --config_path configs/search/kcolor/20.yaml
If a configuration file has the line eval_multi: True, the training script will create 25 processes to perform evaluation during training. Remove this line or change the value to False if you prefer to use a single process instead.
When attempting to use multiple processes you may see the error Too many open files. This can be avoided by executing ulimit -n 4096 (or another large value that your system allows) before starting training.
After training is completed, run the following commands to evaluate a learned model and WalkSAT on a set of formulas.
conda activate sat
python code/evaluate.py --dir_path data/kcolor/3-10-0.5 --samples 5 --model_path results/search/kcolor/5/model_best.pth --no_multi
python code/walksat.py --dir_path data/kcolor/3-10-0.5 --samples 5
Arguments used:
--dir_path: Directory containing the formulas.--samples: Number of formulas to run the solver on.--model_path: Saved parameters of the graph neural network to evaluate.--no_multi: Whether to use a single process for evaluation. Without this argument, the script creates 25 processes.