第三方声明
中文译文供参考,许可条款以原文为准。
本页列出组件来源、许可和署名要求。 供复用任务材料或准备分发的用户阅读。
第三方条款适用于任务文件夹和容器中的对应文件。原始许可文本位于 docs/licenses/third-party/。各资源可共享的范围见分发条件,固定来源和文件列表见组件记录。
Solver 代码、数据与参考材料
读法说明:每行列出指定组件及其署名要求。environment/app/ 下的路径均相对于该行所指任务。
| 资源与位置 | 来源、作者与条款 | 署名与分发条件 |
|---|---|---|
BPPLIB 实例:tasks/solver/online/bpp-bpplib/environment/app/instances/、library/ 和 tests/official-instances/ | M. Delorme、M. Iori、S. Martello 及各实例族作者;BPPLIB 许可,CC BY-NC-ND 4.0 | 保留原始署名和许可。非商业及禁止演绎条件继续有效。 |
| BPPLIB 装箱方案、注册表提取数据及变换数据,包括隐藏判分数据 | 基于 BPPLIB 数据和求解日志,适用相同的 CC BY-NC-ND 4.0 条款 | 获取原件,并在本地准备所需文件。按分发条件将生成文件保留在本地。来源与准备记录及表格来源记录标明对应材料。 |
课程排课实例及变换:tasks/solver/online/curriculum-itc2007/ | Sara Ceschia、Francesca Da Ros、Luca Di Gaspero、Andrea Schaerf;cb-ctt 许可,CC BY 4.0 | 署名作者并保留转换说明。comp15 对应官方 comp03;许可依据不延伸至 comp11。参见来源比较。 |
CPSolver 封装层源码:environment/app/cpsolver-src/ | Tomáš Müller 等;原始仓库;源码头注明 LGPL-3.0-or-later | 保留源码头、原始声明和修改说明。分发二进制文件时一并提供对应源码及构建材料。 |
CPSolver 核心 JAR:environment/app/lib/cpsolver-all-1.2.jar | CPSolver 1.2_bld46;上游任务包来源;JAR 内含 LGPL-3.0 文本 | 源码、构建与替换指南标明对应发布源码及包内所需内容。保留 LGPL 和相关依赖声明。 |
dom4j 1.6.1:environment/app/lib/dom4j-1.6.1.jar | MetaStuff Ltd.;JAR 的 META-INF/LICENSE.txt 内含五条款 BSD 风格条款 | 保留完整声明,包括署名、禁止背书和名称限制。五个条款均须完整保留。 |
log4j 1.2.8:environment/app/lib/log4j-1.2.8.jar | Apache Software Foundation;官方源码归档中的 Apache Software License 1.1 | 保留完整许可、其要求的致谢和名称限制。参见 third-party/Log4j-1.2.8-Apache-1.1.txt。 |
官方 ITC 2007 validator.cc 和 OptHub 已知最好解 | Andrea Schaerf、Luca Di Gaspero 及解的贡献者;ITC 2007 和 OptHub | 这些文件的再分发条款尚未确认。从原始来源获取,并遵循各自条款。 |
MQLib 软件:tasks/solver/online/maxcut-mqlib/environment/app/mqlib/ | Iain Dunning、Swati Gupta 和 John Silberholz;MQLib 许可,MIT | 保留版权、MIT 许可和修改代码的声明。实例数据采用下列各实例族条款;随附论文和补充材料请查阅各自来源。 |
| MQLib 实例及变换副本 | MQLib 下载脚本指向单独托管的来源 | 实例条款因实例族而异。逐项从其来源获取,并遵循该实例族条件。 |
MQLib 使用的 OR-Library 实例 g001642、g002564 和 g002776 | J. E. Beasley;OR-Library 法律页面,MIT | 保留 Beasley 版权、完整 MIT 文本和 MQLib 变换署名。该依据仅覆盖这三个实例。参见 MQLib 实例族记录。 |
| ROADEF/EURO 2012 实例、重排副本和 Google 判分器 | 固定 Google OR-Tools 源码,Apache-2.0 | 保留 Google 署名、许可,以及源码文件和数据的修改说明。来源链记录标明对应材料。 |
| ROADEF 竞赛 PDF 和项目生成的参考分配方案 | 官方竞赛页面;参考分配方案由本项目生成 | PDF 的再分发条款尚未确定,请从官方来源获取。参考分配方案为项目生成的数值输出,记录在来源记录中。来源记录将其与 PDF 和判分器代码分别标明。 |
ROADEF 判分器源码:environment/app/checker-src/ | Copyright 2011 Google Inc. All Rights Reserved.;上述固定官方源码,Apache-2.0 | 保留 Google 版权和许可,并标明空行修改。参见来源比较。 |
Qute 源码:tasks/solver/online/qbf-qbfeval/environment/app/qute/ | Friedrich Slivovsky 和 Tomáš Peitl;固定源码;作者软件补充材料中的 MIT 条款 | 保留源码版本、版权、完整许可,以及许可添加于较旧源码快照之后这一说明。后来的 MIT 声明是否适用于较旧快照尚未确认。参见版本比较。 |
| Qute 随附的 MiniSat 和 docopt.cpp | 原组件作者;随附 MiniSat、LICENSE-MIT 和 LICENSE-Boost-1.0 文件 | 分别保留各组件原始声明,包括 docopt.cpp 的两份许可文本。 |
| qrp2rup | Tomáš Peitl;2026 年 CC BY 4.0 软件补充材料,署名 Tomáš Peitl 和 Leroy Chew | 署名来源、标明修改,并随二进制文件提供对应源码和声明。参见来源记录和材料列表。 |
| drat-trim | Marijn Heule 和 Nathan Wetzler;固定源码头,MIT | 分发二进制文件时,保留源码头中的版权、许可和免责声明。 |
| QBFEVAL 数据、公开和隐藏实例及变换副本 | QBFEVAL 2020 官方规则;ParaProofa v1 补充材料,CC BY 4.0 | 署名 Mark Peyrer、Maximilian Heisinger、Martina Seidl 及原始实例族。三个 BMC 实例保留 University of Toronto 2007 非商业教学研究条款。参见逐实例来源记录和所含材料列表。 |
log4j 1.2.8 条款要求的确切致谢原文为:“This product includes software developed by the Apache Software Foundation (http://www.apache.org/).” 完整原始条款位于 third-party/Log4j-1.2.8-Apache-1.1.txt。
Lean、构造与系统组件
读法说明:每行列出固定组件或数学数据来源。
| 资源 | 来源与条款 | 署名与分发条件 |
|---|---|---|
| Lean 4.33.0-rc1 和 elan 4.2.3 | Lean 许可和 elan 许可,Apache-2.0 | 保留两者声明,以及镜像所含组件适用的声明。 |
mathlib 提交 5b3f719bf129e3cf48daf6ff76a2ec5cb6e9b1e3 | 固定 mathlib 许可,Apache-2.0 | 保留文件级版权头。源码、编译缓存、版本和声明应相互匹配。 |
| Batteries、Aesop、Qq、ProofWidgets、ImportGraph、LeanSearchClient 和 Plausible | 各固定提交的许可;Apache-2.0 声明位于 third-party/ | 保留组件声明。ProofWidgets 生成的浏览器代码包含使用各自许可的依赖;参见前端许可记录。 |
Lean4 CLI 提交 da07ca808b6718cb2aed14dba154e5a08b8f8ecf | mhuisi;固定许可,MIT | 保留其 MIT 声明;它独立于 Lean 的 Apache-2.0 许可。 |
| 基于 FormalizedFormalLogic/Foundation 的 Frege 定义层 | 上游许可,Apache-2.0 | 署名 FormalizedFormalLogic/Foundation 贡献者,保留许可及来源记录中的改编说明。 |
含 136 个码字的二元码参考:tasks/construction/binary-code-a24-10/solution/ | Laaksonen 和 Östergård;根据论文中的参数和轨道代表元转换得到 | 署名作者并标明来源。任务内容包含转换后的码字。参见参考记录。 |
| 极值图参考:124 个顶点、629 条边及 Lean 编码 | Jan Goedgebeur、Jorik Jooken、Gwenaël Joret 和 Tibo Van den Eede;固定上游来源,GPL-3.0 | GPL-3.0 适用于上游代码和图数据。保留原图、Lean 源码、署名、GPL 文本和转换说明。包含 GPL 材料的组合作品必须满足 GPL 条款。参见来源记录和组件文件列表。 |
| 本地生成示例,包括 Petersen 图、交叉多胞形和根系 | 各任务的生成代码和说明 | 将数学对象数据与复制的代码和第三方程序分别处理;对实际材料应用各来源条款。 |
容器镜像包含 Debian、Ubuntu、GNU 工具、Java、Python 和其他系统组件。各组件保留自身许可。保留组件声明,并在要求时提供对应源码。精确版本和源码位置见系统许可材料。
ProofWidgets 中嵌入的 Graphviz 15.0.0 采用 EPL-2.0;外层 @hpcc-js/wasm 包采用 Apache-2.0。分发时必须包含 EPL 文本,并提供获取 Graphviz 源码及修改的可用途径。Expat 2.8.1、Emscripten 6.0.0 和 Penrose Rust 组件保留原始许可;参见内嵌组件记录。
Full 附加材料
以下声明也适用于 Full 和同源离线包:
- JSPLIB 数据: ScheduleOpt/benchmarks 及相应改编采用 CC BY-SA 4.0。署名原始实例作者和 ScheduleOpt 贡献者;参见来源记录。
- MCQD 最大团代码:
mcqd_anytime.h带有 Janez Konc 的 GPL-3.0-or-later 声明。保留其文件头,并标明节点限制、时间限制、输出移除和最优性查询修改。 - 电路定义: Copyright 2026 Samuel Schlesinger,Apache-2.0;用于
np-vs-acc和nexp-vs-tc0,修改见源码头说明。 - 张量秩定义: Copyright 2026 Jeroen Zuiddam,Apache-2.0;形式化源码署名 Christandl、Hoeberechts、Nieuwboer、Vrana 和 Zuiddam。参见逐任务来源记录。
- 排序网络比较器: Green 1969;相同的比较器数据来自固定 SorterHunter 文件,Copyright 2017 Bert Dobbelaere,MIT。分发转换后的 Lean 元组时,保留署名和许可。
- PACE 2019 实例: M. Ayaz Dzulfikar、Johannes K. Fichte 和 Markus Hecher;官方 Zenodo 记录 3368306,CC BY 4.0。保留其他原始来源和转换说明。
- MaxSAT Evaluation 2026 补充材料: Dieter Vandesande、Christoph Jabs、Jeremias Berg、Johannes Fichte、George Katsirelos、Ruben Martins、André Schidler 和 Dominik Schreiber;Zenodo 记录 21358014,CC BY 4.0。保留实例族署名;所含求解器软件保留自身许可。
- PACE 2024 判分器: Copyright 2023 Philipp Kindermann、Fabian Klute 和 Soeren Nickel,MIT。保留所含 wheel 中的声明。
逐任务许可记录标明其他 MIT、BSD 风格、CC0、Apache 和 GPL 组件。对于条款尚未确认的材料,遵循分发条件。