实验报告：lab3/report.md
本文记录现有代码的运行方法、各任务的操作和思路，以及整理回顾时的实际复跑结果。原报告和实验代码未作修改。命令用于复现；模型的打印顺序和具体方案可能因求解器版本等因素变化，应检查约束是否满足，而不是要求输出逐字相同。
实验主线是：自然语言要求 → 选择合适的变量类型 → 写出约束 → 求解 → 把模型还原为具体方案 → 独立核验和解释结果。
| 任务 | 要回答的问题 | 核心方法 |
|---|---|---|
| 1 | 同一个部署问题如何用两种模型表达？ | 12 个 Bool 编码位置，或 4 个 Int 直接表示节点 |
| 2 | 给定的排课方案是否合法？ | C++ 检查范围和冲突 |
| 3 | 能否从规则中自动找到排课方案？ | 整数范围与冲突不等式 |
| 4 | 加一后是否一定更大？ | 否定性质，寻找边界反例 |
| 5 | 规则能否推出模块发布结论？ | 谓词、量词、性质否定 |
| 6 | 部署要求为什么无解？ | 不可满足核与逐条删减 |
| 7 | 合法方案中最少需要几个时间段？ | Optimize 最小化实际使用数量 |
需要区分两类求解：
- 寻找方案：检查约束 C，sat 表示存在满足要求的方案。
- 验证性质：检查 C 与 Not(P)，sat 表示存在违反 P 的反例；unsat 表示 C 能够推出 P。
因此，任务 5 输出“存在可发布模块：unsat”并不是说没有模块可发布，而是说“不存在可发布模块”这一反例情形无法成立。前提是基础约束自身可满足。若求解器返回 unknown，不能按 sat 或 unsat 解读。
使用 Windows、PowerShell、Python 虚拟环境、z3-solver 和支持 C++17 的 G++。
从仓库根目录进入实验目录并激活已有虚拟环境：
Set-Location D:\ME\FormalMethods\lab3
.\.venv\Scripts\Activate.ps1
python z3_smoke.py环境检查输出应为：
Z3 smoke test passed
如果不想激活虚拟环境，也可以直接指定解释器。这也是本次复跑 Python 脚本采用的方式：
Set-Location D:\ME\FormalMethods\lab3
.\.venv\Scripts\python.exe -B z3_smoke.py
.\.venv\Scripts\python.exe -B mission3_2.py-B 表示不生成 Python 字节码缓存，不改变脚本的求解逻辑。本次通过一个外部 Python 驱动程序依次启动现有 14 个脚本，每个脚本单独启动解释器、收集输出并检查退出码，未改动脚本。下文为便于手动操作，将各次运行列为单独的 python 文件名.py 命令。
若新建环境，可使用以下命令准备依赖；这些是环境重建说明，不代表本次重复安装了依赖：
python -m venv .venv
.\.venv\Scripts\Activate.ps1
python -m pip install z3-solver安装包名是 z3-solver，代码中导入的是 z3。应确认安装依赖和运行脚本使用同一个 Python 环境。
python mission1.py
python mission1_2.py布尔模型中，X_G_0 等变量表示某组件是否位于某节点，共 12 个 Bool。每个组件使用一条“至少一个”子句和三条“两两不能同时选择”子句，表达恰好部署在一个节点。
五条业务要求也转换为子句。例如：
网关与数据库不在节点 0 共存：Not(g0) Or Not(d0)
认证位于节点 0 则数据库也在：Not(a0) Or d0
数据库位于节点 0 则认证也在：Not(d0) Or a0
缓存在节点 1 则网关在节点 0：Not(c1) Or g0
每次 s.add(...) 加入必须满足的约束，所有约束之间是合取。因此无需输出 DIMACS 文件，也可以直接把 CNF 表达式交给 Z3。
整数模型直接用 G、A、D、C 表示所在节点，限制在 0..2 内；相同节点写 A == D，不同节点写 G != D，条件要求写 Implies(C == 1, G == 0)。
两份脚本均返回 sat。布尔模型给出 G=0、A=1、D=1、C=1；整数模型给出 G=1、A=0、D=0、C=2。两份方案不同，但都满足五条规则，说明无需要求两次求解返回相同模型。
当前 mission1.py 对网关位置同时加入 Not(g2) 和 Or(g0, g1)。在已有“恰好一个节点”约束下，两者等价，因此有一条冗余约束：当前文件实际包含 29 条子句；只保留其中一种写法时是此前讲解的 28 条。冗余不影响模型正确性，本次未修改代码。
思路： 布尔编码需要显式描述各种位置选择，整数 SMT 可以直接表达节点值及其关系。表达更简洁不等于已经证明求解更快。
手动编译和运行方式为：
g++ -std=c++17 lab3_solution.cpp test2.cpp -o test2.exe
.\test2.exe两个文件需要一起编译：lab3_solution.cpp 提供 validSchedule 实现，test2.cpp 提供函数声明、测试数据和 main。提交用的函数文件不含 main，也不执行标准输入输出。
本次复跑使用相同的两个源文件，把可执行文件输出到系统临时目录，避免覆盖实验目录中已有的 test2.exe：
$testBinary = Join-Path $env:TEMP 'formalmethods-lab3-review-test2.exe'
g++ -std=c++17 lab3_solution.cpp test2.cpp -o $testBinary
& $testBinary函数先检查所有值是否满足 0 <= slot[i] < slotCount，再检查每条冲突是否满足 slot[u] != slot[v]。任意检查失败就返回 false，全部通过才返回 true。
| 测试 | slot | 实际返回 | 结果 |
|---|---|---|---|
| 合法方案 | [0,1,2,0,0,1] | true | PASS |
| 编号越界 | [3,1,2,0,0,1] | false | PASS |
| 冲突课程同时上课 | [0,0,2,0,0,1] | false | PASS |
| 非冲突课程共享时间段 | [0,1,1,0,0,1] | true | PASS |
最后一例中课程 1、2 都在时间段 1，但原始冲突列表没有 (1,2)，所以合法。不能要求所有课程时间段互不相同，也不能将课程数量写死为六。
python mission3.py
python mission3_2.py为六门课程分别声明 Int，将时间段限制在 0..2，对七条冲突分别加入不等式。mission3.py 复跑返回 sat，得到：
slot = [1, 0, 0, 1, 1, 2]
时间段 0：课程 [1, 2]
时间段 1：课程 [0, 3, 4]
时间段 2：课程 [5]
model.eval(s0).as_long() 把模型中的 Z3 数值读取为普通 Python 整数。六个值必须按课程编号顺序提取，不能按模型打印顺序直接抄写。
mission3_2.py 在原始七条冲突上新增 (0,3)，每次创建新 Solver，分别限制在两个和三个时间段内：
2 个时间段：unsat
3 个时间段：sat
slot = [0, 2, 2, 1, 1, 2]
集合 {0,1,3} 中存在 (0,1)、(1,3)、(0,3)，三门课程两两冲突，至少需要三个时间段。任意两门课都能用两个时间段安排，所以三门课已经是一个最小的不可二时间段排课集合。实际三时间段方案的存在说明整个问题在三个时间段内可行。
任务要求将 Z3 输出方案交给 validSchedule。当前 mission3.py 只输出方案和分组，mission3_2.py 只输出求解结果和方案；它们没有自动调用 C++。当前 test2.cpp 也只检查固定四个用例。本次复跑不将固定用例通过写成“已调用 C++ 检查全部 Z3 输出方案”。
复现这一环节时，应另行在测试程序中用实际输出构造 std::vector<int> 并调用检查函数；检查新增冲突后的方案，还要把 (0,3) 加入传入的冲突列表。也可人工逐条检查范围和全部冲突，但人工检查不替代手册要求的函数调用。
思路： 任务 2 是“方案 → 检查规则”，任务 3 是“规则 → 求出方案”。范围 0..2 只意味着允许三个时间段，不保证求解器实际用满三个。
python unsigned_increment.py
python signed_increment.py
python mission4.py三个脚本都检查“加一后更大”的否定，而不是直接断言性质成立。
| 语义 | 比较表达式 | 实际求解结果 | 反例及解释 |
|---|---|---|---|
| 8 位无符号 | Not(UGT(y, x)) | sat，x=255 | 加一只保留低 8 位，得到 0 |
| 8 位有符号 | Not(y > x) | sat，x=127 | 加一得到位模式 10000000，按有符号解释为 -128 |
| 数学整数 | Not(y > x) | unsat | Int 不发生固定位宽回绕，找不到反例 |
当前两个 BitVec 脚本只打印模型中的 x，不会单独打印 y，因为 y 是 x + 1 表达式。表中的 y 来自位运算边界的独立计算。位向量的 > 是有符号比较，UGT 是无符号比较；二者并未改变加法保留低 8 位的机制。
思路： 验证前先确定数值语义。不能把数学整数的结论直接套到机器位宽模型上，也不要把所有定宽运算结论直接当作 C++ 源程序语义的结论。
python mission5.py
python mission5_2.pyEnumSort 定义仅含 Parser、Database、UI 的模块类型。Function(..., Module, BoolSort()) 声明模块到真假的谓词，ForAll 表示所有模块遵守规则，Exists 表示至少存在一个模块。
两条规则分别为“通过测试则可以发布”和“可以发布则已经通过测试”，共同要求 Tested 与 Releasable 一致。
mission5.py 的事实是 Parser、UI 通过测试，Database 未通过测试。三个独立反例检查的实际结果为：
| 待检查性质 P | 检查基础约束与 Not(P) | 结论 |
|---|---|---|
| 存在可发布模块 | unsat | 性质成立 |
| Database 不可发布 | unsat | 性质成立 |
| 所有模块都可发布 | sat | Database 构成反例 |
输出模型中 Parser、UI 的 Tested 和 Releasable 均为 True，Database 的二者均为 False。这与前两项的 unsat 完全一致，因为 unsat 描述的是性质否定无解，不是性质为假。
mission5_2.py 将 Database 的事实替换为已通过测试，再检查全部三个性质，实际结果依次为 unsat、sat、unsat。所有模块都可发布；“Database 不可发布”反而有反例。不能保留旧的否定事实再追加肯定事实，否则基础模型本身就矛盾了。
python deployment_core.py
python mission6.pydeployment_core.py 用 assert_and_track 给每条要求附上标签，求解为 unsat 后用 unsat_core() 取得冲突标签。本次复跑得到六条容量相关标签：
api_high_availability
worker_matches_api
database_high_availability
standby_required
one_service_per_node
maintenance_capacity
它们共同推出 API 至少 2、Worker 至少 2、数据库至少 2、备用节点至少 1，总需求至少为 7，与最多 6 个节点矛盾。监控和审计两条要求未出现在核中。
mission6.py 每次创建新求解器，保留全部领域约束，从完整要求中单独删除一条。它遍历全部八条要求，因此包括题目要求的六条核约束删减，也额外检查了两条非核约束：
| 单独删除项 | 实际结果 |
|---|---|
| api_high_availability | sat |
| worker_matches_api | sat |
| database_high_availability | sat |
| standby_required | sat |
| one_service_per_node | sat |
| maintenance_capacity | sat |
| monitoring_required | unsat |
| monitoring_requires_audit | unsat |
例如不要求备用节点时可以取 2+2+2+0=6。删除监控要求不能降低副本和备用节点需求，所以容量矛盾仍然存在。删除总节点计算关系后得到 sat，只说明删减后的模型可满足，不能据此声称原部署规则仍被完整满足。
思路： 六条核约束分别删除后都变为 sat，说明当前核在固定领域约束的前提下不可继续删减。这是包含意义上的最小性，不是一般意义上已证明所有核中条数最少。某条约束未出现在当前核中，也不能推广为它在所有需求分析中都没有作用。
python mission7.py
python mission7_2.py先建立与原始排课问题相同的范围和七条冲突，再对每个时间段定义：
used[t] == Or(slot[0] == t, ..., slot[5] == t)
objective = Sum(If(used[t], 1, 0))
used[t] 必须与“至少一门课使用该时间段”真假一致，不能仅靠单方向蕴含代替。If 将真假转为 1 或 0，Sum 计算实际使用数量。随后用 Optimize() 和 minimize(objective) 寻找最小值。
本次复跑：
| 模型 | 最少时间段数 | 一份实际模型，按课程 0..5 排列 |
|---|---|---|
| 原始七条冲突 | 2 | [1,2,2,1,1,2] |
| 原始冲突新增 (1,2) | 3 | [1,2,0,1,2,0] |
原始问题至少有一条冲突边，因此一个时间段不够；两时间段方案存在，说明最优值为 2。新增 (1,2) 后，集合 {0,1,2} 两两冲突，给出至少三个时间段的下界；三时间段方案存在，说明下界可达，最优值为 3。
任务 7 新增的是 (1,2)，任务 3 新增的是 (0,3)，两者都应分别从原始七条冲突出发。
当前两个优化脚本打印模型和目标值，没有内置逐条冲突检查输出。为独立核验，本次对表中的两组方案人工逐条代入：
| 冲突对 | 原方案两端时间段 | 新方案两端时间段 |
|---|---|---|
| (0,1) | 1、2 | 1、2 |
| (0,2) | 1、2 | 1、0 |
| (1,3) | 2、1 | 2、1 |
| (2,3) | 2、1 | 0、1 |
| (2,4) | 2、1 | 0、2 |
| (3,5) | 1、2 | 1、0 |
| (4,5) | 1、2 | 2、0 |
| 新增 (1,2) | 不适用于原问题 | 2、0 |
全部适用冲突的两端均不相等，且两组方案的值均在 0..2 内。原方案只使用 {1,2}，新方案使用 {0,1,2}，计数与目标值一致。不能用最大时间段编号加一直接代表实际使用数量，例如原方案最大编号为 2，却只使用两个时间段。
本次实际执行 14 个现有 Python 脚本，均正常退出；同时以 C++17 编译现有两个 C++ 文件，四个固定测试全部 PASS。Python 输出、C++ 返回值和上述人工核验分别提供不同层面的证据，不能将其中一种替代另一种而不说明。
使用 LLM 辅助时，应记录真实提示词、实际采用或修改的代码，以及独立核验方式。有效的核验包括边界计算、逐条代入业务规则、使用独立检查函数，以及“下界证明 + 达到下界的方案”。截图用于保存实际执行证据，不能只靠预期输出充当运行结果。