XQuad 最小顶点覆盖实战：用 XQCP 构建 QUBO、ATLEAST 约束编码与端到端求解

本文以 XQuad 仓库中的 examples/vertex_cover 为例，完整讲解如何将图论经典问题——最小顶点覆盖（Minimum Vertex Cover）——转化为 QUBO（二次无约束二值优化）模型，并通过 XQCP 约束编程 DSL 建模、XQVM 三程序流水线编码/验证/解码、XQSA 求解器采样，最终在 CPU 模拟退火或 GPU/QPU 硬件后端上得到可行解。读完本文，你将掌握 problem.vec() + model.apply_atleast() 这一核心约束编码模式、ATLEAST 在底层的 slack 变量分配原理，以及如何运行、调参和验证该示例。

问题定义：什么是最小顶点覆盖

给定一个无向图 G = (V, E)，顶点覆盖（Vertex Cover）是指一个顶点子集 C ⊆ V，使得图中每条边 (i, j) ∈ E 至少有一个端点在 C 中。最小顶点覆盖则是在所有可行覆盖中寻找顶点数量最少的那个子集——它属于经典的 NP-hard 组合优化问题。

以 examples/vertex_cover/README.md 的定义为准，该示例的目标是：

找到最小顶点子集，使得无向图中的每条边至少有一个端点在该子集中。

在 XQuad 的例子里，图是随机生成的：runner.py 以 --seed 为随机种子，为 n 个节点两两之间以 60% 的概率生成边（详见 runner.py 中 rng.random() < 0.6 的判定）。

QUBO 公式化：变量、目标与约束

决策变量

输入：节点数 N、边列表（每条边为一对端点索引 (i, j)）。

模型：N 个二进制变量，x_v = 1 表示顶点 v 被选入覆盖集合。模型通过 define_model(size=N, domain=Domain.BINARY) 声明为纯二进制域，见 runner.py。

目标函数

覆盖集合要尽可能小，因此目标是最小化选入的顶点数：

minimise sum(x_v)  for v in 0..N

在 runner.py 中，这一目标通过循环为每个变量的线性系数加 1 实现：

with problem.range(0, num_nodes) as v:
    problem.model.linear[v].add(1)

约束条件

每条边 (i, j) 必须被覆盖，即两个端点中至少一个为 1：

x_i + x_j >= 1   (每条边一个约束)

这正是 ATLEAST（k=1） 约束的形态，即"这组索引中至少有 1 个变量取 1"。

ATLEAST 约束的底层编码原理

为什么需要 slack 变量

x_i + x_j >= 1 是一个不等式，而 QUBO 求解器最小化的是形如 sum(a_ij * x_i * x_j) + sum(b_i * x_i) 的二次函数，无法直接表达 >=。标准做法是引入松弛（slack）变量把不等式改写成等式，再施加平方惩罚。

对于每条边，ATLEAST 在 model.size 处分配一个 slack 变量 s ∈ {0, 1}，并加入惩罚项：

P * (x_i + x_j - 1 - s)^2

这正是 examples/vertex_cover/README.md 中给出的编码公式。三种赋值情形下的惩罚分别为：

端点取值 (x_i, x_j)	需求	slack s	惩罚项	结果
(0, 0)	违反覆盖	0	P*(0+0-1-0)^2 = P	被惩罚
(1, 0) 或 (0, 1)	恰好满足	0	P*(1+0-1-0)^2 = 0	可行
(1, 1)	超额满足	1	P*(1+1-1-1)^2 = 0	slack 吸收超额

关键在于第三条：当两个端点都被选中（和等于 2）时，等式 x_i + x_j - s = 1 需要 s = 1 来吸收超出的 1，这正是原文档所说 "s in {0,1} accounts for the case when both endpoints are selected" 的由来。

slack 数量的计算

根据 spec/xqvm/HLF.md 中 ATLEAST 的规范推导：

