今年美团杯的热身题是一道数回。

在出这道热身题的时候，蒜斜先选定了如下的模板，从而确定题目中一定有 MT 和 PKU 两个图案。

下一步就是要把模板中的所有 ? 都替换成 0-3 的数字，从而把模板变成一道数回题。在这个时候，非常重要的一点是需要保证唯一解（数回问题上解的定义可以见热身题）。

出题的时候，蒜斜发现要在这个模板上出一道难度合适且保证唯一解的数回题实在是太难了。于是他在出题的时候临时修改了一下这个模板，从而得到了这场比赛采用的热身题。

虽然最终热身题还是勉强出出来了，但是这种出题失败的挫败感让蒜斜很不舒服。因此，他希望你能帮助他完成原本的目标：根据原来的模板出一道保证唯一解的数回题。

Small Task: 你需要将模板中的所有 ? 分别替换成 0-3 中的整数，并保证对应的数回题具有唯一解。

Large Task: 你需要将模板中的所有 ? 分别替换成 1-3 中的整数，并保证对应的数回题具有唯一解。

输出格式

本题是一道提交答案，linkslither1.out 和 linkslither2.out 分别对应着 small task 和 large task。

对于每个部分，你需要提交一个 $12 \times 12$ 的仅包含空格以及数字 0-3 的矩阵，表示你出出来的数回题。

下面是一个样例的输出，但是它并没有办法在本题中得分，因为它存在多个不同的解。(在网页显示的时候中间空行里的空格被省略了，你在本地测试的时候需要手动加上)

0   0   000 
00 00  0   0
0 0 0  0   0
0 0 0  0000 
0 0 0  0    
0   0  0    

0  0   00000
0 0      0  
00   0 0 0  
0 0  0 0 0  
0  0 000 0  

测试工具

众所周知，求解数回是一个 NP-Complete 的问题。蒜斜并不想在年纪轻轻的时候就挑战图灵奖，于是他调用了 SAT-Solver 来判断你的解是否正确。

在比赛开始 15 分钟之后（即热身题停止计分后），本题的下发文件中将会包含本题的校验器 chk.py。校验器是用 python3 实现的，且依赖外部求解器 Z3。

要在本地运行校验器，你需要先通过指令 pip3 install z3-solver 或者 Z3 仓库中的安装指南在本地安装 Z3。然后，可以使用命令 python3 chk.py type.txt sol.txt 来运行求解器，其中：

1. type.txt 中包含一个 $0$ 或者 $1$ 的整数，分别表示 small task 和 large task。
2. sol.txt 中包含一个 $12 \times 12$ 的字符矩阵，表示你的答案。

如果你的解的格式没有任何问题，那么 chk.py 有如下三种可能的输出：

1. ok Correct! 表示你出的题目满足要求。同时 chk.py 还会打印出对应的唯一解。
2. There is no valid solution 表示你的出的题目没有任何合法解。
3. wa: There are multiple valid solutions 表示你的输出有不止一组合法解。这时，chk.py 会打印出其中两组不同的合法解。

因为 chk.py 的实现基于外部求解器，所以在理论上并不能保证 chk.py 对于所有输入都能很快地找到结果。因此，你需要保证 chk.py 可以在 $60$ 秒内求解出你出的题目。 我们相信这并不是一个太强的限制：在我们本地构造的所有测试上，chk.py 的求解时间均不超过 $2$ 秒。

下载

下发文件下载