VLSAT-2 Benchmark Suite

VLSAT-2 Benchmark Suite是由法国国家信息与自动化研究所的CONVECS项目团队创建，包含100个SAT公式，用于科学实验和软件竞赛，解决SAT问题。数据集分为50个可满足和50个不可满足的公式，采用DIMACS CNF格式，部分数据已在2020和2021年的国际SAT竞赛中使用。数据集的创建涉及将Petri网分解为自动机网络，生成大量布尔公式，并从中精选出符合SAT竞赛要求的子集。该数据集主要应用于SAT问题的解决，旨在通过提供复杂度递增的测试案例，推动SAT求解技术的发展。

The VLSAT-2 Benchmark Suite was created by the CONVECS project team at the Institut National de Recherche en Informatique et en Automatique (INRIA), France’s national institute for digital science and technology. It contains 100 SAT formulas and is designed for scientific experiments and software competitions focused on SAT solving. The dataset is split into 50 satisfiable and 50 unsatisfiable formulas, and is stored in the DIMACS CNF format. A portion of the data was used in the International SAT Competitions held in 2020 and 2021. The development of this dataset involved decomposing Petri nets into automaton networks, generating a large number of Boolean formulas, and selecting a subset that meets the requirements of SAT competitions from the generated pool. This dataset is primarily utilized for SAT problem solving, aiming to promote the development of SAT solving technologies by providing test cases with increasing complexity.

搜集汇总

数据集介绍

构建方式

在形式化方法与并发理论领域，VLSAT-2基准套件的构建源于将Petri网分解为自动机网络的研究工作。该数据集通过一套工具链生成，该工具链将普通、安全的Petri网作为输入，并将其并发约束转化为逻辑问题，进而生成布尔可满足性问题（SAT）公式。具体而言，每个公式对应一个特定的Petri网，通过定义位置集合、并发关系以及选定的单元数量，将网分解问题编码为图着色实例。公式以合取范式表达，并采用DIMACS CNF格式存储，最终从超过132,000个候选公式中精心筛选出100个具有挑战性的样例，其中50个可满足，50个不可满足，确保了问题复杂度的递增性与多样性。

特点

VLSAT-2基准套件在SAT求解研究领域展现出显著的科学价值与实用特性。该数据集包含100个公式，严格平衡了可满足与不可满足实例的数量，且所有公式均以DIMACS CNF标准格式提供，并采用宽松的Creative Commons许可协议，便于学术共享与工具评估。其核心特点在于公式的难度经过精心校准：通过五种主流SAT求解器的严格测试，筛选出那些在短时间内难以解决但又在合理时间内可验证的案例，从而覆盖了从易到难的完整谱系。此外，约25%的公式已被国际SAT竞赛采纳，进一步印证了其在基准测试中的权威性与代表性。

使用方法

VLSAT-2基准套件主要用于评估与比较SAT求解器的性能，推动形式化验证与并发理论领域的研究进展。研究人员可下载其压缩格式的文件，利用支持DIMACS CNF输入的求解工具进行实验。该数据集适用于多种场景：在算法竞赛中，可作为标准测试集检验求解器的效率与鲁棒性；在学术研究中，能够用于分析复杂SAT实例的结构特性，或验证新型求解策略的有效性。用户需注意，数据集中的公式具有不同的变量数与子句规模，建议在实验设计中综合考虑计算资源与时间约束，并参考报告中提供的难度分级，以系统化地评估求解器在不同复杂度下的表现。

背景与挑战

背景概述

在形式化验证与并发理论领域，Petri网分解为自动机网络是一个自上世纪70年代延续至今的核心问题。2021年9月，法国国家信息与自动化研究所的CONVECS团队发布了VLSAT-2基准测试套件，由Pierre Bouvier与Hubert Garavel主导开发。该数据集源于将Petri网的并发约束转化为布尔可满足性问题（SAT）的研究工作，旨在为SAT求解器的性能评估与算法竞赛提供高质量的测试基准。VLSAT-2包含100个精心筛选的SAT公式，其中半数可满足、半数不可满足，其生成过程融合了来自通信协议、分布式系统等工业级Petri网模型，体现了理论研究与工程实践的深度结合。该数据集已被国际SAT竞赛2020与2021届赛事采纳，显著推动了SAT求解技术在形式化验证领域的应用与发展。

当前挑战

VLSAT-2数据集主要应对SAT求解领域的两类挑战：一是解决复杂工业系统形式化验证中Petri网分解问题的可满足性判定难题，该问题本质上等价于图着色问题的扩展，当单元数量接近图的色数时，组合爆炸导致求解难度急剧上升；二是在数据集构建过程中，研究者需从超过13.2万个候选公式中筛选出兼具代表性与挑战性的实例，既要排除现有求解器能在一分钟内解决的简单公式，又要确保所有公式在有限计算资源下具有可处理性。此外，生成公式需平衡规模与难度，并引入对称性约束以降低问题冗余度，这对基准设计的科学性与实用性提出了双重考验。

常用场景

经典使用场景

在形式化验证与自动推理领域，VLSAT-2基准测试集作为布尔可满足性问题的代表性数据集，其经典使用场景主要集中于SAT求解器的性能评估与算法竞赛。该数据集精心构建了100个复杂度递增的SAT公式，其中半数可满足、半数不可满足，这种平衡设计使其成为国际SAT竞赛的核心测试材料。通过提供标准化的DIMACS CNF格式文件，VLSAT-2为不同求解器提供了公平比较的平台，研究人员能够系统性地分析算法在应对大规模并发约束时的表现差异。

衍生相关工作

围绕VLSAT-2数据集衍生的经典研究工作形成了完整的技术生态链。其前身VLSAT-1测试集专注于可满足公式的模型计数问题，而VLSAT-2的平衡设计催生了针对混合类型公式的求解策略研究。相关成果已融入Model Checking Contest和RERS挑战赛等国际竞赛的评测体系。基于该数据集生成的Nested-Unit Petri Net分解方法，进一步推动了CADP、LTSmin等工具链的算法优化，形成从理论模型到工程工具的全链条创新体系。

数据集最近研究

最新研究方向

在布尔可满足性问题领域，VLSAT-2基准套件作为源自佩特里网分解的复杂SAT公式集合，正推动着SAT求解器性能评估的前沿研究。该数据集通过将并发理论中的图着色问题转化为逻辑约束，生成了兼具可满足与不可满足性的挑战性实例，其中25%的公式已被国际SAT竞赛采纳为官方测试用例。当前研究热点聚焦于利用这些高度结构化的公式，探索对称性破缺、子句学习等高级求解策略在超大规模实例上的效能边界，同时为形式化验证工具在分布式系统与硬件电路等工业场景中的应用提供基准支撑。其影响在于为SAT求解算法的鲁棒性提供了标准化测试平台，促进了求解器在应对组合爆炸问题时的理论突破与工程优化。

相关研究论文

• The VLSAT-2 Benchmark Suite

  法国国家信息与自动化研究所 · 2021年