多冲突检测不再只并行两条递归分支：合并循环里的每次一致性检查也提前算，2核实测平均加速1.21倍
核心概要
约束系统诊断需要一次找出多个最小冲突，MergeXplain 用一次分解返回多个冲突，但此前只把两条递归分支并行，消除跨半区冲突的合并循环仍串行。ParallelMergeXplain 在限定深度内并行递归分支，并把合并循环中每次 GetConflict 换成基于 QXGen 前瞻的推测并行版本。在2核机器上，全部非平凡配置的平均墙钟加速为1.21倍（标准差0.20），真实 SATLIB uf50-218 实例上 par full 在 p=2 时平均加速1.531倍，且返回结果与串行 MergeXplain 完全一致。
深度剖析
多冲突检测的并行化从只拆递归分支，扩展到合并循环内部：每次为消除跨半区冲突而调用的 GetConflict 本身也是一次 QuickXplain 求解，现在被替换成推测并行的 ParallelGetConflict。 此前的并行版本 PMXP 只把 FindConflicts 的两条独立递归调用放进两个线程，合并阶段那个反复调用 GetConflict 的循环保持严格串行。 在2核机器上，仅合并阶段推测（par spec，p=2、lmax=4）在真实 SATLIB uf50-218 实例上平均加速1.005倍（标准差0.052），基本持平；而仅分支并行（par branch）为1.513倍（标准差0.191），两层合并（par full，p=2）为1.531倍（标准差0.134）。
两层并行叠加后，在测试的每一种检查代价情形里都是最好或并列最好的平均表现，且返回的冲突集合与串行算法逐例相同。 串行 MergeXplain 是这条比较的基准，并行版本只改变计算发生的时间和位置，不改变计算内容。 75 次计时运行（15 个实例×5 个变体）返回的冲突集合与串行 MergeXplain 按 frozenset 集合意义完全相同，另有 80 组专门的正确性组合也全部一致；真实实例上返回的每个冲突都在事后被独立验证为可靠且最小。
并行收益取决于冲突结构：真实实例上串行 MergeXplain 总共只发出36至57次求解器调用，返回的冲突规模为2、4、5（候选共50个），留给合并阶段前瞻的空间很小。 合成基准此前无法显示这种数据依赖，因为其冲突基数和位置是受控植入的。 同一真实实例上，分支并行单独达到1.513倍，而合并阶段推测单独只有1.005倍，说明两层并行的相对收益随冲突规模变化。
启示与展望
演示范围限于2个物理核的 Linux 沙箱、18至50个需求的合成与真实实例，以及保守的冲突消除策略；合并阶段推测只施加在最外层 FindConflicts 调用上。参考实现与全部原始测量数据以 MIT 许可公开，便于替换一致性判定模块后复现。
作者指出2核硬件比此前评估 ParallelQuickXplain 和 FastDiagP 所用的8至16核机器少一个数量级，因此报告的绝对加速应视为保守值；自建的 CDCL 一致性判定器与独立 DPLL 求解器在85个实例上零不一致，但不是 Sat4j、MiniSat 这类工程化求解器。真实世界验证只用了 SATLIB uf50-218 一个外部公式和三个受控翻转场景，而非多样化的真实特征模型语料。