1. 计算 max_excess = N - k（本例每条边 N=2, k=1，即 max_excess = 1）；
2. 分配 S = floor(log2(max_excess)) + 1 个 slack 变量（本例 S = floor(log2(1)) + 1 = 1）；
3. 构建组合系数向量 [+1, +1, ..., -1, -2, -4, ..., -2^(S-1)]——原始变量为 +1，slack 变量为负的 2 的幂；
4. 以 target = k 施加 EQUALITY 展开。

即约束被展开为 sum(x_i) - 1·s_0 - 2·s_1 - ... = k。对顶点覆盖的每条边，恰好分配 1 个 slack 变量，与文档 "ATLEAST allocates one slack variable at model.size" 一致。

汇编层面的印证

仓库的一致性测试向量 conformance/vectors/constraints/atleast_basic/program.xqasm 完整展示了该机制：4 个变量、k=1、penalty=1 时，max_excess = 3，num_slacks = bit_length(3) = 2，模型尺寸从 4 增长到 6，组合系数为 [1,1,1,1,-1,-2]，随后通过 ATLEAST r0 r1 指令执行：

PUSH 1           ; k
PUSH 1           ; penalty
ATLEAST r0 r1

HLF 展开后第一个 slack 变量的线性系数为 3（证明模型确实发生了增长）。ATLEAST 在指令集层面的完整属性表见 spec/xqcp/CONSTRAINTS.md：栈输入为 penalty、k，寄存器输入为 indices_vec，副作用为"分配辅助变量"（即增长 model.size）。

runner.py 逐段解析：DSL 建模代码

声明输入与模型

problem = Problem("VertexCover")

num_nodes = problem.input("num_nodes", type=Types.Int)
num_edges = problem.input("num_edges", type=Types.Int)
edges_in = problem.input("edges", type=Types.Vec)

problem.define_model(size=num_nodes, domain=Domain.BINARY)

见 runner.py。节点数、边数、扁平化的边列表（每个端点两个整数）通过 calldata 传入；模型为 num_nodes 个二进制变量。

逐边施加 ATLEAST 约束

with problem.range(0, num_edges) as e:
    offset = problem.stow("offset", e * 2)
    ni = problem.stow("ni", edges_in.get(offset))
    nj = problem.stow("nj", edges_in.get(offset + 1))

    edge_indices = problem.vec()
    edge_indices.push(ni)
    edge_indices.push(nj)

    problem.model.apply_atleast(edge_indices, 1, 200)

见 runner.py。这里出现了原文档列出的两个 DSL 方法：

• problem.vec()：分配一个向量寄存器，用于承载每条边的两个端点索引。VecRef 支持 .push() 追加元素。
• problem.model.apply_atleast(indices, k, penalty)：ATLEAST 约束，k=1 表示"至少一个端点在覆盖中"，penalty=200 为约束权重。

problem.stow() 把表达式（如 edges_in.get(offset)）存入寄存器并返回一个可复用的寄存器引用，避免重复计算（见 problem.py）。

从源码结构看，apply_atleast 在 XQCP 内部通过 _record_atleast 记录为一个 Action("atleast", {"model", "indices", "k", "penalty"})，同时追加到 Problem._actions（编译遍历的序列）和 Problem._constraints（约束子集）两个列表，直到 compile() 时才统一生成三份汇编，见 problem.py。

声明输出

cover = problem.output("cover", type=Types.Vec)
with problem.range(0, num_nodes) as v:
    cover.append(problem.sample.getline(v))

见 runner.py。解码器把采样结果中每个变量的取值读回一个 cover 向量——这是三程序流水线中 decoder 程序的输出部分。

端到端流水线：XQuad 的三程序架构

顶点覆盖示例遵循 XQuad 全项目统一的 encoder / verifier / decoder 三程序架构（见 docs/book/src/concepts/three-programs.md），整体分为六个阶段，原文档的 Pipeline overview 与此一一对应：

