已知异或结果时如何求解位向量S1…S3、C1…C3布尔方程组

以下方法按实现成本从低到高、适配场景从简单到复杂排序，可根据实际约束条件选择：

• 逐位拆分模2求解（无跨位约束首选）
  XOR本身是按位独立运算，只要S1_S3、C1C3之间没有跨位约束（比如不存在移位、进位、位拼接这类把不同比特位关联起来的规则），完全可以把整个问题拆成单个比特级的小方程组求解：

  1. 先把给出的十六进制参考值全部转成等长二进制串，按比特位对齐
  2. 对每一个比特位置，把涉及到的S_i、C_i对应位的变量列成模2加法（XOR等价于模2加）方程
  3. 对每个位的小方程组做高斯消元，直接得到该位所有变量的可行取值，最后逐位拼回完整位向量即可
     这个方法复杂度极低，哪怕位向量长度到上千位也能秒出结果，还能直接算出整个解空间的自由变量数量，方便枚举所有合法解。

• SMT/SAT求解器通用求解（有额外约束首选）
  如果S、C位向量本身带额外逻辑约束（比如来自电路逻辑、密码算法的关联规则，不是完全独立的自由变量），直接用位向量理论的SMT求解器是最省开发量的方案：

  1. 按实际位宽声明所有S1_S3、C1C3的位向量变量，比如32位值就声明对应位宽的BitVec类型
  2. 把所有异或匹配规则作为硬约束添加，例如S1 ^ S3 ^ C2 == 0xXXX这类等式
  3. 把S、C之间存在的其他逻辑约束（比如移位、截断、非线性运算关系）一并添加
  4. 调用求解器直接输出可满足解，需要枚举多组解的话，每次求出解后添加阻塞约束排除当前解，循环调用即可
     常用工具选Z3、Boolector都可以，Python环境下装个z3-solver库，十几行代码就能完成建模求解，不需要自己实现消元逻辑。

• 线性方程组专项优化（大位宽密码分析场景）
  如果这套方程组来自对称密码的线性层、线性反馈移位寄存器这类场景，位宽很大（几千到几万位）且方程是纯线性的，可以针对性做性能优化：

  1. 把所有方程整理成模2域下的标准线性形式M * x = v，M是0-1系数矩阵，x是所有S、C位展平后的变量向量，v是参考值转成的比特串
  2. 如果矩阵是稀疏的，用稀疏高斯消元、Wiedemann算法替代普通高斯消元，求解速度能提升几个数量级
  3. 如果夹杂少量非线性约束，可以先固定部分高概率取值的变量，把问题降维成纯线性方程组再求解。

• 暴力枚举（极低位宽场景凑合用）
  如果每个S、C的位宽在16位以内，总搜索空间不大，直接写脚本遍历取值做异或比对也能出结果，注意提前剪枝：比如已知S1 ^ S2 = 固定值，枚举S1之后可以直接算出S2，不需要重复枚举S2，能把搜索空间降低好几个量级。

避坑提示：如果异或表达式里存在移位、循环移位、跨位拼接/截断这类操作，不要用逐位拆分的方法，优先选SMT求解器方案，不容易出错。

参考异或结果对照表：

内容的提问来源于stack exchange，提问作者user84310