🥮 mooncakes.io

    moonmatroid

    有限拟阵建模、共同独立集选择与可检查的最优性证书

    matroid
    combinatorics
    optimization
    independence
    Download zip
    Version
    0.1.0
    License
    MIT
    Repository
    Last updated
    7 hours ago
    Downloads
    3

    No dependencies

    #MoonMatroid

    MoonMatroid 是纯 MoonBit 的有限拟阵建模与组合选择库。将“每组最多选几个”“边集不能成环”“二进制特征必须线性独立”等约束表示为秩函数，可以查询结构、做最优加权选择，或在两个约束系统间寻找最大共同独立集，并检查其最优性证书。

    模块：yujieMamba/moonmatroid@0.1.0。许可证：MIT。运行时仅使用 MoonBit 核心类型，不依赖外部求解器或网络。

    #用途与完整工作流

    使用者输入与处理输出和可运行例子
    排班、申请分配工具开发者申请 ID、部门上限与时段上限；构造两个分区拟阵并求交最大数量的可行申请、可独立检查的秩上界；examples/quotas
    网络设计与图算法开发者端点和边类别；图拟阵与分区拟阵求交，再按两个森林分层不成环且满足配额的边集、独立森林分解；examples/network
    二进制编码与特征分析开发者GF(2) 列向量、整数收益和待收缩特征最优加权基、收缩后的精确模型、可恢复的秩快照；examples/features

    这些是可复用的程序接口与确定性示例，不是已部署的业务系统。一般线性规划、任意布尔约束或三个拟阵求交不在范围内。

    #安装与快速开始

    开发和 CI 固定使用 moonc v0.10.18+6c83a7f62（高于验收要求的 0.10.16），对应 MoonBit 官方工具链。先按 MoonBit 安装文档 安装，再执行 moon version --all 和 moonc -v。支持 js、wasm、wasm-gc 和 Linux native；JS 示例需要 Node.js，Linux native 需要 C 编译器。Windows 本机验证范围另见验收记录。

    在新的空目录创建消费者项目：

    moon new selection-demo --user demo --name selection-demo
cd selection-demo
moon add yujieMamba/moonmatroid@0.1.0

    将 cmd/main/moon.pkg 设置为：

    import {
      "yujieMamba/moonmatroid" @matroid,
      "moonbitlang/core/debug",
    }
    pkgtype(kind: "executable")

    将 cmd/main/main.mbt 设置为：

    ///|
    fn main {
      let department = @matroid.Matroid::partition([0, 0, 1], [1, 1]) catch { _ => abort("department") }
      let slot = @matroid.Matroid::partition([0, 1, 0], [1, 1]) catch { _ => abort("slot") }
      let result = @matroid.intersect(department, slot) catch { _ => abort("intersection") }
      @matroid.verify_intersection(department, slot, result) catch { _ => abort("certificate") }
      println("quota selection: \{@debug.to_string(result.elements)}")
      println("upper bound: \{result.left_rank + result.right_rank}")
    }

    moon check --target js --deny-warn
moon run cmd/main --target js --deny-warn

    预期输出：

    quota selection: [1, 2]
