# 红石计算机：题解

## 解法比较

出题人解法把每一位的按位关系转换为 2-SAT 蕴含边，把所有位的图一次建好，用递归 Tarjan 求强连通分量，再在缩点图上选择互不矛盾的真假分量。某变量及其否定同属一个强连通分量时无解；否则缩点图的逆拓扑选择得到赋值。各位之间没有边，所以可以独立求解，建边规则及正确性见下文。

Codex（GPT-6）采用的实现逐位建图并复用空间，用显式遍历求分量。若有 $n$ 个数、$m$ 条关系、$k$ 位，两者时间均为 $O(k(n+m))$ .图的同时驻留空间由 $O(k(n+m))$ 降为 $O(n+m)$ ；但关系字符串和输出仍需保存，总空间上界仍为 $O(k(n+m))$ .收益是减少图对象并避免深递归，不应把局部工作区减少写成总空间降阶。

## 每一位独立求解

按位运算不会在不同二进制位之间传递信息，因此分别求解每一位的布尔约束，最后拼成各个数。设某一位上的两个变量为 $u,v$ ，目标位为 $c$ .

枚举 $(s,t)\in\{0,1\}^2$ .如果 $s\mathbin{\mathrm{op}}t\ne c$ ，这对取值被禁止，等价于子句

$$\neg(u=s)\lor\neg(v=t)$$

它产生两条蕴含边：$(u=s)\Rightarrow(v=1-t)$ 和 $(v=t)\Rightarrow(u=1-s)$ .这样统一处理三种运算，无需手写容易遗漏的分支表。$a=b$ 时仍按同一规则建边。

## 强连通分量与赋值

为每个变量建“值为零”和“值为一”两个节点。在蕴含图中求强连通分量。若某个变量的两个节点位于同一分量，它们互相强制，因而该位无解，整个问题也无解。

否则按分量的拓扑顺序赋值。参考程序使用 Kosaraju 算法：先在原图记录 DFS 完成顺序，再按其逆序遍历反图；得到的分量编号按原图拓扑顺序递增。选择编号较大的那个真假节点，即令 $x_i=1$ 当且仅当一节点的分量编号大于零节点。

## 正确性

每个禁止取值对恰由对应子句排除，所有合法取值对均保留，所以蕴含图与原布尔约束等价。两个互补节点强连通时不可能一致赋值。没有这种冲突时，上述拓扑赋值满足所有蕴含：若选中的字面量能推出未选中字面量，结合取反后的逆向蕴含，会与所选分量编号较大的规则矛盾。

各位求出的布尔解拼接后满足每一条按位关系；反之，任意一位无解都排除了完整二进制解。因此算法正确。

## 复杂度与评测

每位建立 $O(n+m)$ 个节点和边，求解需要 $O(n+m)$ 时间，总时间为 $O(k(n+m))$ .单个位的图占 $O(n+m)$ 空间，加上关系字符串和答案，总空间为 $O((n+m)k)$ .遍历使用显式栈。

`tests/checker.cpp` 接受输入、参考输出、选手输出三个路径参数。参考输出为 `No` 时核对无解标记；否则逐条计算选手给出的按位关系，接受任意合法赋值，并拒绝位数错误、非二进制字符或多余输出。空赋值单独按零个输出数处理。