XQuad 加权集合覆盖（Weighted Set Cover）示例详解：ATLEASTW 约束的 QUBO 建模与端到端求解管线

本文围绕 XQuad 仓库中 examples/weighted_set_cover 这一自包含的优化问题示例展开：它把经典 Set Cover 推广为“集合带覆盖容量、元素带需求”的加权形式，并通过 XQCP 约束编程 DSL 与 XQVM 的 ATLEASTW 指令将其编码为 QUBO 模型。读完本文，你将掌握加权覆盖类问题的 QUBO 公式化方法、problem.vec() / problem.branch() / model.apply_atleastw() 三个 DSL 关键调用的真实用法、六阶段端到端管线的每一步职责，以及如何用 uv run 在 Python 与 Rust 两种 XQVM 后端上运行并验证它。

问题定义与 QUBO 公式

加权集合覆盖是经典 Set Cover 的直接推广。经典版本的目标是选出最小的子集集合使其并集覆盖整个全集（见 set_cover 示例）；加权版本则引入两个额外的量：

• 每个集合 s 有一个覆盖容量 cap[s]；
• 每个元素 e 有一个需求 demand[e]。

目标是选择总成本最小的一组集合，使得被选集合对每个元素提供的容量之和不低于该元素的需求。形式化地：

• 输入：元素数量 E、集合数量 S、集合成本 costs、集合容量 caps、元素需求 demands、覆盖关系矩阵 covers（covers[e][s] = 1 表示集合 s 覆盖元素 e）；
• 模型：S 个二进制变量，x_s = 1 表示选择集合 s；
• 目标：最小化 sum(cost[s] * x_s)；
• 约束：对每个元素 e，sum_{s: covers[e][s]=1} cap[s] * x_s >= demand[e]，由 ATLEASTW（加权至少-k 约束）强制执行。

当所有 cap[s] 均为 1、所有 demand[e] 均为 1 时，问题退化为经典 Set Cover（约束变成“每个元素至少被一个已选集合覆盖”）。因此加权版本引入了容量与需求的不均衡性：一个高容量集合可能同时满足多个元素，而一个低成本低容量集合可能只满足单一元素，取舍空间更接近现实中的资源分配场景。

DSL 关键方法：vec、branch 与 apply_atleastw

该示例只用到了三个建模原语，但每个都直击 XQCP 建模的核心：

