XQuad 实战：用 HOBO 降次与 REDUCE 端到端求解 Max-3-SAT（QUBO 建模 + 六段流水线 + 双解释器验证）

原创2026-10-12 21:16:57657 阅读

XQuad 实战：用 HOBO 降次与 REDUCE 端到端求解 Max-3-SAT（QUBO 建模 + 六段流水线 + 双解释器验证）

Max-3-SAT 是 XQuad 示例集（examples/）中展示"高阶伪布尔目标（HOBO）如何降次为 QUBO"的典型问题：给定 N 个布尔变量上的 M 条三正文字子句，求满足子句数量最多的赋值。本文以 examples/max3sat/README.md 为骨架，结合 runner.py 的实现与 XQCP DSL、XQVM 规范中的 REDUCE 指令源码，完整讲解从问题建模、DSL 调用、指令级降次原理到"建模 → 汇编 → 编码 → 采样 → 验证 → 解码"六段流水线的每一步，读完你可以直接复现 uv run python examples/max3sat/runner.py --seed 42，也能把这个例子改造成自己的高阶优化问题。

问题定义与 QUBO 公式

输入：N 个二元变量，M 条由 3 个正文字组成的子句。每条子句 (i, j, k) 在三变量同时取 0 时被违反，因此问题目标为最小化所有子句的违反惩罚之和：

min  Σ over clauses of P*(1-x_i)(1-x_j)(1-x_k)

其中模型声明为 N 个二元变量 x_v ∈ {0, 1}（XQCP 中对应 Domain.BINARY），P 为每条未满足子句的惩罚强度。

展开乘积（丢弃常数项后）得到：

P*(-x_i - x_j - x_k + x_i*x_j + x_i*x_k + x_j*x_k - x_i*x_j*x_k)

即每个子句贡献 3 个线性项 -P*x_v、3 个二次项 +P*x_u*x_v，以及 1 个三次项 -P*x_i*x_j*x_k。三次项无法直接写入 QUBO 模型（XQMX 只存储线性与二次系数），必须通过 Rosenberg 降次（1975 年提出的经典 HOBO-to-QUBO 方法）消去。

三次项的降次：REDUCE(i, j) -> w

对每个子句引入一个辅助变量 w，用 REDUCE(i, j) -> w 把乘积 x_i*x_j 替换为 w，并施加 Rosenberg 强制约束：

P_AUX*(x_i*x_j - 2*x_i*w - 2*x_j*w + 3*w)

该惩罚在 w = x_i*x_j 时为 0，否则不小于 1，因此求解器总是倾向选择正确的 w（详见 spec/xqvm/HLF.md#L131-L155 的推导）。原三次项 -P*x_i*x_j*x_k 随之改写为二次项 -P*w*x_k，至此整个目标函数只剩线性与二次项，可交给任意 QUBO 求解器。

从公式上可以直观理解辅助变量的语义：w 必须同时满足 w = x_i*x_j（Rosenberg 强制）并携带原三次项的系数进入 -P*w*x_k，两者共同保证模型能量最低点对应的仍是"子句违反数最小"的原始问题。

XQCP DSL 中的 REDUCE：model.reduce()

在 runner.py 的 build_problem 中，降次被表达为一行 DSL 调用：

w = problem.model.reduce(ci, cj, _P_AUX)
problem.model.quadratic[w, ck].add(-_P_CLAUSE)

其中常量定义在文件头部：

_P_CLAUSE = 10   # 每条未满足子句的惩罚
_P_AUX = 50      # Rosenberg 辅助惩罚

P_AUX 必须超过三次项系数的幅值（_P_CLAUSE），否则求解器可能为了省惩罚而选择错误的 w。这里取 50 对 10，满足约束且留有余量。

reduce() 的返回值与链式用法

model.reduce(var_a, var_b, p_aux) 的签名与语义在 xqcp/symbols.py#L362-L370 中有完整定义：

分配一个辅助变量（寄存器槽位），记录 REDUCE action；
返回一个 RegLoad，持有辅助变量索引，可直接作为下标参与 model.quadratic[w, ck].add(...)；
返回表达式还可继续参与后续 reduce() 调用，实现链式降次——这正是高阶项（如四次项 x_i*x_j*x_k*x_l）通过两次连续 REDUCE 再 ADDQUAD 落地的方式（spec/xqvm/HLF.md#L155）。

