# 数据模型、算法与验收约束

Family 表示有序宇宙 `[0,n)` 的有限子集的集合。0 表示空族，1 表示只含空集的族。
节点 `(v,lo,hi)` 表示 lo 中的成员加上 hi 成员附加 v；子节点项号严格递增。
`hi=0` 节点被省略；同一 `(v,lo,hi)` 共享节点；`lo=hi` 不会被省略。
缺失变量表示该项不在任何成员中，不能套用 ROBDD 的缺失变量规则。

## 构建与所有权

所有 Family 不可变、无全局 manager 身份。组合时两个输入导入本次临时 Engine，
通过唯一表重建节点；操作结束只保留从结果根可达的节点，并维持子先于父的编号。
构造或预算失败不修改输入。GraphData 导入和导出均不共享可修改的数组。
默认节点上限包含两个终端；工作步数包括导入、递推和最终压缩，因而节点很少的输出
也可能因中间图或计算量触及预算。宇宙上限 256 同时限制正常图递归的深度。
这些上限不保证固定内存字节数或实时响应时间。

## 递推与复杂度

二元集合代数按两根中较早的变量分裂；不存在该变量的一侧分为 `(id,0)`。
union/intersection/difference 缓存节点对，最坏访问两个输入节点数之积；中间唯一表
与最终压缩仍计入预算。逐成员并、交、差是对成员的笛卡尔积计算，不等同于族的交并差。
乘积递推会组合多个子结果，输出大小和求极小成员的中间图可能指数增长。

minimal/maximal 使用包含关系筛除递推移除非极值成员；transversals 在边族的
节点上计算极小击中集，空边使结果为空、空边族结果只含空集。该过程不先枚举边，
但不承诺对任意输入多项式时间。rename 重建顺序，不能只替换变量标签。

计数是按子先于父的 DAG 动态规划，时间 O(N)、内存 O(N)，使用受检 UInt64 加法。
rank/unrank 利用低边成员数；page 先定位偏移再逐成员定位，适用于有界页面。
occurrences 乘合根到节点的前缀路径数与高边后缀成员数，避免共享节点漏计。
权重极值、大小界和端点见证按 DAG 动态规划，不枚举全部成员。
投影、闭包、包含关系与乘积依赖输出共享程度，均不宣称压缩率下界。

## 交换格式与错误

严格 GraphData/JSON 协议见 [format.md](format.md)。导入先检查版本、根、宇宙、
有序边、零抑制、唯一性及全部节点可达性；JSON 还限制文本长度、解析深度、字段与重复键。
计数及权重不静默回绕；枚举和分页明确报告完整性。DOT 超限报错，不返回残图。

## 可复现验收映射

- `oracle_wbtest.mbt`：独立位掩码集合模型检查小宇宙全部族及选定族对；预期不复用图递推。
- `boundaries_wbtest.mbt`：最大宇宙、预算失败原子性、非法预算、计数与负权溢出。
- `exchange_wbtest.mbt`、`json_wbtest.mbt`：恶意图、序列化及数据所有权。
- 其他 `*_wbtest.mbt`：各公共能力、终端、次序、空输入和错误分支。
- `examples/configurations`、`examples/coverage`、`examples/itemsets`：三个真实下游流程。
- `.github/workflows/ci.yml`：固定编译器、四后端严格检查、构建、测试与示例；结果以对应提交 CI 为准。

独立模型验证有限域语义，不能证明任意规模性能、无漏洞或与 Graphillion 完全兼容。