• problem.vec() —— 分配一个无类型向量寄存器，返回符号化的 VecRef。源码实现见 xqcp/problem.py：problem.vec() 会从分配器申请一个寄存器并记录 vec_alloc action，之后通过 .push() 追加元素（编译后对应 VECPUSH 指令）。
• problem.branch(cond, arm, default) —— 多臂条件分支。签名是变长的 (condition, callable) 对，最后一个参数是必须提供的默认分支（可以是 None），采用“首个匹配”语义，最少需要 3 个参数（见 xqcp/problem.py）。在加权集合覆盖中，它依据覆盖标志 covers_es 决定是否把 (set_index, capacity) 对压入该元素的索引/系数向量。
• model.apply_atleastw(indices, coeffs, k, penalty) —— 加权至少-k 约束，强制 sum(coeffs<a href="https://link.gitcode.com/i/55664855e6c0a9e70c83f50960f6587d" target="_blank">j] * x[indices[j]]) >= k。方法定义在 [xqcp/symbols.py，它调用 _record_atleastw（见 xqcp/problem.py）记录一个 atleastw action。

在 build_problem 中，三者组合成每个元素的一条约束（见 examples/weighted_set_cover/runner.py）：

with problem.range(0, num_elements_in) as e:
    elem_indices = problem.vec()
    elem_coeffs = problem.vec()
    with problem.range(0, num_sets_in) as s:
        covers_es = problem.stow("covers_es", covers_in.get(e * num_sets_in + s))
        cap_s = problem.stow("cap_s", caps_in.get(s))
        problem.branch(
            covers_es,
            lambda: (elem_indices.push(s), elem_coeffs.push(cap_s)),
            None,
        )
    demand_e = problem.stow("demand_e", demands_in.get(e))
    problem.model.apply_atleastw(elem_indices, elem_coeffs, demand_e, 200)

这段代码的要点：

1. 外层 range(0, num_elements_in) 为每个元素构建一条独立约束；
2. 内层 range(0, num_sets_in) 遍历所有集合，stow 把覆盖标志与容量取到寄存器中（stow 的语义是“求值表达式并存入寄存器”，见 xqcp/problem.py），branch 只在 covers_es 为真时执行两个 push——这保证了 indices/coeffs 两个向量长度一致且只含真正覆盖该元素的集合；
3. apply_atleastw(elem_indices, elem_coeffs, demand_e, 200) 用需求作为阈值 k，200 作为惩罚权重。

覆盖矩阵以扁平 Vec 形式作为运行时输入（covers_in.get(e * num_sets_in + s) 即行主序访问），与文档描述的“flat Vec of E*S entries”一致。

编译时，atleastw action 会被发射为 XQASM 指令。见 xqcp/compiler.py：

def _emit_atleastw(d: dict[str, Any], lines: list[str], indent: int) -> None:
    """Emit ATLEASTW instruction."""
    d["k"].emit(lines, indent)
    lines.append(line(f"PUSH {fmt_int(d['penalty'])}", indent))
    lines.append(line(f"ATLEASTW r{d['model'].reg} r{d['indices'].reg} r{d['coeffs'].reg}", indent))

即先求值阈值 k，压入惩罚值，然后执行 ATLEASTW model indices coeffs。同时 atleastw 被列入 _GROWING_KINDS（见 xqcp/compiler.py），意味着它会向模型追加变量（slack 变量），这一点将在后文“底层原理”小节详述。

端到端管线：三程序架构与六阶段流程

示例文档给出了六阶段管线，它对应 XQuad 的“三程序架构”（详见 docs/book/src/concepts/three-programs.md）：encoder、verifier、decoder 是三个相互独立、只通过 calldata 与输出槽通信的 XQVM 程序。

1. CP（xqcp） —— 生成随机加权覆盖实例，为每个集合声明一个二进制变量，并通过条件分支与 ATLEASTW 编码每个元素的加权需求约束。这一步在 runner.py 的 build_problem() 中完成。
2. Assemble —— 通过 xquad.asm 把 .xqasm 文本汇编为字节码（xqffi.asm.assemble_source，由 xquad/vm.py 引入）。
3. Encode —— 在选定的 XQVM 上运行 encoder 程序，产出 XQMX 模型。
4. Sample —— 求解器（SA/QPU/GPU）在模型上采样。
5. Verify —— verifier 程序检查样本是二进制的且每个需求都被满足，然后计算能量。
6. Decode —— decoder 程序提取被选中的集合。

runner.py 的 run() 函数（见 examples/weighted_set_cover/runner.py）把三程序架构落实为四次调用：

vm = VM(backend=backend)
vm.set_calldata([num_elements, num_sets, flat_covers, caps, demands, costs])
vm.set_output_slots(1)
vm.run(programs.encoder)
model = vm.outputs()[0]

solver = build_solver(solver_name, seed=seed)
sample = solver.solve(model).sample

vm = VM(backend=backend)
vm.set_calldata([num_elements, num_sets, flat_covers, caps, demands, costs, model, sample])
vm.set_output_slots(2)
vm.run(programs.verifier)
energy, valid = vm.outputs()

vm = VM(backend=backend)
vm.set_calldata([sample, num_sets])
vm.set_output_slots(1)
vm.run(programs.decoder)

• encoder 的 calldata 是问题原始输入，输出槽 1 个，产出模型；
• verifier 的 calldata 额外追加 model 和 sample，输出槽 2 个，产出 (energy, valid)——能量由 ENERGY 指令从模型与样本重新计算，而不是从求解器转发；
• decoder 的 calldata 是 [sample, num_sets]，输出槽 1 个，产出被选集合的向量。

VM 是 xquad/vm.py 提供的统一封装：它按 VMBackend.RUST 或 VMBackend.PYTHON 分派到 Rust FFI VM（xqffi.vm.Vm）或纯 Python 参考 VM（xqvm_py.Executor），并在边界处完成 XQMX/Vec 与 FFI 类型的转换。programs = problem.compile()（见 xqcp/problem.py）返回 CompiledPrograms(encoder, verifier, decoder) 三个 .xqasm 源字符串。

求解器由 xquad.sa 重导出（xquad/sa.py），build_solver(solver_name, seed=seed) 与 SOLVERS 注册表来自 xqsa。若导入或运行失败（例如所选后端未安装），runner 会打印错误并以退出码 1 结束（examples/weighted_set_cover/runner.py）。

运行方式与命令行参数

从仓库根目录运行（示例目录结构、运行与改造方法见 docs/book/src/examples/using-examples.md）：

uv run python examples/weighted_set_cover/runner.py --seed 42
uv run python examples/weighted_set_cover/runner.py --num-sets 6 --interpreter rust

命令行参数表（与 examples/weighted_set_cover/README.md 一致，实现在 examples/weighted_set_cover/runner.py）：

Flag	Default	Description
--num-elements	4	全集中的元素数量
--num-sets	5	集合数量
--solver	dwave-cpu	求解器后端（见下节）
--interpreter	python	XQVM 后端：python 或 rust
--seed	42	随机种子
-o / --output	stdout	将解码结果以 JSON 写入该路径，缺省输出到 stdout

几点运行细节：

• 数据生成逻辑（examples/weighted_set_cover/runner.py）：覆盖矩阵保证每个元素至少有一个覆盖集合（先强制置 1，再以 40% 概率补加）；容量 caps 从 [1, 3] 均匀采样；所有元素需求固定为 1；成本 costs 从 [1, 10] 均匀采样。
• 结果 JSON 由 main() 统一组织（examples/weighted_set_cover/runner.py），包含 _seed、num_elements、num_sets、covers、caps、demands、costs、selected、total_cost、is_valid、energy、valid 等字段，按键排序后输出。
• is_valid_cover（examples/weighted_set_cover/runner.py）在宿主侧独立复核“每个元素的需求被已选集合满足”，与 verifier 的检查互为印证。

求解器选择

--solver 决定采样后端，可用取值与安装方式如下（与文档表一致，安装方式来自各包的 extras 声明）：

Name	Hardware	Install
dwave-cpu	CPU（默认）	pip install xquad
dwave-qpu	D-Wave Leap 账户	pip install xquad[dwave]
cuda-gpu	NVIDIA CUDA GPU	pip install xquad[cuda]
metal-gpu	Apple Silicon（macOS）	pip install xquad[metal]
quip	Quip Network（远程矿工，环境配置）	pip install xqsa[quip]

驱动前置条件参见仓库根 README.md，各求解器的参数调优快速上手参见 xqsa/README.md。

需要注意：非默认求解器无法复现规范化输出（不同 RNG/硬件），而 example-smoke 始终使用 dwave-cpu。--interpreter 选择的是执行编译后程序的 VM 后端（python 或 rust），与 --solver 选择采样后端是两条完全独立的轴（见 docs/book/src/examples/using-examples.md）：一个正确建模的问题在两个解释器上总会得到相同的 valid 与 energy，但解码结果在存在同能量多个最优解时可能不同。

规范化输出与验证

示例文档指出：example-smoke 用 --seed 42 --solver dwave-cpu 验证两个解释器都产出 valid == 1，且该 smoke 测试是基于不变量的——只检查有效性，不比对精确输出。这一点在 scripts/example-smoke.py 的文档字符串中有明确说明：SA 对 BQM 构造顺序敏感，两个路径可能找到不同但同样有效的最优解，因此不做逐字节输出对齐。

smoke 测试的实际逻辑（scripts/example-smoke.py）：对每个示例、每种解释器（python、rust）运行 runner，取出 valid 与 energy，只要 valid != 1 就记为失败。示例清单本身由 examples/manifest.yaml 声明（dir: weighted_set_cover，标题 “Weighted Set Cover”，描述 “Select sets with capacities to cover element demands at minimum cost.”），文档页面由 scripts/gen-example-docs.py 自动生成（见 docs/book/src/examples/weighted_set_cover.md 的头部注释）。

底层原理：ATLEASTW 指令与 slack 变量

ATLEASTW 是 XQVM 指令集中“XQMX 高层函数”家族的一员，机器码 0x76，参数形式 model indices coeffs，栈上效果为 <a href="https://link.gitcode.com/i/a62e59175e6c425d33a64464ea754cec" target="_blank">..., k, penalty] → [...]（见 [spec/xqvm/ISA.md）。其语义要点：

• 从栈弹出 penalty、k；从 indices（vec<int>）读取变量索引、从 coeffs（vec<int>）读取权重；
• 在 model.size 处分配 slack 变量；对加权变量、负 slack 系数、目标 k 应用 EQUALITY 展开；
• indices 与 coeffs 长度必须匹配，否则两个实现都抛 VecLengthMismatch；k <= 0 抛 IndexOutOfBounds；权重和及其超出 k 的余量在索引顺序上累积、每个部分值做范围检查，溢出抛 ArithmeticOverflow。

数学推导见 spec/xqvm/HLF.md：要强制 Σ(w_i × x_i) ≥ k，先计算 max_excess = Σ(w_i) − k，分配 S = floor(log2(max_excess)) + 1 个 slack 变量，构造组合系数向量 [w_0, w_1, ..., w_{N-1}, −1, −2, −4, ..., −2^(S-1)]，再对目标 k 应用 EQUALITY 展开——负的 2 的幂次 slack 系数吸收超出 k 的选择量，等式 Σ(w_i × x_i) − 1×s_0 − 2×s_1 − ... = k 在可行域内成立。

与之配套的约束建模知识参见 docs/book/src/modelling/constraints.md：文档把 atleastw 归入“会越过网格追加变量”的约束族（atleast、atleastw、inequality 会直接增长 model.size），并给出 slack 变量数量公式：每个 atleast/atleastw 调用分配 floor(log2(max_excess)) + 1 个 slack 变量，当 max_excess <= 0 时不分配；同一组三个索引上，coeffs = <a href="https://link.gitcode.com/i/69d310bbe4a572380dfabdfdcb2f2b7c" target="_blank">1, 1, 1] 不额外分配、[1, 1, 2] 分配 1 个、[1, 2, 3] 分配 2 个。这也解释了为什么 XQVM 需要 EQUALITY、ATLEAST、ATLEASTW、REDUCE 这四个修改 model.size 的指令在增长前都要做大小上限检查（[spec/xqvm/HLF.md）。

在加权集合覆盖示例中，惩罚值选为 200。约束文档给出的经验法则是：惩罚必须超过任何违规赋值相对最优可行解能买到的最大目标改进；对 atleastw 这类等式形状的约束，整数超出量 d 实际支付 penalty * d^2（见 docs/book/src/modelling/constraints.md）。

小结与进一步阅读

加权集合覆盖示例是理解 XQuad 建模管线的理想切片：问题本身足够简单，却完整覆盖了“加权不等式约束如何进入 QUBO”这一核心模式——vec() 构造操作数、branch() 条件填充、apply_atleastw() 一次性完成加权约束编码，随后经过 encoder → solver → verifier → decoder 三程序管线闭环验证。想进一步深入，可以继续阅读：

• 建模 DSL 全貌：docs/book/src/modelling/README.md
• 约束形式对照表与惩罚权重选择：docs/book/src/modelling/constraints.md
• 三程序架构详解：docs/book/src/concepts/three-programs.md
• 示例总览与其他 13 个问题：examples/README.md
• 指令级规范：ATLEASTW 见 spec/xqvm/ISA.md，展开推导见 spec/xqvm/HLF.md