upper bound: 2

    这组输入有意包含贪心陷阱：单独先选 0 会挡住 1、2；求交通过最短增广路交换，最终选择 1、2。示例用 abort 简化顶层错误处理；实际应用应捕获 MatroidError 并向调用方报告错误。

    #模型与 API

    所有 ground ID 为 0..ground_size-1，一般上限 64。构造器复制输入，公开的 Matroid 字段不可由下游修改。集合输入会拒绝重复和越界 ID，再转为升序。relabel 保留传入排列；restrict_to、delete、contract 的新 ID 对应保留的原 ID 升序。

    能力入口关键语义
    基础模型Matroid::uniform/free/zero固定秩上限、自由拟阵、全环拟阵
    分区与层次配额Matroid::partition/laminar分组上限；层次集合必须嵌套或不相交
    图与 GF(2)Matroid::graphic/binary支持自环、平行边、不连通图；位向量精确消元
    二部可匹配性Matroid::transversal、transversal_assignment选中的左端点是否能匹配；恢复最大匹配见证
    外部有限模型Matroid::from_ranks至多 12 元；逐项检查所有局部秩公理，不信任外部函数
    结构查询rank/independent/nullity/closure/basis/is_basis/is_circuit/spans/is_flat精确秩与闭包、基、回路
    交换结构fundamental_circuit/fundamental_cocircuit/loops/coloops/connectivity明确前置条件；不合法请求抛错
    变换relabel/restrict_to/delete/contract/dual/truncate/direct_sum依赖集也可收缩，使用标准秩公式
    扩张与分解add_loop/add_coloop/parallel_extension/free_extension/series_extension新元素 ID 为旧 ground 大小
    平行类和连通分量parallel_classes/simplify/components/component_factors/is_simple/is_connected简化保留原 ID 映射；环、余环各为单元素分量
    加权优化weighted_basis、max_weight_independent整数权；基可含负权，后者忽略非正权；总权重 Int64
    无权求交intersect、verify_intersection最大基数共同独立集；独立复算秩上界
    并集分解union_partition、verify_partition复制 ground 上求交；输出互不重叠的各拟阵独立块
    有界枚举与不变量bases/circuits/flats/rank_distribution/tutte/tutte_at完整枚举或报错，不返回伪装成完整的部分结果
    交换格式encode、decode_snapshot版本化 ASCII 秩表，恢复时重新检查公理

    完整类型和参数见根目录生成的 pkg.generated.mbti，约束和证书含义见 API 说明。

    #证书与资源边界

    intersect(M1,M2) 返回独立集 I 与集合 U，满足：

    |I| = rank_M1(U) + rank_M2(E \ U)

    右侧是任意共同独立集大小的上界。verify_intersection 重新检查两边独立性、集合合法性和上界相等，独立于搜索路径。oracle_calls 和 augmentations 只用于诊断，不参与证明。两模型必须使用相同 ground ID 语义；只有大小相同无法替调用者保证业务标签一致。

    • 求交 max_calls 默认 1,000,000，允许 1..10,000,000；预算以秩调用次数计，不是时间或内存限额。超限抛出 BudgetExceeded。
    • 并集要求 1..64 个模型且 模型数 × 元素数 <= 64；无权最大基数，不提供加权并集。
    • 图端点、二部右侧顶点至多 256；GF(2) 行数至多 64；层次约束至多 128 项。
    • 枚举与 Tutte 至多 18 元，max_subsets 上限 262,144，开始前检查完整子集数量；指数成本明确存在。tutte_at 仅接受 -2..2 整数坐标，保证 Int64 中间值有界。
    • 秩快照至多 12 元。规范格式 MM1:n:r0,r1,...，无末尾换行，位掩码升序；只接受规范十进制数字，拒绝多余字段、前导零、空白、Unicode 数字和不满足公理的表，输入长度上限 16,384 个 UTF-16 单元（合法内容均为 ASCII）。
    • 不提供加权拟阵求交、实数矩阵容差、无限 ground、任意用户回调、HOL 定理证明、通用 LP/SAT 或持久化服务。未做性能领先或任意规模可用的承诺。

    #从源码复现

    git clone https://github.com/yujieMamba/moonmatroid.git
cd moonmatroid
moon info
moon fmt --check
moon check --target js --deny-warn
moon build --target js --deny-warn
moon test --target js --deny-warn
moon run examples/quotas --target js --deny-warn
moon run examples/network --target js --deny-warn
moon run examples/features --target js --deny-warn

    将 js 换成 wasm、wasm-gc 或 Linux 的 native 即运行对应后端。示例输出保存在 工作流说明。CI 对四个后端分别执行检查、构建、测试和三个示例，并检查格式、公开接口与独立穷举样本可再生成性。

    22 个命名测试块包含固定边界用例及独立 oracle：48 个模型 × 64 子集秩、144 个加权最优值、全部 16 个三元素拟阵的 256 对求交、128 对混合模型求交、24 对并集穷举、768 个对偶 Tutte 网格关系。它们是实测用例数量，不是代码覆盖率。没有宣称 100% 分支覆盖。

    独立 oracle 仅使用 Python 标准库，采用可行子集、注入匹配和 XOR 闭包穷举生成答案，而非调用 MoonMatroid：

    python tools/oracle.py
