Solver Tuner for IC3/PDR

A tool for tuning PDR solver parameters for AIGER circuit model checking using graph neural networks.

Quick Start with Docker 🐳

The easiest way to get started is using Docker:

# Build the Docker image
docker build -t solver-tuner .

# Run interactive session
docker run -it --rm \
  -v $(pwd)/data:/app/data \
  -v $(pwd)/benchmarks:/app/benchmarks \
  -v $(pwd)/output:/app/output \
  -v $(pwd)/models:/app/models \
  solver-tuner

# Inside container: install python package
cd python && pip install -e .

# Inside container: prepare data
python scripts/generate_data.py benchmarks/ -o data/

# Train a model
trainer data/test_experiment.csv data/test_circuit --model-out=models/model.pt --features-dir=data/circuit_features/ --epochs=20 --mode train --model-type="GraphSAGE"

# Make predictions (pre-trained model: use best_kendall_model.pt and best_kendall_params.pkl)
predictor --aig-file data/6s8.aig --model data/best_kendall_model.pt --find-best --params data/best_kendall_params.pkl

Manual Environment Setup

If you prefer to set up the environment manually, this project has both Rust and Python dependencies:

cargo build --release # build the aig2feat binary
conda env create -f env/environment.yml
conda activate st
cd python && pip install -e . # install the python package: trainer, predictor, sampler

Usage

Data Preparation

1. Place your labeled training data in data/train_data.csv. A sample file is provided at data/experiment_formated.csv.

2. Ensure all AIGER circuit files referenced in data/train_data.csv are located in the benchmarks/ directory.

3. Extract circuit features and generate PyTorch Geometric (PyG) graph data by running:

# Extract circuit features and generate PyG data
python scripts/generate_data.py benchmarks/ -o data/

Training a Model

# Basic training
trainer data/experiment_formated.csv data/test_circuit --model-out=data/model.pt --features-dir=data/circuit_features/ --epochs=20 --mode train

# Compare different models
trainer ... --model-type hoga        # HOGA (DAC24: Less is more)
trainer ... --model-type graphsage   # GraphSAGE  
trainer ... --model-type graphsaint  # GraphSAINT
trainer ... --model-type gcn         # Graph Convolutional Network
trainer ... --model-type gat         # Graph Attention Network

# Hyperparameter optimization with Optuna
trainer ... --optimize-hyperparams --n-trials 50

# Mixed precision training (faster on GPU)
trainer ... --use-amp

Making Predictions

# Find best PDR configuration for a circuit
predictor --aig-file benchmarks/6s8.aig  \
    --model models/model.pt \
    --find-best \
    --params models/param.pkl