阶段	组件	说明
1. CP	xqcp	随机生成图，声明每顶点一个二进制变量，逐边编码 ATLEAST 约束
2. Assemble	xquad.asm	将 .xqasm 文本汇编为字节码
3. Encode	XQVM（python/rust）	运行 encoder 程序，产出 XQMX 模型
4. Sample	XQSA 求解器	SA/QPU/GPU 对模型采样
5. Verify	XQVM	verifier 检查采样是否二进制、每条边是否被覆盖，并计算能量
6. Decode	XQVM	decoder 提取被选中的顶点集合

在 runner.py 的 run() 函数中，宿主代码依次执行三次 VM.run()，中间插入一次求解器调用：

vm = VM(backend=backend)
vm.set_calldata([n, m, flat])        # 图数据入 calldata
vm.set_output_slots(1)
vm.run(programs.encoder)             # ① encoder 产出 XQMX 模型
model = vm.outputs()[0]

solver = build_solver(solver_name, seed=seed)
sample = solver.solve(model).sample  # ② 求解器在 VM 之外采样

vm = VM(backend=backend)
vm.set_calldata([n, m, flat, model, sample])
vm.set_output_slots(2)
vm.run(programs.verifier)            # ③ verifier 输出 (energy, valid)
energy, valid = vm.outputs()

vm = VM(backend=backend)
vm.set_calldata([sample, n])
vm.set_output_slots(1)
vm.run(programs.decoder)             # ④ decoder 输出 cover 向量

三个程序通过 calldata 入、输出槽出通信，彼此不共享状态；求解发生在 VM 之外（XQVM 指令集没有"调用求解器"的指令）。VM(backend=...) 的选择由 --interpreter 决定：VMBackend.PYTHON 走纯 Python 参考实现，VMBackend.RUST 通过 xqffi FFI 走 Rust 运行时（见 vm.py）。

运行方式与命令行参数

从仓库根目录执行：

uv run python examples/vertex_cover/runner.py --seed 42
uv run python examples/vertex_cover/runner.py --n 7 --interpreter rust

完整的命令行参数表（继承自 examples/vertex_cover/README.md，并在 runner.py 的 argparse 定义中可验证）：

Flag	Default	Description
--n	5	节点数
--solver	dwave-cpu	求解器后端（见下节）
--interpreter	python	XQVM 后端：python 或 rust
--seed	42	随机种子（图生成与可播种求解器共用）
-o	stdout	将 JSON 结果写入文件而非打印到标准输出

-o 接受一个路径参数，结果以 json.dumps(indent=2, sort_keys=True) 格式写出（见 runner.py）。默认输出示例（--n 5 --seed 42 形态）：

{
  "_seed": 42,
  "_note": "canonical CI golden",
  "n": 5,
  "edges": [[0, 1], ...],
  "cover": [1, 0, 1, 0, 1],
  "cover_size": 3,
  "is_valid": true,
  "energy": -600,
  "valid": 1
}

