IBM Ponder this 2018 March

10个月没做IBM了。。

学一波SAT solver，以后讲不准会用到。

令$x_{ij}$表示灯的状态为$i$时，Bob回答$j$。那么：

• 对每个$i\in\{0,1\}^6$，Bob只能回答一种答案，这个可以用以下式子表示：
  • $x_{i0}\lor x_{i1}\lor\dots\lor x_{i4}$，即Bob至少回答一种
  • $\overline{x_{ij}}\lor\overline{x_{ik}}(j\ne k)$，即Bob至多回答一种
• 对每个元音$j$和每个灯的状态$i$，Alice一定能通过只调节一个灯，使得Bob的回答是$j$。如下表示：
  • $x_{ij}\lor x_{k_1 j}\lor x_{k_2 j}\lor\dots$，其中$k_1,k_2,\dots$为$i$改变一个灯可能的状态。

代码：

import pycosat
p = 5
def m(i, j) :
	return i * p + j + 1

cnf = []
n = 6
N = 2 ** n
for i in range(N) :
	cnf += [[m(i, j) for j in range(p)]]
	for j in range(p) :
		for k in range(j + 1, p) :
			cnf += [[-m(i, j), -m(i, k)]]
	for j in range(p) :
		cnf += [([m(i, j)] + [m(i ^ (2**k), j) for k in range(n)])]

ans = pycosat.solve(cnf)
print ans
a = ""
for i in range(N) :
	for j in range(p) :
		if ans[m(i, j) - 1] > 0 :
			a += "AEIOU"[j]
print a

(ps. 只用了$40\texttt{s}$就跑出来了)

官方solution用的是mixed integer programming。有一个叫做CPLEX的包，改天学一学。

看上去，在涉及到整数(不仅仅是布尔值)的时候，MIP比SAT用起来要更方便。

另外吐槽一下，IBM April 2018的题目是真的水；还有就是官方鸽到4月8号才放3月的题解（