MoonSatKit

MoonSatKit 是面向 MoonBit 的 SAT 建模、CNF 编码与冲突诊断基础库。它适合功能开关、依赖解析、产品配置和规则校验：基础约束保持不变，调用方以临时假设提交本次选择；选择冲突时，库可以给出一个确定性的、逐项必要的 UNSAT core。

核心价值

• CnfBuilder：变量、蕴含、等价、门电路、exactly-one、顺序计数器等建模能力。
• solve_with_assumptions：无需复制业务模型或永久写入子句，即可验证临时选择。
• minimal_unsat_core：从冲突选择中删除无关项，返回 inclusion-minimal core。
• DIMACS 导入导出与可解释 DPLL trace，便于教学、调试和外部求解器对接。
• 核心代码无平台 IO 依赖，并在 Native、JavaScript、Wasm、Wasm-GC 上持续验证。

这里的 minimal 表示返回集合中每个文字都不可单独删除，不表示全局最小基数。API 明确报告有效性、SAT 状态、core、求解调用次数与说明，避免把诊断结果包装成无法验证的结论。

快速开始

let builder = @sat.CnfBuilder::new()
let local = builder.new_var("local")
let distributed = builder.new_var("distributed")
let strict = builder.new_var("strict")
builder.exactly_one([local, distributed])
builder.implies(strict, distributed)

let report = @sat.minimal_unsat_core(builder.cnf(), [strict, local])
println(report.to_json())

moon test
moon run cmd/main
moon run cmd/bench

验收入口

• assumptions.mbt：假设求解和冲突核算法。
• assumptions_test.mbt：临时性、无关项消除、逐项必要、基础 UNSAT、非法输入等测试。
• cmd/main：可直接运行的配置冲突演示。
• cmd/bench：24 个候选项的确定性工作负载，输出变量、子句、core 和 solver call 数。
• docs/RELATED_WORK.md：与社区现有 SAT 项目的边界。
• .github/workflows/ci.yml：四后端矩阵。

许可证：Apache-2.0。