IBM Ponder this 2018 March

r_64 posted @ 2018年4月08日 21:37 in 未分类 with tags IBM , 170 阅读

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月的题解(


登录 *


loading captcha image...
(输入验证码)
or Ctrl+Enter