这是我第一次出题目，感谢师傅们的捧场。

这道题目的标题 FilpGame 其实就是一个 hint，通过搜索我们可以得知

FlipGame，又名点灯游戏，是一个十分有趣的智力游戏：有一行 N 行 N 列的灯，开始时全部是灭的，当你点击其中一盏灯时他的上下左右（若存在的话）状态全部改变，现在要求你以最少地步数，将全部的灯点亮。

转换逻辑

变换代码

这部分内容也可以通过代码中的关键变换语句看到

这个异或属于常见的一种位运算，而当它在这里的时候，起到的作用就是让 0 变成 1,1 变成 0。做到了翻转的功能，而1 << (15 - v12)实际上就是让坐标小的来作为数据中的高位，更加贴近一般思路。

最终目标

可以发现，当 data 数组的内容全部都是-1（0xFFFF）的时候，会输出 flag 的信息，所以我们的目标就是让 data 数组中的全部内容都变成 0xFFFF，从之前搜索到的信息，这个时候就可以猜测程序把灯的亮灭（10）都放在了一个一个 int16 的变量中（状态压缩），从而达到节省程序空间的目的。

解题思路

所以我们要解决的就是如何以最少的步数来让全部灯亮起来，并且需要记录操作。这需要一些算法的知识，很多师傅可能卡在了这里，希望各位师傅可以善用搜索来学习。

注意一下，这道题用 dfs 搜索是不可行的，因为 16*16 的规模比较大，用 dfs 的时间是不能够接受的。所以应该用爆破第一层，其余层按上一层的内容推出。

我这里贴一下我生成数据的代码，以及本题的代码。

解题程序

#define MAXN 16
#include <cstdio>
#include <cstring>
#include <algorithm>
#include <cstdlib>
#include <ctime>
#include <vector>
using namespace std;
char a[MAXN][MAXN], g[MAXN][MAXN];
int dx[] = { -1, 0, 0, 0, 1 }, dy[] = { 0, 0, -1, 1, 0 }, ans;
vector < pair<int, int> > PathVec;
vector < pair<int, int> > PathAns;
void filp(int y, int x)
{
    PathVec.push_back(make_pair(x, y));
    ans++;
    for (int i = 0; i < 5; i++)
    {
        int nx = x + dx[i], ny = y + dy[i];
        if (0 <= nx && nx < MAXN && 0 <= ny && ny < MAXN) g[ny][nx] ^= 1;
    }
}

int solve()
{
    int min_Ans = 1000;
    for (int i = 0; i < 1 << 16; i++)
    {
        PathVec.clear();
        ans = 0;
        memcpy(g, a, sizeof(a));
        for (int j = 0; j < MAXN; j++)
            if (i >> j & 1) filp(0, j);
        for (int j = 0; j < MAXN - 1; j++)
            for (int k = 0; k < MAXN; k++)
                if (g[j][k] == 0) filp(j + 1, k);
        for (int j = 0; j < MAXN; j++)
            if (g[MAXN - 1][j] == 0) 
                goto next;
        if (min_Ans > ans)
        {
            PathAns.assign(PathVec.begin(), PathVec.end());
            min_Ans = ans;
        }
    next:;
    }
    if (min_Ans == 1000) min_Ans = -1;
    return min_Ans;
}
char ToChar(int x)
{
    if (x >= 10) return x - 10 + 'A';
    return x + '0';
}
int main()
{
    unsigned short data[MAXN] = { 0xBEF5, 0x8BBC, 0xA0E9, 0x7310, 0xD910, 0xA3AD, 0xCCB6, 0x4DDE, 0x344C, 0x3BD6, 0x6711, 0x868F, 0x1C7A, 0x8425, 0x6B0D, 0x1B4C };
    while (true)
    {
        /*
        memset(data, 0, sizeof(data));
        time_t t;
        srand((unsigned)time(&t));
        for (int i = 0; i < MAXN; i++)
        {
            for (int j = 0; j < MAXN; j++)
                data[i] = data[i] << 1 | (rand() % 2);
        }
        */
        for (int i = 0; i < MAXN; i++)
            for (int j = 0; j < MAXN; j++)
                a[i][j] = data[i] >> (MAXN - 1 - j) & 1;
        int ans = solve();
        if (ans != -1) break;
    }
    for (auto x : PathAns)
    {
        printf("%c%c", ToChar(x.first), ToChar(x.second));
    }
    printf("\n");
    for (int i = 0; i < MAXN; i++)
    {
        printf("0x%X, ", data[i]);
    }

    return 0;
}

