neuroback/DataBack

DataBack是一个包含120,286个SAT公式（CNF格式）的数据集，每个公式都标注了其骨干变量的相位。数据集分为两个子集：预训练集（DataBack-PT）和微调集（DataBack-FT），分别用于预训练和微调NeuroBack模型。数据集的结构包括原始和双CNF公式及其骨干变量相位，文件命名和格式也有详细说明。

DataBack is a dataset consisting of 120,286 SAT formulas (in CNF format), each labeled with the phases of its backbone variables. DataBack contains two distinct subsets: the pre-training set, named DataBack-PT, and the fine-tuning set, named DataBack-FT, for pre-training and fine-tuning our NeuroBack model, respectively. The state-of-the-art backbone extractor, CadiBack, has been employed to extract the backbone variable phases. The datasets directory structure includes original and dual CNF formulas and their backbone variable phase files. The file naming follows a specific convention, ensuring that CNF files and their associated backbone files share the same name.

原始信息汇总

DataBack: Dataset of SAT Formulas and Backbone Variable Phases

数据集概述

DataBack 是一个包含 120,286 个 SAT 公式（以 CNF 格式）的数据集，每个公式都标记了其骨干变量的相位。DataBack 包含两个不同的子集：预训练集 DataBack-PT 和微调集 DataBack-FT，分别用于预训练和微调我们的 NeuroBack 模型。

目录结构

|- original # 原始 CNF 公式及其骨干变量相位 | |- cnf_pt.tar.gz # 预训练的 CNF 公式 | |- bb_pt.tar.gz # 预训练公式的骨干相位 | |- cnf_ft.tar.gz # 微调的 CNF 公式 | |- bb_ft.tar.gz # 微调公式的骨干相位 | |- dual # 双 CNF 公式及其骨干变量相位 | |- d_cnf_pt.tar.gz # 预训练的双 CNF 公式 | |- d_bb_pt.tar.gz # 预训练双公式的骨干相位 | |- d_cnf_ft.tar.gz # 微调的双 CNF 公式 | |- d_bb_ft.tar.gz # 微调双公式的骨干相位

文件命名约定

在 original 目录中，每个 CNF tar 文件（cnf_*.tar.gz）包含压缩的 CNF 文件，命名格式为：[cnf_name].[compression_format]，其中 [compression_format] 可以是 bz2、lzma、xz、gz 等。相应的，每个骨干 tar 文件（bb_*.tar.gz）包含压缩的骨干文件，命名格式为：[cnf_name].backbone.xz。需要注意的是，压缩的 CNF 文件与其关联的压缩骨干文件将始终共享相同的 [cnf_name]。

对于双公式及其对应的骨干文件，命名约定保持一致，但增加了 d_ 前缀。

提取的骨干文件格式

提取的骨干文件（*.backbone）遵循 CadiBack 的输出格式。

参考文献

如果您在研究中使用 DataBack，请引用以下论文：

NeuroBack paper: bib @article{wang2023neuroback, author = {Wang, Wenxi and Hu, Yang and Tiwari, Mohit and Khurshid, Sarfraz and McMillan, Kenneth L. and Miikkulainen, Risto}, title = {NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks}, journal={arXiv preprint arXiv:2110.14053}, year={2021} }

CadiBack paper: bib @inproceedings{biere2023cadiback, title={CadiBack: Extracting Backbones with CaDiCaL}, author={Biere, Armin and Froleyks, Nils and Wang, Wenxi}, booktitle={26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)}, year={2023}, organization={Schloss Dagstuhl-Leibniz-Zentrum f{"u}r Informatik} }