在 build_problem 的循环体里，每个子句被完整编码为违反惩罚的展开：

with problem.range(0, num_clauses) as c:
    offset = problem.stow("offset", c * 3)
    ci = problem.stow("ci", clauses_in.get(offset))
    cj = problem.stow("cj", clauses_in.get(offset + 1))
    ck = problem.stow("ck", clauses_in.get(offset + 2))

    # 线性项：展开式中的 -P*x_v
    problem.model.linear[ci].add(-_P_CLAUSE)
    problem.model.linear[cj].add(-_P_CLAUSE)
    problem.model.linear[ck].add(-_P_CLAUSE)

    # 二次项：展开式中的 +P*x_u*x_v
    problem.model.quadratic[ci, cj].add(_P_CLAUSE)
    problem.model.quadratic[ci, ck].add(_P_CLAUSE)
    problem.model.quadratic[cj, ck].add(_P_CLAUSE)

    # 三次项 -P*x_i*x_j*x_k：REDUCE(i, j) -> w，然后加入 -P*w*x_k
    w = problem.model.reduce(ci, cj, _P_AUX)
    problem.model.quadratic[w, ck].add(-_P_CLAUSE)

注意 stow 与 range 的组合：子句以扁平 Vec 传入（每条子句 3 个变量下标连续存放），循环内通过 c * 3 计算偏移后逐条展开——这是 XQCP 处理"向量化输入 + 循环建模"的标准写法，XQCP 编译器负责把这些 DSL 调用录制为 action，并在 compile() 时一次性生成三段 .xqasm 程序（xqcp/README.md）。

指令级原理：REDUCE 在 XQVM 中的展开

HLF 规范中的展开公式

REDUCE 属于 XQVM 的"高层函数"（High-Level Functions）指令族。根据 spec/xqvm/HLF.md#L131-L155，给定 var_a、var_b、P_aux（栈上顺序为 [..., var_a, var_b, P_aux]，P_aux 在栈顶先弹出）：

在 model.size 处分配辅助变量 w（模型 size 增长 1）；
写入强制项：

quad[var_a, var_b]  += P_aux
quad[var_a, w]      += -2 * P_aux
quad[var_b, w]      += -2 * P_aux
linear[w]           += 3 * P_aux

把 w 的索引压栈，供后续链式使用。

也就是说一条 REDUCE 共写 3 个二次项 + 1 个线性项，并让模型 size 加 1。这正是 spec/xqvm/ISA.md#L291 对 REDUCE opcode 栈效果 [..., var_a, var_b, P_aux] -> [..., aux] 与"模型增长"语义的来源。

参考实现的落地

Python 参考 VM 在 xqvm_py/executor.py#L1546-L1558 的 _runner_REDUCE 中实现：先弹出 p_aux, var_b, var_a，计费（1 个变量、3 个二次项 + 1 个线性项的字节数、4 次系数写步数），再调用 expand_reduce(model, var_a, var_b, p_aux) 落表，最后把 w 压栈。计费行为与 spec/xqvm/METERING.md#L122 中 REDUCE = 4 * COEFF_WRITE_STEPS 的步数表一致。

汇编级佐证：conformance 向量

仓库的符合性向量直接给出了 REDUCE 的指令级展开结果，例如 conformance/vectors/constraints/reduce_basic/program.xqasm：

PUSH 3
BQMX r0        ; 3 变量二元模型
PUSH 0         ; var_a
PUSH 1         ; var_b
PUSH 1         ; p_aux（栈顶）
REDUCE r0      ; 分配 w=3，model.size 变为 4
               ; quad[0,1] += 1, quad[0,3] += -2, quad[1,3] += -2, linear[3] += 3

随后用 GETQUAD/GETLINE 逐项读回系数验证展开正确性。另一向量 reduce_chain 验证连续两次 REDUCE 的链式语义（w1=4 后 size 4→5 再分配 w2）。这些向量同时跑在 Rust 生产 VM（xqvm）与 Python 参考 VM（xqvm_py）上，任何实现分歧都会导致 CI 失败。

编译与验证中的约束