2021 年 8 月 14 添加 z3 解法

实际上这道题目还可以用 z3 来求解（使用 ZeroExt 可以让两个不同 btv 的 BitVec 相加）

from z3 import *

init_check = [
    [1, 0, 1, 1, 1, 1, 1, 0, 1, 1, 1, 1, 0, 1, 0, 1],
    [1, 0, 0, 0, 1, 0, 1, 1, 1, 0, 1, 1, 1, 1, 0, 0],
    [1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 1, 0, 0, 1],
    [0, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 0, 0, 0, 0],
    [1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0],
    [1, 0, 1, 0, 0, 0, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1],
    [1, 1, 0, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 1, 0],
    [0, 1, 0, 0, 1, 1, 0, 1, 1, 1, 0, 1, 1, 1, 1, 0],
    [0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 0, 0, 1, 1, 0, 0],
    [0, 0, 1, 1, 1, 0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0],
    [0, 1, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 0, 0, 0, 1],
    [1, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1],
    [0, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0],
    [1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 1, 0, 1],
    [0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 1],
    [0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0]
]

posx = [0, -1, 0, 1, 0]
posy = [0, 0, -1, 0, 1]

solver = Solver()

change = [[BitVec('change%x%x' % (i, j), 1) for j in range(16)] for i in range(16)]

for i in range(16):
    for j in range(16):
        for k in range(5):
            if 0 <= i + posx[k] < 16 and 0 <= j + posy[k] < 16:
                init_check[i][j] ^= (change[i + posx[k]][j + posy[k]])

for i in range(16):
    for j in range(16):
        solver.add(init_check[i][j] == 1)

sum = BitVec('sum', 16)
t = sum
solver.add(sum == 0)
for i in range(16):
    for j in range(16):
        t += ZeroExt(15, change[i][j])

solver.add(t <= 214 // 2)
solver.check()
ans = solver.model()

for i in range(16):
    for j in range(16):
        if ans[change[i][j]] == 1:
            print('%X%X' % (j, i), end='')

题目代码

#define MAXN 16
#define MAXS 0x6b
#include <cstdio>
unsigned short a[MAXN] = { 0xBEF5, 0x8BBC, 0xA0E9, 0x7310, 0xD910, 0xA3AD, 0xCCB6, 0x4DDE, 0x344C, 0x3BD6, 0x6711, 0x868F, 0x1C7A, 0x8425, 0x6B0D, 0x1B4C };
int posX = 0, posY = 0;
int dx[] = { -1, 0, 0, 0, 1 }, dy[] = { 0, 0, -1, 1, 0 };
int max_idx = -1;
inline bool check(int x, int y)
{
    return x >= 0 && x < MAXN && y >= 0 && y < MAXN;
}
inline int ToNum(char x)
{
    if ('0' <= x && x <= '9') return x - '0';
    if ('A' <= x && x <= 'Z') return x - 'A' + 10;
    return -1;
}
int main()
{
    printf("Input: ");
    char data[0x200];
    scanf_s("%s", data, 0x200);
    for (int i = 0; data[i]; i++)
    {
        if (i >= MAXS * 2) goto exit;
        if (i & 1) posY = ToNum(data[i]);
        else posX = ToNum(data[i]);
        if (!check(posX, posY)) goto exit;
        if (i & 1)
        {
            int idx = posY * MAXN + posX;
            if (max_idx >= idx) goto exit;
            max_idx = idx;
            for (int j = 0; j < 5; j++)
            {
                int nx = posX + dx[j], ny = posY + dy[j];
                if (check(nx, ny)) a[ny] ^= 1 << (MAXN - nx - 1);
            }
        }
    }
    for (int i = 0; i < MAXN; i++) if (a[i] != 0xFFFF) goto exit;
    printf("right, vnctf{MD5(%s)}\n", data);
    return 0;
exit:
    printf("wrong\n");
    return 0;
}