moon fmt
git diff --exit-code

    详见 测试方法、实测样本计数、验收映射 和 语义查重。

    #来源、许可证与 AI 使用

    本项目采用 MIT，为此次任务在独立仓库原创编写；没有移植、复制或嵌入 SageMath、HOL Light、moongraph 等项目代码或数据。SageMath 的有限拟阵概念与 API 用作成熟行为参考，具体边界、相关项目许可证及独立实现方法见 参考与归属。使用 MoonBit 官方标准工具链与标准库。开发中使用 AI 辅助设计、编码、生成独立测试、调试和文档；测试与来源披露不替代参赛者对成果的责任。

    MatroidError

    source
    pub suberror MatroidError {
      InvalidInput(String)
      InvalidCertificate(String)
      BudgetExceeded(String)
    }

    Intersection

    source
    pub(all) struct Intersection {
      elements : Array[Int]
      certificate : Array[Int]
      left_rank : Int
      right_rank : Int
      oracle_calls : Int
      augmentations : Int
    }

    U certifies |I|=r_left(U)+r_right(E\U). Calls counts actual rank evaluations.

    Matroid

    source
    pub struct Matroid {
      size : Int
      model : String
      evaluate : (Array[Int]) -> Int
    }

    A finite, exactly evaluated matroid. Constructors own their inputs.

    Matroid::add_coloop

    source
    fn Matroid::add_coloop(self : Matroid) -> Matroid raise MatroidError

    Matroid::add_loop

    source
    fn Matroid::add_loop(self : Matroid) -> Matroid raise MatroidError

    Matroid::bases

    source
    fn Matroid::bases(self : Matroid, max_subsets? : Int) -> Array[Array[Int]] raise MatroidError

    Complete enumeration in ascending bitmask order, or an explicit budget error. The budget is charged before traversal; a partial answer is never returned.

    Matroid::basis

    source
    fn Matroid::basis(self : Matroid, subset : Array[Int]) -> Array[Int] raise MatroidError

    Matroid::binary

    source
    fn Matroid::binary(rows : Int, columns : Array[UInt64]) -> Matroid raise MatroidError

    Columns are UInt64 bit vectors over GF(2), low bits are row indices.

    Matroid::circuits

    source
    fn Matroid::circuits(self : Matroid, max_subsets? : Int) -> Array[Array[Int]] raise MatroidError

    Matroid::closure

    source
    fn Matroid::closure(self : Matroid, subset : Array[Int]) -> Array[Int] raise MatroidError

    Matroid::coloops

    source
    fn Matroid::coloops(self : Matroid) -> Array[Int]

    Matroid::component_factors

    source
    fn Matroid::component_factors(self : Matroid) -> Array[(Array[Int], Matroid)] raise MatroidError

    Recover a structural decomposition, retaining the original labels per factor.

    Matroid::components

    source
    fn Matroid::components(self : Matroid) -> Array[Array[Int]] raise MatroidError

    Connected components of the circuit equivalence relation. Fundamental circuits of any basis generate this relation; no powerset walk. A loop and a coloop are each singleton components.

    Matroid::connectivity

    source
    fn Matroid::connectivity(self : Matroid, subset : Array[Int]) -> Int raise MatroidError

    Connectivity across an explicit bipartition, lambda(A)=r(A)+r(E-A)-r(E).

    Matroid::contract

    source
    fn Matroid::contract(self : Matroid, contracted : Array[Int]) -> Matroid raise MatroidError

    Contracts even dependent sets using r(X union C)-r(C).

    Matroid::delete

    source
    fn Matroid::delete(self : Matroid, removed : Array[Int]) -> Matroid raise MatroidError

    Matroid::direct_sum

    source
    fn Matroid::direct_sum(self : Matroid, right : Matroid) -> Matroid raise MatroidError

    Disjoint concatenation; right element j becomes left.size+j.

    Matroid::dual

    source
    fn Matroid::dual(self : Matroid) -> Matroid

    Matroid::encode

    source
    fn Matroid::encode(self : Matroid) -> String raise MatroidError

    Versioned, canonical ASCII snapshot: MM1:n:r0,r1,...\n (no final newline). Rank rows are in bitmask order and revalidated on decoding, not trusted.

    Matroid::flats

    source
    fn Matroid::flats(self : Matroid, max_subsets? : Int) -> Array[Array[Int]] raise MatroidError

    Matroid::free

    source
    fn Matroid::free(n : Int) -> Matroid raise MatroidError

    Matroid::free_extension

    source
    fn Matroid::free_extension(self : Matroid) -> Matroid raise MatroidError

    Free extension at n lies in full closure but in no proper flat.

    Matroid::from_ranks

    source
    fn Matroid::from_ranks(n : Int, ranks : Array[Int]) -> Matroid raise MatroidError

    Fully checks local rank axioms; these imply all finite rank axioms. Tables are limited to 12 elements (4096 rows).

    Matroid::full_rank

    source
    fn Matroid::full_rank(self : Matroid) -> Int

    Matroid::fundamental_circuit

    source
    fn Matroid::fundamental_circuit(self : Matroid, independent : Array[Int], e : Int) -> Array[Int] raise MatroidError

    Matroid::fundamental_cocircuit

    source
    fn Matroid::fundamental_cocircuit(self : Matroid, basis : Array[Int], e : Int) -> Array[Int] raise MatroidError

    Matroid::graphic

    source
    fn Matroid::graphic(vertices : Int, edges : Array[(Int, Int)]) -> Matroid raise MatroidError

    Edge IDs are stable, including loops and parallel edges. Vertices <=256.

    Matroid::ground

    source
    fn Matroid::ground(self : Matroid) -> Array[Int]

    Matroid::ground_size

    source
    fn Matroid::ground_size(self : Matroid) -> Int

    Matroid::independent

    source
    fn Matroid::independent(self : Matroid, subset : Array[Int]) -> Bool raise MatroidError

    Matroid::is_basis

    source
    fn Matroid::is_basis(self : Matroid, subset : Array[Int]) -> Bool raise MatroidError

    Matroid::is_circuit

    source
    fn Matroid::is_circuit(self : Matroid, subset : Array[Int]) -> Bool raise MatroidError

    Matroid::is_connected

    source
    fn Matroid::is_connected(self : Matroid) -> Bool raise MatroidError

    The empty matroid has zero components and is not connected by this API.

    Matroid::is_flat

    source
    fn Matroid::is_flat(self : Matroid, subset : Array[Int]) -> Bool raise MatroidError

    Matroid::is_simple

    source
    fn Matroid::is_simple(self : Matroid) -> Bool

    Matroid::kind

    source
    fn Matroid::kind(self : Matroid) -> String

    Matroid::laminar

    source
    fn Matroid::laminar(n : Int, sets : Array[Array[Int]], capacities : Array[Int]) -> Matroid raise MatroidError

    Sets must be nested or disjoint; missing root is equivalent to capacity n.

    Matroid::loops

    source
    fn Matroid::loops(self : Matroid) -> Array[Int]

    Matroid::max_weight_independent

    source
    fn Matroid::max_weight_independent(self : Matroid, weights : Array[Int]) -> Selection raise MatroidError

    Maximum weight independent set; nonpositive weights are omitted.

    Matroid::nullity

    source
    fn Matroid::nullity(self : Matroid, subset : Array[Int]) -> Int raise MatroidError

    Matroid::parallel_classes

    source
    fn Matroid::parallel_classes(self : Matroid) -> Array[Array[Int]]

    Nonloop parallel classes in increasing representative order. The rank-two test works for all supported representations, including minors.

    Matroid::parallel_extension

    source
    fn Matroid::parallel_extension(self : Matroid, element : Int) -> Matroid raise MatroidError

    Adds a parallel copy at element n. A copy of a loop is a loop.

    Matroid::partition

    source
    fn Matroid::partition(groups : Array[Int], capacities : Array[Int]) -> Matroid raise MatroidError

    Group labels index capacities; absent groups and zero capacities are valid.

    Matroid::rank

    source
    fn Matroid::rank(self : Matroid, subset : Array[Int]) -> Int raise MatroidError

    Matroid::rank_distribution

    source
    fn Matroid::rank_distribution(self : Matroid, max_subsets? : Int) -> Array[Array[Int64]] raise MatroidError

    Entry [cardinality][rank] counts all subsets with those invariants.

    Matroid::rank_snapshot

    source
    fn Matroid::rank_snapshot(self : Matroid) -> Array[Int] raise MatroidError

    Matroid::relabel

    source
    fn Matroid::relabel(self : Matroid, order : Array[Int]) -> Matroid raise MatroidError

    The returned ground is reindexed by the supplied ordered labels.

    Matroid::restrict_to

    source
    fn Matroid::restrict_to(self : Matroid, retained : Array[Int]) -> Matroid raise MatroidError

    Retained labels are ascending; new index i denotes retained[i].

    Matroid::series_extension

    source
    fn Matroid::series_extension(self : Matroid, element : Int) -> Matroid raise MatroidError

    Series extension is dual to a parallel extension.

    Matroid::simplify

    source
    fn Matroid::simplify(self : Matroid) -> Simplification raise MatroidError

    Mapping arrays are independent snapshots; modifying them leaves the model intact.

    Matroid::spans

    source
    fn Matroid::spans(self : Matroid, subset : Array[Int]) -> Bool raise MatroidError

    Matroid::transversal

    source
    fn Matroid::transversal(rights : Int, neighbors : Array[Array[Int]]) -> Matroid raise MatroidError

    Ground elements are left vertices; a set is independent iff matchable.

    Matroid::truncate

    source
    fn Matroid::truncate(self : Matroid, rank : Int) -> Matroid raise MatroidError

    Matroid::tutte

    source
    fn Matroid::tutte(self : Matroid, max_subsets? : Int) -> Array[TutteTerm] raise MatroidError

    Expand sum_A (x-1)^(r(E)-r(A)) (y-1)^(|A|-r(A)). At n<=18 every coefficient and signed intermediate sum fits Int64.

    Matroid::tutte_at

    source
    fn Matroid::tutte_at(self : Matroid, x : Int, y : Int, max_subsets? : Int) -> Int64 raise MatroidError

    Integer evaluation restricted to -2..2 so all n<=18 intermediates fit Int64.

    Matroid::uniform

    source
    fn Matroid::uniform(n : Int, rank : Int) -> Matroid raise MatroidError

    Matroid::weighted_basis

    source
    fn Matroid::weighted_basis(self : Matroid, weights : Array[Int], maximize? : Bool) -> Selection raise MatroidError

    Optimal-weight basis, even when all weights are negative.

    Matroid::zero

    source
    fn Matroid::zero(n : Int) -> Matroid raise MatroidError

    Selection

    source
    pub(all) struct Selection {
      elements : Array[Int]
      weight : Int64
      rank : Int
    }

    Owned result arrays; mutating them cannot mutate the input model.

    Simplification

    source
    pub(all) struct Simplification {
      matroid : Matroid
      representatives : Array[Int]
      classes : Array[Array[Int]]
      removed_loops : Array[Int]
    }

    Restriction to one representative per nonloop parallel class. representatives[i] maps simplified ID i to the original ground.

    TutteTerm

    source
    pub(all) struct TutteTerm {
      x_degree : Int
      y_degree : Int
      coefficient : Int64
    }

    A term cx^x_degreey^y_degree in the ordinary Tutte polynomial.

    UnionSelection

    source
    pub(all) struct UnionSelection {
      elements : Array[Int]
      groups : Array[Array[Int]]
      proof : Intersection
    }

    Maximum-cardinality union selection and its disjoint independent blocks.

    decode_snapshot

    source
    fn decode_snapshot(text : String) -> Matroid raise MatroidError

    Strict decode: 16KiB cap, canonical decimals, exact row count, all rank axioms.

    intersect

    source
    fn intersect(left : Matroid, right : Matroid, max_calls? : Int) -> Intersection raise MatroidError

    Shortest augmenting paths for maximum cardinality common independence. Two matroids must share identical ground IDs. Weighted intersection is not offered.

    transversal_assignment

    source
    fn transversal_assignment(rights : Int, neighbors : Array[Array[Int]], subset : Array[Int]) -> Array[(Int, Int)] raise MatroidError

    Recover an actual maximum matching for the selected transversal elements. Pairs are (left element ID, right vertex ID), ordered by right ID. Unmatched elements are omitted; returned length equals the transversal rank.

    union_partition

    source
    fn union_partition(models : Array[Matroid], max_calls? : Int) -> UnionSelection raise MatroidError

    Reduce matroid union to intersection on (block, original-element) copies. The copied ground is bounded by 64; no exponential enumeration is used.

    verify_intersection

    source
    fn verify_intersection(left : Matroid, right : Matroid, result : Intersection) -> Unit raise MatroidError

    Verify primal feasibility and an Edmonds upper bound independently of BFS. Call counters are diagnostics; they do not participate in the proof.

    verify_partition

    source
    fn verify_partition(models : Array[Matroid], groups : Array[Array[Int]], covered : Array[Int]) -> Unit raise MatroidError

    Check an element-to-block decomposition, including exact coverage and disjointness.

    Source Files