字段说明：cover 是解码后的顶点选择；cover_size 为 sum(cover)；is_valid 由 is_valid_cover() 判定——all(cover<a href="https://link.gitcode.com/i/ed6b7fc2040408a53f002f601c356177" target="_blank">i] or cover[j] for i, j in edges)，即每条边至少一个端点被覆盖（见 [runner.py）；energy 为 verifier 重新计算的模型哈密顿量（含全部惩罚项）；valid 是 verifier 的可行性标志。

选择求解器：从 CPU 模拟退火到硬件后端

--solver 的取值由 XQSA 的求解器注册表定义，见 xqsa/registry.py。原文档的求解器表格与仓库 README 的安装前置条件合并如下：

Name	Hardware	Install
dwave-cpu	CPU（默认，模拟退火）	pip install xquad
dwave-qpu	D-Wave Leap 账号（Advantage QPU）	pip install xquad[dwave]
cuda-gpu	NVIDIA CUDA GPU（需 CUDA 12.x 驱动）	pip install xquad[cuda]
metal-gpu	Apple Silicon（macOS，Metal 设备）	pip install xquad[metal]
quip	Quip Network（远程矿工网络，环境变量配置）	pip install xqsa[quip]

要点：

• dwave-cpu 是全局默认，因为它是无需额外依赖与硬件的可复现基线（xqsa/registry.py）；example-smoke 始终使用它。
• seed 语义：dwave-cpu、cuda-gpu、metal-gpu 接受 seed 以复现；dwave-qpu 是物理硬件无 seed 概念，quip 由环境变量（QUIP_RPC_URL + 签名器）配置且不接受 seed，两者都会忽略传入的 seed（xqsa/registry.py）。
• 额外依赖按需加载：求解器类在导入时是轻量的，CUDA/Metal/D-Wave/Quip 的可选依赖只在构造或运行求解器时才引入，不可用的后端会在 build_solver 时给出可操作的错误信息（xqsa/registry.py）。
• 非默认求解器无法复现规范输出：不同后端 RNG 与硬件路径不同，会返回不同的（但同样合法的）最优解。
• GPU/QPU 的驱动前置条件与按求解器的快速上手文档见 xqsa/README.md，安装总表见仓库根 README.md。

规范输出与 CI 验证机制

example-smoke（make example-smoke，见 Makefile）会遍历 examples/*/runner.py，对每个示例在 python 与 rust 两个解释器上分别以 --seed 42 --solver dwave-cpu 运行，并断言 valid == 1。该烟测是基于不变量的——只检查可行性，不做字节级输出对比，原因见 scripts/example-smoke.py 的模块文档：

SA is sensitive to BQM construction order, so the two paths may find different (but equally valid) optima.

也就是说：encoder/verifier/decoder 三个程序在任一解释器上都是确定性的（同样的字节码输入产生同样的输出），但夹在中间的求解步骤只锚定 seed 与 dwave-samplers 版本。当模型存在多个同能量最优解时，两个解释器可能解码出不同的最优解，但 valid 与 energy 一致。example-smoke 同时通过 _require_xqffi_verifier() 强制要求 xqffi.verifier.verify_source 可导入，确保编译产物真的经过了字节码验证（scripts/example-smoke.py）。

扩展实践：惩罚权重的选择与调试

apply_atleast(edge_indices, 1, 200) 中的 200 是惩罚权重 P。选择原则在 docs/book/src/modelling/constraints.md 中有完整论述，对顶点覆盖尤其直接：

• 安全上界：P 必须大于任何违规赋值相比最优可行解能获得的收益。本例目标 sum(x_v) 中每个变量至多贡献 1，因此所有系数绝对值之和为 N，取 P > N 恒可拒绝违规——200 对于默认的 n=5（上限 5）绰绰有余。
• 精确边界：ATLEAST 的惩罚项是 P * d^2（d 为整数超额），对边约束而言违反时 d = 1，所以阈值就是"一个违规端点能省下的最大目标值"——通常远小于安全上界。
• 过高不会损坏模型：惩罚项在可行赋值上恒为 0，不会改变可行解之间的相对顺序；代价体现在硬件表示精度上。

调试时建议同时检查 JSON 输出中的两个字段：is_valid（外部独立验证，不依赖 verifier）与 valid（verifier 的二进制域检查 + 能量计算）。若出现 is_valid: false 而 valid: 1，说明采样可行但顶点覆盖约束被破坏——此时应调大 penalty；反之若能量异常偏大，可检查 energy 中惩罚项的比例。

总结

examples/vertex_cover 是理解 XQuad 约束编程全流程的最小而完整的样例：一条 apply_atleast(indices, 1, penalty) 调用，背后是 slack 变量分配、HLF 等式展开、模型尺寸增长与 verifier 约束跟踪的完整链条；一次 uv run python examples/vertex_cover/runner.py --seed 42，则串起了 XQCP 建模、XQVM 三程序执行与 XQSA 求解采样的端到端流水线。掌握本例，即可将其中的 problem.vec() + apply_atleast 模式推广到一切"至少覆盖 k 个"形态的组合优化问题（集合覆盖、装箱、设备选择等），更多同类示例见 examples/README.md 与 Using the Examples。