编译器发射：XQCP 在 xqcp/compiler.py#L443-L449 的 _emit_reduce 中依次求值 var_a、var_b、p_aux，发 REDUCE r{model} 后紧跟 STOW r{stow_reg} 保存辅助索引；
验证器不重放 REDUCE：验证器持有的是求解器返回的 sample，不能对模型二次执行 REDUCE（会突变模型），因此 XQCP 用影子计数器追踪辅助索引——从声明 size 播种，在每个 reduce 点读取计数器作为 w、STOW 到编码器自己的寄存器（使链式 reduce() 可解析）、然后递增（xqcp/compiler.py#L1231-L1253）；
顺序约束：影子计数器只在"没有其他操作先增长模型"时正确，因此编译期拒绝任何 atleast/atleastw/inequality/带 slack 的 equality 出现在 reduce() 之前或与之同块（xqcp/compiler.py#L892-L924，并有对应测试 xqcp/tests/test_xqcp.py#L1094）；
REDUCE 是结构变换而非领域约束：它记录在 _actions 中但刻意不进 _constraints，验证器仍会单独检查其辅助变量（spec/xqcp/CONSTRAINTS.md#L118-L127）。

端到端流水线：从问题到解码

Max-3-SAT 示例完整走通 XQuad 的六段流水线（docs/book/src/examples/max3sat.md 亦有同步文档）：

CP（xqcp）：build_problem 生成随机三正文字子句、声明二元变量，并通过 REDUCE 对三次违反项降次；
汇编：.xqasm 文本经 xquad.asm 转为字节码。注意本例中 problem.compile() 直接在内存生成三段 .xqasm 字符串，运行时再交给 VM，目录里没有落盘的 .xqasm 文件（docs/book/src/examples/using-examples.md）；
编码：在所选 XQVM（python 或 rust）上运行 encoder 程序，产出 XQMX 模型；
采样：xqsa 求解器（SA/QPU/GPU）在模型上求解，得到 sample；
验证：verifier 程序检查 sample 每个值属于 {0,1} 二元域、逐一核对每个 Rosenberg 辅助变量 w 是否等于其代表的乘积 x_i*x_j，再计算模型能量；
解码：decoder 程序从 sample 中提取变量赋值向量。

runner.py 的流水线实现

runner.py 的 run() 把上述流程组织为三次 VM.run() 调用，每次调用之间通过 calldata 与输出槽传递数据（VM 是 xquad/vm.py 提供的统一封装，支持 VMBackend.PYTHON / VMBackend.RUST 双后端）：

vm = VM(backend=backend)
vm.set_calldata([n, m, flat])      # 输入：变量数、子句数、扁平子句向量
vm.set_output_slots(1)
vm.run(programs.encoder)
model = vm.outputs()[0]            # 产出 XQMX 模型

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

vm = VM(backend=backend)
vm.set_calldata([n, m, flat, model, sample])   # 模型 + 样本一起交给验证器
vm.set_output_slots(2)
vm.run(programs.verifier)
energy, valid = vm.outputs()

vm = VM(backend=backend)
vm.set_calldata([sample, n])       # 只给样本和解码长度
vm.set_output_slots(1)
vm.run(programs.decoder)
assignment = ...                   # 变量赋值

最后 main() 组装 JSON 结果：包含 clauses（子句列表）、assignment（赋值）、satisfied（满足子句数，用 count_satisfied 独立核算 assignment[i] or assignment[j] or assignment[k]）、energy（模型能量）与 valid（验证标志）。satisfied 与 energy 是同一事实的两种表达：前者是问题语义（满足几条），后者是 QUBO 能量（含惩罚项），都来自同一个解码结果。

运行指南

在仓库根目录执行（需要 uv 管理的 Python 环境，仓库 pyproject.toml 已声明依赖）：

uv run python examples/max3sat/runner.py --seed 42
uv run python examples/max3sat/runner.py --n 8 --m 10 --interpreter rust

参数表（与 examples/max3sat/README.md 一致，另见 runner.py 中 argparse 的注释）：

Flag	Default	Description
`--n`	`6`	Boolean 变量个数
`--m`	`8`	子句条数
`--solver`	`dwave-cpu`	求解器后端（见下节）
`--interpreter`	`python`	XQVM 后端：`python` 或 `rust`
`--seed`	`42`	随机种子
`-o`	stdout	把 JSON 结果写入文件（否则输出到 stdout）

随机子句的生成在 main() 中完成：clauses = [tuple(sorted(rng.sample(range(args.n), 3))) for _ in range(args.m)]——每条子句从 0..n-1 中无放回抽 3 个变量并排序，保证 i < j < k 的规范形态。

