AutoSAT

Welcome to the official repository for the paper "AutoSAT: Automatically Optimize SAT Solvers via Large Language Models". This repository is dedicated to automatically optimize heuristics in SAT solvers through Large Language Models (LLMs). We hope our method can be universally applied to a variety of solvers and welcome researchers from all backgrounds to join us in this endeavor!

This branch is for AutoSAT_v2(Multi Agent Version) , you can find original version (AutoSAT_v1) in branch AutoSAT_v1.

Clone this repo

git clone https://github.com/YiwenAI/AutoSAT

Installation

We support both Linux and Windows

1. Python 3.10
2. G++ 17 or higher to support filesystem

Install requirements: pip install -e .

Install this package python setup.py develop

Use Docker

docker build -t autosat .

Dataset

• All of our datasets can be obtained from cnf_data_link

• The codes we used to generate the specific problems are in ./data/

• Access more SAT Competition questions by visiting SAT Competition

Metrics

We use the following metrics to evaluate the performance of a Solver.

• PAR-2: The Penalized Average Runtime with factor 2

• #solved: Number of questions the Solver solved within timeout

• total time: Total running time for a Solver.

• #satisfied: Number of getting feasible solution.

• #unsatisfied: Number of solving unfeasible questions

• #timeout: Number of timeout cases.

Train&Test

Preparation

• Please refer to data explanation to prepare your dataset
• Prepare your api key
• Make sure you have checkout prompts in ./examples

Train

In AutoSAT version 2.0, we add multi-agent for better exploration.

python3 main_MultiAgent.py \
        --iteration_num 4 \
        --batch_size 4 \
        --data_parallel_size 6 \
        --devoid_duplication False \
        --timeout 1500 \
        --data_dir <your_train_set_path> \
        --project EasySAT \
        --task bump_var_function \
        --original True \
        --agent_type 'advisor-coder-evaluator' \
        --agent_args_folder <your_agentsPrompt&args_path> \
        --temperature 0.5 \ 
        --api_base <your_api_base> \
        --api_key <your_api_key>

💡 Tips

• Please refer to configs explanation for more details.

• We recomend to use python3 main_MultiAgent.py --config your_config_file_path and pass the params by .yaml such as config.yaml (an example)

💡 More Details

• When original is set to False, you have to set dict original_result in your config.yaml

• agent_type determines what agents to be used. agent_args_floder (includes advisor_args, coder_args, evaluator_args). We left flexiable interfaces to guide agents. See more details in agents_args_doc

• The heuristic functions generated and the some metrics are save in the folder: './temp/prompts/' (final_result.json or iter_xx_result.json)

Test

You can also evaluate your found solver heuristics:

python3 evaluate.py \
        --SAT_solver_file_path SAT_solver_file_path \
        --results_save_path your_final_eval_results_savePath \
        --batch_size 4 \
        --eval_parallel_size 6 \
        --eval_timeout 500 \
        --eval_data_dir your_test_set_path \
        --rand_seed 42
        --keep_intermediate_results False \
        --method_name your_solver_name

💡 Tips

We recomend to use python3 evaluate.py --config your_eval_config_file_path and pass the params by .yaml such as config_eval.yaml (an example)

Refer to configs explanation for more details.

The final evaluation results are saved in the folder you set previously -- results_save_path

Acknowledgement

Our Backbone (as baseline) is EasySAT and we only add data parallel and file saving modules. Thanks for the wonderful work.

Citing us

If our work has been helpful to you, please feel free to cite us:

@article{sun2024autosat,
  title={AutoSAT: Automatically Optimize SAT Solvers via Large Language Models},
  author={Sun, Yiwen and Zhang, Xianyin and Huang, Shiyu and Cai, Shaowei and Zhang, Bing-Zhen and Wei, Ke},
  journal={arXiv preprint arXiv:2402.10705},
  year={2024}
}