P1745 [CERC2016] Lost Logic

Gustav 正在阅读关于「2-可满足性」的问题，这是一个著名的问题，涉及为布尔变量分配真值以满足一系列「约束」——每个约束是涉及两个变量的简单逻辑公式。 我们使用 $n$ 个变量 $x_1, x_2, \cdots , x_n$，这些变量可以取值 $0$（假）和 $1$（真）。一个约束是形如 $a\to b$ 的公式，其中 $a$ 和 $b$ 都是可能被取反的变量。通常，$\to$ 表示逻辑蕴涵：$a \to b$ 仅在 $a$ 为 $1$ 且 $b$ 为 $0$ 时为 $0$。变量 $a$ 的取反表示为 $!a$。 给定变量的一个赋值，我们称约束在其结果为 $1$ 时被「满足」。Gustav 构建了一系列约束，并正确地得出有「恰好三种」不同的变量赋值可以满足所有约束。Gustav 写下了所有三种赋值，但不幸的是，他丢失了约束列表。 给定三个变量的 $n$ 个值的赋值，找出一个最多包含 $500$ 个约束的列表，使得这三个给定的赋值是唯一满足所有约束的赋值。

第一行包含一个整数 $n (2 \leq n \leq 50)$ —— 变量的数量。接下来三行，每行描述一个赋值。第 $k$ 行包含 $n$ 个用空格分隔的整数 $v_1^k,v_2^k,\cdots,v_n^k$，其中每个 $v_i^k$ 不是 $0$ 就是 $1$，表示第 $k$ 个赋值中变量 $x_i$ 的值。所有三个赋值将是不同的。

如果没有解，输出一行包含整数 $-1$。 否则，第一行应包含一个整数 $m$，其中 $1 \leq m \leq 500$ —— 你解决方案中的约束数量。接下来的 $m$ 行中的第 $k$ 行应包含第 $k$ 个约束。每个约束应根据以下规则构造一个字符串： - 一个「变量」是形如「$\texttt{x}i$」的字符串，其中 $i$ 是一个介于 $1$ 和 $n$ 之间的整数，且不含前导零。 - 一个「文字」是一个可能以「$\texttt{!}$」字符开头的变量组成的字符串。 - 一个「约束」是形如「$a\texttt{ -> }b$」的字符串，其中 $a$ 和 $b$ 都是文字。蕴涵符号由「减号」和「大于号」字符组成，且在蕴涵符号前后各有一个空格字符。

（由 ChatGPT 4o 翻译）