--interpreter 只决定由哪个 VM 执行三段程序（Python 参考 VM xqvm_py 或经 xqffi 调用的 Rust VM），与求解器是两条独立轴。一个正确的模型在两个解释器上 valid 与 energy 恒等；当模型存在多个能量相同的等价最优解时，解码结果可能不同但同样正确——max3sat 正是这类存在平局（tie）的示例之一（docs/book/src/examples/using-examples.md）。

求解器选择

求解器接口由 xqsa 统一（xqsa/README.md），runner.py 通过 build_solver(name, seed=seed) 按名构造，调用方无需关心后端差异：

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 网络（远程矿工，环境变量配置）	`pip install xqsa[quip]`

GPU/QPU 驱动的先决条件（CUDA 12.x 驱动、Leap API token、QUIP_RPC_URL 等）见 README.md，各求解器的参数调优快速入门见 xqsa/README.md。

两个值得注意的事实：

非默认求解器不保证复现 canonical 输出：不同后端 RNG/硬件路径不同，同样的 seed 可能返回不同（但同样有效）的最优解；
example-smoke（即 make example-smoke）恒以 dwave-cpu 运行，覆盖全部示例 × 双解释器。

验证与一致性保障

verifier 程序对 REDUCE 辅助变量的检查逻辑（xqcp/compiler.py#L1231-L1253）做了三件事：读出影子计数器中的辅助索引、把索引 STOW 到编码器寄存器（保证链式 reduce 解析）、然后用 GETLINE 分别取 sample[w]、sample[var_a]、sample[var_b]，执行 MUL 后与 sample[w] 做 EQ 提交检查——即验证 w == x_a * x_b。除此之外还逐变量检查 sample 值是否落在模型声明域 {0, 1}（emit_domain_check 对 BINARY 域比较 0 与 1）。

Canonical output 与 smoke 测试

examples/max3sat/README.md 明确给出 canonical 输出约定：example-smoke 以 --seed 42 --solver dwave-cpu 验证两个解释器都产出 valid == 1。烟测是基于不变式的——只检查有效性（每个示例每个解释器 valid == 1），不要求字节级输出一致（scripts/example-smoke.py#L19-L27），因为 SA 对 BQM 构造顺序敏感，两条路径可能找到不同但同等有效的极值。

scripts/example-smoke.py 的主循环（scripts/example-smoke.py#L126-L161）对每个 examples/*/runner.py 依次跑 python 与 rust 两个解释器，检查 valid != 1 即判失败；若本机探测到硬件求解器（_hwprobe），还会对 manifest 中标注 hardware: true 的示例（maxcut、tsp、knapsack）加跑一轮硬件后端。所有示例在双解释器上通过后打印汇总。

XQuad 实战：用 HOBO 降次与 REDUCE 端到端求解 Max-3-SAT（QUBO 建模 + 六段流水线 + 双解释器验证）

XQuad 实战：用 HOBO 降次与 REDUCE 端到端求解 Max-3-SAT（QUBO 建模 + 六段流水线 + 双解释器验证）

问题定义与 QUBO 公式

三次项的降次：REDUCE(i, j) -> w

XQCP DSL 中的 REDUCE：model.reduce()

reduce() 的返回值与链式用法

指令级原理：REDUCE 在 XQVM 中的展开

HLF 规范中的展开公式

参考实现的落地

汇编级佐证：conformance 向量

编译与验证中的约束

端到端流水线：从问题到解码

runner.py 的流水线实现

运行指南

求解器选择

验证与一致性保障

Canonical output 与 smoke 测试

延伸阅读

热门文章

XQuad 实战：用 HOBO 降次与 REDUCE 端到端求解 Max-3-SAT（QUBO 建模 + 六段流水线 + 双解释器验证）

XQuad 实战：用 HOBO 降次与 REDUCE 端到端求解 Max-3-SAT（QUBO 建模 + 六段流水线 + 双解释器验证）

问题定义与 QUBO 公式

三次项的降次：REDUCE(i, j) -> w

XQCP DSL 中的 REDUCE：model.reduce()

reduce() 的返回值与链式用法

指令级原理：REDUCE 在 XQVM 中的展开

HLF 规范中的展开公式

参考实现的落地

汇编级佐证：conformance 向量

编译与验证中的约束

端到端流水线：从问题到解码

runner.py 的流水线实现

运行指南

求解器选择

验证与一致性保障

Canonical output 与 smoke 测试

延伸阅读

相关推荐

热门文章