VLSAT-1

VLSAT-1是由国家信息与自动化研究所创建的，包含100个SAT公式的数据集，用于科学实验和软件竞赛，特别是解决大规模布尔可满足性问题。这些公式以DIMACS CNF格式提供，总容量为2.1GB，压缩后为419MB。数据集的创建过程涉及将Petri网分解为自动机网络，生成大量SAT公式，并从中精选出100个。VLSAT-1的应用领域包括模型计数和形式验证，旨在提高解决复杂逻辑问题的效率和准确性。VLSAT-1 is a dataset containing 100 SAT formulas, developed by the National Institute of Information and Automation for scientific experiments and software competitions, especially for solving large-scale Boolean satisfiability problems. These formulas are provided in DIMACS CNF format, with an uncompressed total size of 2.1 GB and a compressed size of 419 MB. The dataset creation process involves decomposing Petri nets into automaton networks, generating a large number of SAT formulas, and selecting 100 qualified ones for the final dataset. VLSAT-1 is applicable in model counting and formal verification, aiming to improve the efficiency and accuracy of solving complex logical problems.

搜集汇总

数据集介绍

构建方式

在形式化验证与并发系统分析领域，VLSAT-1数据集的构建源于Petri网分解为自动机网络的研究工作。该数据集通过一套工具链生成，该工具链将普通、安全且规模适中的Petri网作为输入，并基于其位置集合与并发关系，转化为可满足性（SAT）问题。具体而言，每个SAT公式对应一个特定的Petri网，通过引入命题变量表示位置与单元之间的归属关系，并添加约束条件以确保并发位置不被分配至同一单元，同时采用对称性打破技术避免冗余解。最终，从超过12,000个Petri网生成的SAT公式中精选出100个，以DIMACS CNF格式存储，并经过bzip2压缩以优化存储与传输效率。

特点

VLSAT-1数据集在布尔可满足性问题研究领域具有显著的代表性与实用性。其核心特点在于涵盖100个复杂度递增的SAT公式，所有公式均为可满足且设计为拥有大量模型，从而能够有效评估SAT求解器在处理大规模问题时的性能。数据集的公式规模跨度极大，变量数量从10至数百万不等，子句数量亦呈现广泛分布，充分反映了实际应用中并发系统模型的多样性。此外，数据集采用开放的Creative Commons Attribution 4.0许可，支持学术与竞赛场景下的自由使用与共享，并已成功应用于2020年国际模型计数竞赛，体现了其权威性与基准价值。

使用方法

VLSAT-1数据集主要服务于SAT求解算法的实验评估与性能比较。研究人员或开发者可下载以DIMACS CNF格式提供的压缩文件，解压后直接将其输入SAT求解器进行可满足性判定或模型计数。由于公式具有已知的可满足性，用户可验证求解结果的正确性，并通过分析求解时间、内存消耗等指标来评估算法效率。该数据集特别适用于测试求解器处理大规模、高复杂度实例的能力，亦可用于训练机器学习模型以预测公式特性或优化求解策略。在具体应用中，建议结合公式的变量与子句数量分布，设计渐进式实验以系统性考察求解器的可扩展性与鲁棒性。

背景与挑战

背景概述

VLSAT-1基准测试套件由法国国家信息与自动化研究所的CONVECS团队于2020年11月正式发布，旨在为布尔可满足性问题（SAT）的求解研究提供大规模、高复杂度的标准化测试数据。该数据集源于Petri网分解为自动机网络的前沿研究，通过将并发约束转化为逻辑问题，生成了100个满足性公式，并以DIMACS CNF格式公开。这些公式已应用于2020年国际模型计数竞赛，推动了形式化验证与SAT求解工具的效能评估与算法优化，成为该领域重要的实验基准。

当前挑战

VLSAT-1数据集核心挑战在于应对超大规模SAT问题求解的复杂性，其公式变量与子句数量跨越多个数量级，最高可达数百万变量与数十亿子句，对现有求解器的可扩展性与计算效率提出严峻考验。构建过程中，研究人员需从逾1.2万个Petri网中筛选代表性实例，并通过对称性约束消除单位置换冗余，确保公式既保持理论意义又具备渐进难度，这一过程涉及并发关系建模、图着色问题转化与大规模逻辑公式生成的精密平衡。

常用场景

经典使用场景

在形式化验证与自动推理领域，VLSAT-1基准套件为布尔可满足性问题（SAT）的研究提供了关键实验平台。该数据集包含100个规模递增的SAT公式，采用DIMACS CNF格式编码，其经典使用场景集中于评估和比较SAT求解器的性能。研究者通过运行这些公式，能够系统分析求解器在处理大规模、高复杂度逻辑问题时的效率与可扩展性，从而推动SAT求解算法的优化与创新。

衍生相关工作

VLSAT-1的发布催生了多项经典研究工作，尤其是在SAT求解竞赛与形式化方法工具链的开发中。例如，该数据集的部分公式经过调整后，被应用于2020年国际模型计数竞赛的实例轨道，推动了模型计数算法的发展。同时，基于VLSAT-1的公式结构，研究者进一步探索了嵌套单元佩特里网（NUPN）的分解优化方法，衍生出更高效的验证工具，并在模型检查竞赛等国际活动中得到广泛采用。

数据集最近研究

最新研究方向

在形式化验证与自动推理领域，VLSAT-1基准套件作为大规模布尔可满足性问题的代表性数据集，正推动SAT求解技术的前沿探索。其生成的背景源于Petri网到自动机网络的分解问题，这一经典难题在并发系统验证中具有核心地位。当前研究热点聚焦于利用该数据集评估和优化SAT求解器在处理超大规模、高复杂度实例时的性能与可扩展性，特别是在模型计数竞赛等国际活动中，VLSAT-1已成为检验求解器鲁棒性与效率的关键工具。该数据集通过提供从实际工业系统抽象而来的多样化公式，不仅促进了求解算法在内存管理、并行计算方面的创新，也为硬件验证、协议分析等应用领域提供了可靠的基准支持，对提升形式化方法的实用化水平具有深远意义。

相关研究论文

• The VLSAT-1 Benchmark Suite

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