SAT4CryptoBench

SAT4CryptoBench是一个大规模基准测试，用于评估基于SAT的密码学问题求解。它提供了标准化数据集和实验框架，用于分析不同密码学原语上的求解器性能、实例难度和模型泛化能力。该基准旨在弥合AI增强的SAT求解与传统密码分析之间的差距，为神经引导求解器提供系统比较和训练数据。SAT4CryptoBench is a large-scale benchmark for evaluating SAT-based cryptographic problem solving. It provides standardized datasets and an experimental framework to analyze solver performance, instance hardness, and model generalization capabilities across different cryptographic primitives. This benchmark aims to bridge the gap between AI-augmented SAT solving and traditional cryptanalysis, providing systematic comparison and training data for neuro-guided solvers.

原始信息汇总

SAT4CryptoBench 数据集概述

数据集简介

SAT4CryptoBench 是一个大规模基准测试集，专门用于评估基于SAT的密码问题求解。该数据集提供标准化的数据集和实验框架，用于分析求解器性能、实例难度以及不同密码原语间的模型泛化能力。

主要贡献

• 建立了首个统一的密码问题求解SAT基准测试集
• 提供完整的ANF-to-SAT实例转换流程，包含完整的变量映射和标注
• 集成了求解器无关的评估框架，支持经典和神经SAT求解器
• 包含难度排名和求解器诊断功能，用于可解释性和分析
• 支持基于学习的SAT变量决策、重启和子句剪枝策略优化

基准测试内容

CNF格式数据集

• Cipher：包含8到12轮加密的密码数据集，每个配置1000个样本
• Simon：包含10到12轮、32位密钥的Simon数据集，每个配置1000个样本
• md4-20rounds：20轮MD4哈希函数数据集，1000个样本
• sha1-21rounds：21轮SHA-1哈希函数数据集，1000个样本
• sha256-18rounds：18轮SHA-256哈希函数数据集，1000个样本

ANF格式数据集

• Simon-ANF：包含10到12轮、32位密钥的Simon数据集，每个配置1000个样本

评估框架

独立求解器评估

支持模型训练和评估，使用ANF图结构和CryptoANFNet模型架构

启发式增强

集成12种SAT求解器：

• kissat
• MaplePainless
• CDCL-Crypto
• Maplesat
• glucose-4.1-bmm
• maplecomsps_lrb_vsids_18-bmm
• maplelcmdistchronobt-bmm
• maplesat-bmm
• glucose-4.1
• maplecomsps_lrb_vsids_18
• maplelcmdistchronobt
• cadical

支持11个数据集评估，单实例超时设置为5000秒

超参数优化

支持EasyNAS和HEBO两种超参数优化方法

技术需求

• Python 3.8
• PyTorch及相关扩展库
• torch_geometric==2.6.1
• torch_spline_conv==1.2.2
• torch_sparse==0.6.18
• torch_scatter==2.1.2
• torch_cluster==1.6.3
• pyg_lib==0.4.0

许可证

Apache 2.0 许可证

引用信息

bibtex @inproceedings{Zheng25sat4cryptobench, title={Bridging Crypto with ML-based Solvers: the SAT Formulation and Benchmarks}, author={Xinhao Zheng, Xinhao Song, Bolin Qiu, Yang Li, Zhongteng Gui, Junchi Yan}, year={2025}, booktitle = {Advances in Neural Information Processing Systems}, url={https://openreview.net/pdf?id=BmwbEWRkyE}, }

搜集汇总

数据集介绍

构建方式

在密码学与可满足性理论交叉领域，SAT4CryptoBench通过系统化采集多种密码原语的运算过程构建数据集。该数据集将高级密码函数转化为代数正规形式，再通过标准化管道映射为合取范式实例，覆盖了Cipher、Simon、MD4、SHA-1和SHA-256等典型密码算法。每个算法变体均包含特定轮次配置，通过精确的变量标记机制保持密码运算的语义完整性，最终形成包含数千个标注实例的基准集合。

特点

作为首个面向密码学问题的统一SAT基准，该数据集具备多维度特性。其核心价值在于提供ANF与CNF双格式数据，支持从代数表示到逻辑公式的完整分析链路。数据集通过难度分级机制区分实例复杂度，并配备变量映射标签以实现求解过程的可解释性。不同密码原语与轮次配置的组合，为研究算法在对称密码与哈希函数上的泛化能力提供了系统化实验环境。

使用方法

该数据集支持三类典型应用范式：基于神经网络的端到端求解器训练可通过指定数据路径与图结构参数实现模型优化；传统求解器的增强测试框架支持多线程并行评估，提供超时控制与详细日志记录；超参数优化模块则集成EasyNAS与HEBO工具链，允许通过配置文件调整求解策略。用户可根据实验需求选择独立评估或组合流程，所有输出均遵循标准化度量指标。

背景与挑战

背景概述

SAT4CryptoBench由Xinhao Zheng等研究人员于2025年提出，是首个专为密码学问题求解设计的统一SAT基准测试集。该数据集旨在弥合人工智能增强SAT求解与传统密码分析之间的鸿沟，通过标准化实例转换管道和评估框架，系统化地比较不同密码原语下的求解器性能与模型泛化能力。其覆盖了Cipher、Simon、MD4、SHA-1和SHA-256等多种密码算法，为神经引导求解器的训练与优化提供了关键数据支撑，显著推动了密码学与机器学习交叉领域的研究进程。

当前挑战

在密码学领域，SAT4CryptoBench致力于应对复杂密码原语的可满足性判定难题，其核心挑战在于如何高效处理高轮次加密算法与哈希函数转化后的SAT实例组合爆炸问题。数据集构建过程中，研究者需克服ANF-to-SAT转换时变量映射的完整性保持、不同密码结构实例的难度分级标定，以及多类型求解器性能评估的标准化适配等关键技术障碍。这些挑战直接关系到基准测试在密码分析实际场景中的有效性与可靠性。

常用场景

经典使用场景

在密码学与人工智能交叉领域，SAT4CryptoBench作为首个统一的SAT基准测试集，广泛应用于评估SAT求解器在密码问题中的性能。该数据集通过标准化ANF到SAT实例的转换流程，支持对多种密码原语（如Cipher、Simon、SHA系列）的系统性测试，为研究者提供了可靠的实验平台，以分析求解器在不同加密轮次和配置下的表现。

解决学术问题

SAT4CryptoBench有效解决了密码分析中SAT求解器性能评估标准缺失的学术难题。它通过集成求解器无关的评估框架，支持经典与神经求解器的对比分析，并引入难度排名和诊断机制，提升了模型泛化能力的可解释性。这一基准填补了AI增强求解与传统密码分析之间的鸿沟，推动了学习优化策略在变量决策和子句剪枝中的应用。

衍生相关工作

基于SAT4CryptoBench，衍生出多项经典研究工作，如神经引导求解器的训练与优化框架。这些工作利用数据集的ANF-to-SAT管道和变量映射，开发了针对密码问题的专用求解器（如CDCL-Crypto），并推动了超参数优化工具（如EasyNAS和HEBO）在SAT求解中的集成，显著提升了求解速度与准确度，为后续密码机器学习研究奠定基础。