chc-comp25-benchmarks

这些基准测试已经通过格式化工具预处理，并分类到不同类别中。仓库包含多种文件类型：.smt2文件是CHC-COMP格式的基准测试源文件，.yml文件包含benchexec的基准测试元数据，.set文件指定每个类别的任务列表。元数据指定了预期结果，包括未解决、sat、unsat或不一致。部分基准测试因重复被排除在任务列表之外。

These benchmarks have been preprocessed by formatting tools and categorized into distinct categories. The repository contains multiple file types: .smt2 files are benchmark source files in CHC-COMP format, .yml files contain benchmark metadata for benchexec, and .set files specify the task list for each category. The metadata specifies expected outcomes, including unresolved, sat, unsat, or inconsistent. Some benchmarks have been excluded from the task lists due to duplication.

原始信息汇总

2025年CHC-COMP使用的基准测试数据集

数据集概述

• 数据集用于2025年CHC-COMP竞赛
• 基准测试已通过formatter预处理
• 使用classifier进行分类

文件类型

• .smt2文件：采用CHC-COMP格式的基准测试源文件
• .yml文件：包含benchexec的基准测试元数据
• .set文件：指定每个类别的任务列表

元数据说明

• 元数据指定预期结果：
  • 不存在：2025年没有工具解决此基准测试
  • true：所有成功的工具报告sat
  • false：所有成功的工具报告unsat
  • inconsistent：存在冲突结果

注意事项

• 部分基准测试因重复被排除在任务列表外
• 竞赛脚本位于chc-comp25-scripts

搜集汇总

数据集介绍

构建方式

在约束求解领域，chc-comp25-benchmarks数据集通过系统化流程构建而成。原始基准测试文件经由专用格式化工具处理，符合CHC-COMP标准格式规范，并采用自动化分类器按特定维度进行任务归类。数据集构建过程中特别标注了元数据信息，包括工具验证结果的一致性状态，同时对重复样本进行了去重处理，确保每个测试案例具有唯一性。

特点

该数据集作为2025年CHC-COMP竞赛的官方基准，其核心价值体现在多维度验证信息的标注体系。每个.smt2格式的约束问题均附有详细的元数据描述，包括工具求解结果的预期判定（sat/unsat）及一致性状态。特别设计的.set文件实现了测试任务的分类管理，而.yml文件则与benchexec框架深度兼容，为性能评估提供了标准化接口。

使用方法

研究者可通过解析.smt2文件获取标准格式的约束求解问题，配合附带的元数据文件实现自动化验证。分类后的.set文件支持按需选择特定领域的测试子集，而预置的.yml配置文件可直接接入benchexec测试框架，实现求解工具的标准化性能评估。数据集特别标注的不一致案例为研究约束求解工具的鲁棒性提供了重要素材。

背景与挑战

背景概述

chc-comp25-benchmarks数据集源于2025年CHC-COMP竞赛，由CHC-COMP组织团队构建，旨在为约束霍恩子句（Constrained Horn Clauses, CHC）求解领域提供标准化的评测基准。该数据集通过预处理器格式化并分类，包含多种文件类型，如.smt2格式的基准源文件、.yml格式的元数据文件以及.set格式的任务列表文件。其核心研究问题聚焦于自动化推理工具的效能评估，为形式化验证领域提供了重要的性能比较平台，显著推动了CHC求解技术的发展。

当前挑战

该数据集面临的挑战主要体现在两方面：在领域问题层面，CHC求解本身具有极高的计算复杂性，不同工具对同一问题的判定可能存在冲突（如元数据中的'inconsistent'标记），这要求基准集必须能有效区分工具的真实性能；在构建过程中，需解决重复基准的识别与剔除、多源数据格式的统一转换，以及确保分类系统能准确反映不同求解任务的特性等工程难题。

常用场景

经典使用场景

在约束逻辑编程和自动推理领域，chc-comp25-benchmarks数据集被广泛用于评估和比较不同约束求解器的性能。该数据集通过预处理的.smt2文件提供了标准化的测试用例，为研究人员提供了一个统一的平台来验证求解器在各类约束条件下的表现。特别是在CHC-COMP年度竞赛中，这些基准测试成为衡量求解器效率和可靠性的黄金标准。

实际应用

在实际应用中，这些基准测试被工业界和学术界广泛用于验证新型求解算法的有效性。软件验证工具开发者利用该数据集来优化其产品的推理能力，特别是在程序静态分析和形式化验证场景中。数据集中包含的冲突结果案例也为研究求解器的容错机制提供了宝贵素材。

衍生相关工作

围绕该数据集已衍生出多项重要研究，包括约束求解器的并行化优化、混合求解策略的开发以及求解结果的可视化分析工具。其中基于benchexec框架的性能评估系统已成为该领域的标配工具，而针对不一致结果的分析则催生了新的容错求解算法研究分支。