# Fusekite 使用指南 Fusekite 是 MoonBit 原生布尔推理与组合逻辑规划库。使用者可以从小真值表得到精确的 SOP（与或式）或 POS（或与式），检查布尔等价性，并将 SOP 或 POS 换算为直接门数和 74HC 封装估算。ROBDD、SAT 和受限位向量接口也可以独立使用。 ## 选择入口 | 需求 | 入口与源码 | 当前范围 | | --- | --- | --- | | 小真值表化简 | `TruthSpec::new`、`minimize_sop`、`minimize_pos`；[规格](../fusekite.mbt)、[SOP](../cover.mbt)、[POS](../pos.mbt) | 单输出、1–8 输入，允许无关项 | | 检查候选 SOP/POS | `verify_sop_with_bdd` / `verify_pos_with_bdd`、`verify_sop_with_sat` / `verify_pos_with_sat`；[BDD](../bdd.mbt)、[SOP SAT](../sat_verify.mbt)、[POS 验证](../pos_verify.mbt) | 仅核对规定输出的行；SAT 可返回输入反例或预算耗尽 | | 符号布尔运算 | `BddManager`；[ROBDD](../bdd.mbt) | 固定变量序、1–32 变量；节点只在所属管理器内有效 | | CNF 或布尔表达式求解 | `CnfFormula`、`BoolExpr`、`SolverConfig`；[SAT 包](../sat/solver.mbt) | CNF 最多 4,096 变量；表达式最多 256 个源变量；确定性 DPLL | | 定宽算术约束 | `BitVec`、`QfBvProblem`；[位向量包](../smt/bitvec.mbt) | 1–8 位，同宽按位运算、回绕加减、低位乘法、等值及有符号/无符号小于 | | SOP/POS 器件数量估算 | `estimate_sop_gate_cost` / `estimate_pos_gate_cost` 和 `estimate_74hc_packages` / `estimate_74hc_pos_packages`；[门数](../gate_cost.mbt)、[目录](../parts/catalog.mbt) | 共享输入反相、二输入 AND/OR 树，按器件类型分别向上取整；POS 结果与规格宽度不符时返回 `None` | BDD 在最坏情况下可能指数增长；SAT 搜索预算为 1–1,000,000 个搜索节点，耗尽时返回 `Unknown`。位向量接口通过位爆炸调用 SAT，不提供完整 SMT、SMT-LIB 解析、除法、移位或拼接。精确化简也不保证任意规模的运行时间。 ## 运行与阅读输出 从仓库根目录运行： ```sh moon run cmd/main ``` 工具链版本与安装后的检查命令见 [README](../README.md#build-and-test)。程序依次演示互锁、BCD 显示和多数告警，再输出 DIMACS SAT 与四位回绕加法例子。 需要在自己的模块中调用库时，先看[独立状态指示灯消费者](../examples/status-indicator/README.md)： 它有独立的 `moon.mod` 和自有四输入规则，提供本地源码依赖配置、逐行断言、 错误候选的反例重放及其选择的 SOP 器件估算。从仓库根目录运行 `moon -C examples/status-indicator run .` 即可复现。 每个电路输出块包含输入名称、假设、SOP 模式、POS 零模式、项/子句数、文字数和 SOP/POS 门数/封装估算。`SOP/POS expected rows` 表示逐行核对的规定行数，三个例子分别为 4、10、8；随后是两种形式的 BDD/SAT 检查结果。SAT 使用 100,000 节点预算，反例、非法输入或 `Unknown` 都会使电路演示失败。 ## 构造自己的真值表 将输入顺序固定后，调用 `TruthSpec::new(input_count, on_set, dont_cares)`。第一个变量对应行号最高位，例如输入 `A,B,C` 的行 5 是 `101`。`on_set` 列出必须输出 1 的行，`dont_cares` 列出不约束输出的行，其余行必须输出 0。构造器拒绝越界、重复或相互重叠的行；无效规格返回 `None`。 将成功构造的规格传给 `minimize_sop` 或 `minimize_pos`，通过 `patterns()` 读取结果。两者分别按项/子句数最少、总文字数最少、排序后的模式字典序（`- < 0 < 1`）选择结果。这是两级表达成本，不是器件数量、时延或功耗的全局最优保证。 | 模式字符 | SOP 的 AND 项 | POS 的 OR 子句 | | --- | --- | --- | | `0` | 反文字，如 `!A` | 正文字，如 `A` | | `1` | 正文字，如 `A` | 反文字，如 `!A` | | `-` | 省略变量 | 省略变量 | POS 模式描述的是子句为假的输入组合，不能按 SOP 极性解读。例如 `01` 对应 POS 子句 `(A OR !B)`。空子句列表代表常量 1，一个全横线子句代表常量 0；完全无约束的规格选择 POS 常量 1。`PosSolution::evaluate(row)` 返回所选完成函数的值，行号越界返回 `None`。 使用相同规格调用相应 BDD/SAT 验证器，检查结果在规定行上是否等价。`SatEquivalence::Equivalent` 表示反例查询被判为 UNSAT；`Counterexample` 给出最高位优先的输入赋值；`Unknown` 保留未知，`InvalidInput` 表示输入不合要求。不要将预算耗尽解释为验证成功。 ## 三个可复现的电路场景 三个场景都由上述命令运行。读取对应输出块，先核对输入假设，再比较模式、规定行和 BDD/SAT 结果。完整真值表见[电路说明](../circuits/WORKED.md)，输入和独立期望向量见[示例源码](../circuits/examples.mbt)。 | 使用者与任务 | 输入规格 | 预期结果 | | --- | --- | --- | | 逻辑学习者比较双条件互锁 | `door_closed,sensor_clear`；2 输入，高有效；1 行 `[3]`，无无关项 | SOP `11`；POS `-0,0-`；四行输出 `0,0,0,1`。SOP 1 项/2 文字，POS 2 子句/2 文字；SOP、POS 均为 1 个 AND2、1 片 HC08 | | 显示逻辑学习者分析共阴极 BCD a 段 | `D8,D4,D2,D1`；1 行 `[0,2,3,5,6,7,8,9]`，无关行 `[10,11,12,13,14,15]`；源保证有效 BCD | SOP `--1-,-0-0,-1-1,1---`（4 项/6 文字）；POS `-100,0001`（2 子句/7 文字）。数字 1、4 输出 0，其余有效数字输出 1；SOP 为 2 个 NOT、2 个 AND2、3 个 OR2，HC04/08/32 各 1 片；POS 为 2 个 NOT、1 个 AND2、5 个 OR2，HC04/08 各 1 片、HC32 两片 | | 原型设计者分析两票以上告警 | `sensor_A,sensor_B,sensor_C`；3 输入，高有效且等权；1 行 `[3,5,6,7]`，无无关项 | SOP `-11,1-1,11-`，即 `BC OR AC OR AB`；POS `-00,0-0,00-`，即 `(B OR C) AND (A OR C) AND (A OR B)`。均为 3 项/子句、6 文字；SOP 为 3 个 AND2、2 个 OR2，HC08/32 各 1 片；POS 为 2 个 AND2、3 个 OR2，HC08/32 各 1 片 | BCD 行 12 的 SOP 为 1、POS 为 0，两者都符合无关项规格。若实际输入可能出现非法 BCD，应定义这些行的输出。较少 POS 子句不意味着较少器件：BCD 的 POS 子句更少，但文字更多；直接门数估算也因此需要更多 OR2。估算保留所选形式，不搜索 NAND/NOR 或混合极性网络。 ## 独立求解场景：CNF 与四位计数器 这两条路径不需要 `TruthSpec` 或器件目录。学习 SAT 的开发者可以直接求解 CNF；分析小型定宽计数器的开发者可以构造位向量约束。仍从仓库根目录运行 `moon run cmd/main`，读取最后的 `CNF / DPLL demonstrations` 和 `Bounded QF_BV demonstration` 输出块；可修改的完整代码在 [`show_sat_examples` / `show_qfbv_example`](../cmd/main/main.mbt)，导入配置在 [`cmd/main/moon.pkg`](../cmd/main/moon.pkg)。 ### 从 DIMACS 输入到 SAT、UNSAT 和预算不足 输入是以下 DIMACS 文本，正数表示变量，负数表示取反，`0` 结束一个子句。 三个子句表示 `(x1 OR x2) AND (!x1 OR x3) AND (!x2 OR x3)`： ```text p cnf 3 3 1 2 0 -1 3 0 -2 3 0 ``` 操作顺序是 `CnfFormula::parse_dimacs(text)`、检查 `Ok`/`Err`、创建 `SolverConfig::new(10_000)`，再调用 `formula.solve(config)`。 `Satisfiable(model)` 的数组下标 0、1、2 分别对应 x1、x2、x3；示例用 `formula.accepts(model)` 将模型重放到输入子句。当前确定性输出为： ```text SAT model (x1, x2, x3): 1, 0, 1 SAT model replay: all 3 input clauses satisfied contradictory units: UNSAT four-clause contradiction, budget 1: Unknown (not a proof) same four clauses, budget 10000: UNSAT ``` 第三行来自单独的 DIMACS 输入 `p cnf 1 2` 加子句 `1 0`、`-1 0`，即 `x1 AND !x1`。最后两行来自 `CnfFormula::new(2, [[1,2], [-1,2], [1,-2], [-1,-2]])`：四个子句分别排除两变量的四种赋值。在一个搜索节点的 预算下得到 `Unknown`，将同一公式预算改为 10,000 才得到 `Unsatisfiable`。 这个对照说明如何区分搜索未完成和无解；不能把 `Unknown` 当成 UNSAT。 ### 从四位回绕约束到可重放的计数器值 任务是找到四位无符号计数器加 3 后等于 2 的起始值。输入为位宽 4、常量 3 和 2，算术按模 16 回绕；不使用普通整数的无界加法。示例依次调用： ```moonbit let x = @smt.BitVec::variable(4, 1).unwrap() let three = @smt.BitVec::constant(4, 3).unwrap() let two = @smt.BitVec::constant(4, 2).unwrap() let sum = x.add_wrapping(three).unwrap() let assertion = sum.equal(two).unwrap() let problem = @smt.QfBvProblem::new(4, assertion).unwrap() let outcome = problem.solve(@sat.SolverConfig::new(10_000).unwrap()) ``` 第一个 `4` 是位宽，`variable(4, 1)` 从源变量 1 开始分配四个位； `QfBvProblem::new(4, ...)` 的 `4` 是源布尔变量数。模型按最低位优先排列， 用 `x.evaluate(model)` 取回整数，避免将位序当成真值表行号的最高位优先。 在 `Satisfiable(model)` 分支中，示例同时检查整数算式和 `sum.evaluate(model) == Some(2)`。预期输出： ```text four-bit x + 3 = 2 modulo 16; model x = 15 QF_BV model replay: (15 + 3) % 16 = 2 ``` 这两个场景的程序会在结果类型与预期不符、模型重放失败或非预期预算耗尽时 报错退出，因此 CI 的演示步骤也会失败。预算对照中预期的 `Unknown` 则必须 出现且只消耗一个搜索节点。修改输入后应重新确定预期结果；通用调用方仍需 分别处理 SAT 的三种结果，以及 QF_BV 额外的 `InvalidInput`。 ## 从逻辑结果到器件估算 将同一规格的 SOP 解交给 `estimate_sop_gate_cost`，再将门数交给 `parts/` 的 `estimate_74hc_packages`。具有 n 个文字的乘积项使用 `max(0, n - 1)` 个 AND2，多个乘积项用 OR2 树连接；同一输入的反相在各项之间共享。封装按 HC04 的 6 个反相器、HC08 的 4 个 AND2、HC32 的 4 个 OR2 分别向上取整。 目录也记录 HC00，但当前映射不做 NAND/NOR 优化。数据表来源、目录字段和估算范围见 [74HC 目录说明](../parts/74hc-catalog.md)。估算不包含引脚布线、精确封装后缀、扇出、负载、电压、时序、价格或 LED 驱动；互锁和告警是布尔教学模型，不能据此推导安全资格。 ## 验证证据与进一步阅读 仓库提供独立小规格成本 oracle、真值表枚举、BDD/SAT 交叉检查，以及固定 Z3 版本的 QF_BV 差分语料。POS 测试覆盖全部 6,561 个三输入含无关项规格，并对 1,296 组两输入规格/候选组合重放反例。这些都是有界的软件验证，不代表任意公式的正确性证明或实物测试。 - [设计契约](../DESIGN.md)：输入、不变量、排序、常量语义和求解边界。 - [开发与验证记录](../DEVELOPMENT.md)：版本、复现命令、实际检查结果及 AI 贡献披露。 - [MoonBDD 范围比较](MoonBDD与Fusekite范围对比.md)：固定版本的能力重叠和差异；Fusekite 当前没有 MoonBDD 依赖或互操作接口。 AI 编程助手对实现、测试、示例、文档及 CI 提供了实质性协助，也参与了本指南的整理。自动检查与 Git 署名不构成人工逐行审查、用户反馈或硬件验证的证据。