XQuad 工具链实战：用 xqcp DSL 端到端求解 Max-Cut 图划分问题
XQuad 工具链实战：用 xqcp DSL 端到端求解 Max-Cut 图划分问题
本文以 examples/maxcut/README.md 为骨架，完整讲解 XQuad 开源仓库中 Max-Cut 示例的 QUBO 建模、xqcp DSL 编码、三程序（encoder/verifier/decoder）流水线与求解器接入全流程。读者将掌握：如何用 problem.input() / define_model() / range() / model.linear[i].add() 等 DSL 接口把加权图分割问题写成可编译模型，如何用一行命令在 Python 参考 VM 与 Rust VM 之间切换执行，以及如何选择 CPU/GPU/QPU/Quip 等求解后端并读懂标准输出与 example-smoke 校验规则。
Max-Cut 问题与 QUBO 建模
Max-Cut（最大割）问题要求为一张加权图寻找一个 2-着色划分，使得横跨该划分的边的总权重最大。在 XQuad 中，这个问题被建模为一个 QUBO（二次无约束二值优化）问题：
- 输入：
num_nodes（int）与edges（Vec，边列表的扁平化表示，每条边以(i, j, w)三元组存储，共3*|E|个整数）。 - 模型：
n个二值变量，每个节点一个。x[v] ∈ {0, 1}表示节点v被划到割的哪一侧。 - 目标函数：对每条边
(i, j, w)，向模型累加-w*(x_i + x_j)的线性项和+2w*x_i*x_j的二次项。最小化该表达式等价于最小化-sum w*[x_i != x_j]，即最大化割的总权重。
该推导在 docs/book/src/concepts/quadratic-models.md 中也有完整的工作示例（"A Worked Example: Max-Cut"），其核心思想是把"两端不同色"的奖励转化为 0/1 变量的二次罚函数。
用到的 xqcp DSL 方法
Max-Cut 示例完整覆盖了 xqcp 约束编程 DSL 的主要建模原语（原文档 DSL methods used 一节）：
| DSL 方法 | 作用 |
|---|---|
problem.input() |
声明带类型的 calldata 输入（Types.Int / Types.Vec） |
problem.define_model() |
分配一个二值（Domain.BINARY）XQMX 模型 |
problem.stow() |
将中间计算结果绑定到命名寄存器 |
problem.range() |
发射 RANGE 循环 |
model.linear[i].add() |
在变量 i 上累加线性偏置 |
model.quadratic[i, j].add() |
在变量 i 与 j 之间累加二次耦合 |
problem.output() |
声明带类型的输出槽 |
problem.sample.getline() |
从采样位串中读取一行（即某个变量的取值） |
这些方法的底层实现在 xqcp/problem.py 中：Problem 容器把所有声明（输入、模型、循环、操作、输出）以有序的 Action 列表形式记录下来，compile() 再委托给 xqcp/compiler.py 发射三段独立的 .xqasm 程序源码。例如 model.linear<a href="https://link.gitcode.com/i/da47d656f240e716f1624227688b9500" target="_blank">i].add(-w) 会被记录为 add_linear action，最终编译为 ADDLINE r{model} 指令；model.quadratic[i, j].add(w * 2) 则编译为 ADDQUAD 指令，具体发射逻辑见 [compiler.py 中 _emit_add_linear 与 _emit_add_quadratic。
流水线概览：三程序架构
Max-Cut 的端到端流程（原文档 Pipeline overview 一节）分为六个阶段：
- CP（xqcp）：构建随机加权完全图，为每个节点声明二值变量，并逐边累加 QUBO 的线性/二次项。
- Assemble：通过
xquad.asm将.xqasm文本汇编为字节码。 - Encode：在选定的 XQVM 上运行 encoder，产出 XQMX 模型。
- Sample：求解器（SA/QPU/GPU）在模型上采样。
- Verify：verifier 检查采样值是否为二值，然后计算能量；本问题没有声明约束，因此 verifier 只需做域检查。
- Decode：decoder 从采样中提取 2-着色划分。
这正是 XQuad 的"三程序架构"（Three-Program Architecture）：一个优化问题在 XQuad 中是三个彼此独立、共享同一套指令集的程序，它们只通过 calldata 输入与输出槽通信，详见 docs/book/src/concepts/three-programs.md。xqcp 会从一个 Problem 定义一次性生成全部三个程序——problem.compile() 返回 CompiledPrograms(encoder, verifier, decoder)，即三段各自完整的 .xqasm 源码。
从 examples/maxcut/runner.py 的 run() 函数可以看到这段流水线的实际驱动方式，它依次做了四次调用：
# 1. encoder：calldata 为 [n, flat_edges]，1 个输出槽，产出 XQMX 模型
vm.set_calldata([n, flat])
vm.set_output_slots(1)
vm.run(programs.encoder)
model = vm.outputs()[0]
# 2. solver：完全在 VM 之外运行，产出 sample
solver = build_solver(solver_name, seed=seed)
sample = solver.solve(model).sample
# 3. verifier：calldata 为 [n, flat_edges, model, sample]，2 个输出槽，产出 (energy, valid)
vm.set_calldata([n, flat, model, sample])
vm.set_output_slots(2)
vm.run(programs.verifier)
energy, valid = vm.outputs()
# 4. decoder：calldata 为 [sample, n]，1 个输出槽，产出划分向量
vm.set_calldata([sample, n])
vm.set_output_slots(1)
vm.run(programs.decoder)
xquad.vm.VM 是一个统一封装，通过 VMBackend.RUST / VMBackend.PYTHON 分派到 Rust FFI VM（xqffi.vm）或纯 Python 参考 VM（xqvm_py.Executor），并在边界处统一转换 XQMX / Vec 等类型，见 xquad/vm.py。
运行方式与命令行参数
在仓库根目录执行以下命令即可运行 Max-Cut 示例（原文档 Usage 一节）：
uv run python examples/maxcut/runner.py --seed 42
uv run python examples/maxcut/runner.py --n 6 --seed 7 -o /tmp/mc.json
各命令行参数如下：
| Flag | 默认值 | 说明 |
|---|---|---|
--n |
5 |
完全图的节点数 |
--solver |
dwave-cpu |
求解器后端（见下节"选择求解器"） |
--interpreter |
python |
XQVM 后端：python 或 rust |
--seed |
42 |
随机种子 |
-o |
stdout | 将 JSON 结果写入文件；缺省输出到标准输出 |
所有 14 个示例 runner 都接受 --seed、--interpreter、--solver 与 -o/--output 这些通用参数，问题规模相关参数（如 --n）因示例而异，完整约定见 docs/book/src/examples/using-examples.md。
在 runner.py 的 main() 中可以看到 JSON 结果的结构：包含 _seed、_note、n、partition、cut_weight、energy 和 valid 字段，其中 _note: "canonical CI golden" 是 runner 自身的簿记字段，表示该次调用的用途，而非 CI 对输出做逐字节校验的承诺。
默认输出示例
以 --n 5 --seed 42 运行，输出形如（来自 docs/book/src/examples/maxcut.md 的规范示例）：
{
"_note": "canonical CI golden",
"_seed": 42,
"cut_weight": 354,
"energy": -354,
"n": 5,
"partition": [0, 1, 0, 0, 1],
"valid": 1
}
energy 是 cut_weight 的相反数，是因为 encoder 对每条横跨边最小化 -weight 以构成目标函数，与推导保持一致。valid: 1 在此处只确认每个采样值都在 {0, 1} 中——Max-Cut 未声明约束，这正是它的 verifier 检查的全部内容。partition 经 canonicalize_partition 归一化：由于 Max-Cut 在全局比特翻转（把所有节点两侧互换）下保持不变，将节点 0 固定到侧 0 可以在不改变割权重的前提下让两个解释器的输出稳定一致，具体实现见 runner.py 的 canonicalize_partition()。
选择求解器
求解器选择与安装 extras 对所有示例都是一致的（原文档 Choosing a solver 一节）：
| 名称 | 硬件 | 安装方式 |
|---|---|---|
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] |
GPU/QPU 驱动的先决条件参见仓库根 README.md 的 "GPU/QPU support" 小节，各求解器的参数调优快速入门参见 xqsa/README.md。
从 xqsa/solver.py 可以看出，所有后端共享同一个抽象基类 Solver 与统一的 SolverResult(sample, energy, timing, metadata) 返回结构：sample 是找到的最优赋值，energy 是用精确整数算术独立重算的哈密顿量（绝不直接采信后端返回值），metadata 的形状则因后端而异。runner 中的 build_solver(solver_name, seed=seed) 按名字选择后端，使调用方可以保持与具体后端无关。
注意：非默认求解器不会复现规范输出（因为 RNG/硬件不同）。example-smoke 始终运行 dwave-cpu；CUDA、Metal、QPU 等硬件后端只在检测到可用硬件时通过 scripts/example-smoke.py 的硬件子集（maxcut、tsp、knapsack，由 examples/manifest.yaml 中 hardware: true 标记）执行。
源码解读：build_problem 的核心建模循环
build_problem(n, seed) 是 runner 中建模的核心（examples/maxcut/runner.py）：
rng = random.Random(seed)
edges = [(i, j, rng.randint(1, 100)) for i in range(n) for j in range(i + 1, n)]
problem = Problem("MaxCut")
num_nodes = problem.input("num_nodes", type=Types.Int)
edges_in = problem.input("edges", type=Types.Vec)
problem.define_model(size=num_nodes, domain=Domain.BINARY)
edge_count = problem.stow("edge_count", edges_in.veclen() // 3)
with problem.range(0, edge_count) as e:
offset = e * 3
i = problem.stow("i", edges_in.get(offset))
j = problem.stow("j", edges_in.get(offset + 1))
w = problem.stow("w", edges_in.get(offset + 2))
problem.model.linear[i].add(-w)
problem.model.linear[j].add(-w)
problem.model.quadratic[i, j].add(w * 2)
partition = problem.output("partition", type=Types.Vec)
with problem.range(0, num_nodes) as node:
partition.append(problem.sample.getline(node))
return problem, edges
几个值得注意的细节：
- 边按
i < j顺序生成(i, j, w)三元组，作为扁平Vec（3*|E|个整数）喂给 VM；edges_in.veclen() // 3计算边数。 problem.stow("edge_count", ...)把表达式求值结果绑定到命名寄存器（底层是STOW r{reg}指令，见 compiler.py 中 stow action 的发射逻辑）。problem.range(0, edge_count)是上下文管理器，发射 RANGE 循环；循环内通过edges_in.get(offset)读取向量的第offset个元素（VecGetExpr，见 xqcp/symbols.py 的InputRef.get()）。- 输出段用
problem.sample.getline(node)逐个读取采样位串的行，把每个节点的划分结果追加进partition输出向量（GetLineExpr）。 define_model使用Domain.BINARY，对应编译器_ALLOCATOR映射中的BQMX分配指令（compiler.py），分配n个 0/1 变量。
编译器与 verifier 的源码级原理
problem.compile() 之所以能一次产出三个程序，是因为 xqcp/compiler.py 对同一个 action 流做了三种不同的发射：
- encoder：
_partition_program把 action 列表切分为输入段、模型分配段与主体段；_emit_body_actions以_ENCODER_MODE（_ENCODER_OPS表）发射目标与约束；所有add_linear/add_quadratic等模型改写 action 都会真正发射ADDLINE/ADDQUAD指令；输出段把模型寄存器通过OUTPUT r{model_reg}写到槽 0。 - verifier：
compile_verifier重放 encoder 的 action 流（输入、循环、stow、分支、向量构造），使它在每个约束点与 encoder 保持相同的寄存器/向量状态，但丢弃模型改写；每个约束被替换为对 solver 采样的检查；最后用ENERGY指令从模型与采样重新计算能量，输出(energy, valid)。Verifier 的 calldata 布局是"encoder 自身的输入 + model + sample"，可用problem.verifier_calldata()查询（xqcp/problem.py）。 - decoder：
_DecoderRegisters为 decoder 建立自己的寄存器映射（r0为 sample，r1为标量，其上为输出向量与循环变量），把录制表达式中的每个寄存器映射到 decoder 的寄存器文件。
compile() 生成三个程序后还会调用字节码 verifier（xqffi.verifier.verify_source）对每个程序做 Phase 1 + Phase 2 校验，以在编译期捕获代码生成缺陷；若 xqffi 未安装则静默跳过（xqcp/problem.py 的 _verify_compiled）。
Max-Cut 没有约束，因此它的 verifier 在 ; === Validity checks === 段的循环只做一件事：逐一确认每个采样值属于 {0, 1}（对 BINARY 域是 EQ 0 OR EQ 1，见 emit_domain_check）。但 ENERGY 重算是真实存在的独立校验——verifier 报告的 energy 是从模型与采样重新计算的，而不是从 solver 转述的。
标准输出与 example-smoke 校验
example-smoke 校验规则（原文档 Canonical output 一节）：
example-smoke 以 --seed 42 --solver dwave-cpu 验证两个解释器都能产出 valid == 1。该 smoke 测试是基于不变量的——它检查有效性，而非精确输出。
实现见 scripts/example-smoke.py：脚本对每个示例依次以 --seed 42 --interpreter python 与 --interpreter rust 运行，解析 JSON 并断言 valid == 1。为什么不做逐字节对齐？因为 dwave-cpu 背后的模拟退火对 BQM 构造顺序敏感：encoder、verifier、decoder 在每个解释器内部是确定性的（同样的字节码进、同样的输出出），但夹在中间的求解过程只由 seed 与 dwave-samplers 版本固定，不同版本可能对同一 seed 返回不同的有效采样，进而得到不同的割权重。因此 make example-smoke 检查的是 valid == 1 这一不变量，而不是 cut_weight、energy 或 partition 的一致性。脚本还会在检测到可用硬件时，对 manifest 中 hardware: true 的示例子集（含 maxcut）追加硬件求解器验证。
改编实战：从 Max-Cut 到固定端点的最小 s-t 割
把 Max-Cut 的 runner.py 复制改造是快速上手新问题建模的推荐路径。一个经典改编是把"任意划分"变成"指定两个端点必须分居两侧"的最小 s-t 割：docs/book/src/examples/using-examples.md 详细演示了这一过程——只需把目标项符号翻转（最大化变最小化），并给两个端点加上大小超过所有边权总和的锚定偏置：
with problem.range(0, edge_count) as e:
offset = e * 3
i = problem.stow("i", edges_in.get(offset))
j = problem.stow("j", edges_in.get(offset + 1))
w = problem.stow("w", edges_in.get(offset + 2))
problem.model.linear[i].add(w) # 符号翻转：最小化而非最大化
problem.model.linear[j].add(w)
problem.model.quadratic[i, j].add(w * -2)
# 将节点 0 固定到侧 0、节点 n-1 固定到侧 1；10_000 远超此图所有边权之和
problem.model.linear[0].add(10_000)
problem.model.linear[num_nodes - 1].add(-10_000)
同时必须从 main() 中移除 canonicalize_partition(partition) 调用——两个端点使两侧不再可互换，归一化会抹掉锚定添加的唯一事实。该文档还提醒了一个重要陷阱：valid 与 energy 单独都无法捕捉这类建模错误（割与其补割总是同权），需要直接检查你希望该次编辑保证的具体性质（如 partition[0] == 0 且 partition[-1] == 1），而不是只依赖聚合数字。
小结
examples/maxcut/ 是 XQuad 工具链中"一个文件贯穿每一层"的展示：从 xqcp DSL 建模、compile() 生成三程序、VM 双后端执行、xqsa 求解器采样，到 verifier 独立校验与 decoder 解码输出，全程无预写 .xqasm 文件、无 JSON 输入，只有 CP 进、解码划分出。掌握了这个示例的建模循环与运行方式，就可以把它作为模板，迁移到 TSP、Knapsack、Graph Coloring 等其余 13 个示例乃至你自己的 QUBO 问题中。