可满足性工具求解西瓜视频个性化题目的应用

       2018年的新风口是各大平台的答题赢奖金活动，其中今日头条旗下的西瓜视频算是用户量非常不错的一个平台。当时头条为了防止模拟器多开自动答题情况（还有组团答题），推出了个性化题。所谓的个性化题就是不同的用户看到的题目相同，当时每个人的选项不同或者选项位置不同，这样实现了一题多解的效果。
       对于令人棘手的个性化题目，我们使用已有的研究知识，可以用可满足性工具（SAT）求解正确答案，理论上可保持高正确率。首先拿一个题目分析吧（图片出自互联网）。


这一题问斯诺克比赛中哪个球是偶数分？
这里答案集合里面有7个选项，分别为红球、黄球、绿球、棕球、蓝球、粉球和黑球。
其中正确答案集合是黄球、棕球和粉球三个选项，因为黄球2分、棕色4分、粉球6分。
错误答案集合是红球、绿球、蓝球和黑球四个选项，因为红球1分、绿球3分、蓝球5分、黑球7分。
      现在假设我们不知道答案，我们来如何介绍求解出正确答案集合。(假设我们开5个模拟器进行采集题目数据，同时假设已知的5个手机答案集为：黑粉红、红蓝粉、蓝黑黄、棕绿蓝、红棕绿)。
Step1.首先题目出现之后进行截图，对答案区域进行图片分割和识别，得到备选答案集合。(感觉这一步挺复杂，可惜我不是搞图形图像的，需要朋友帮忙搞定这一块，我就不详细解释了)。后来听朋友说还可以读取每个选项的按钮的LABEL，这样获取选项文本更加方便。不管了这一步很重要，但是不是我处理的重点，略过...
Step2.对于每个截图必然会保持一种性质，那就是每一题只有一个正确选项和两个错误选项，不然不满足单选题的条件。当然，对于所有用户的题目，都要保持这个性质。
Step3.我们使用pairwise编码方式的合取范式和SAT求解器求解正确答案。按照已给的5个模拟器答案对颜色进行编码。（黑色对应数字1，粉色对应数字2，红色对应数字3，蓝色对应数字4，黄色对应数字5，棕色对应数字6，绿色对应数字7）。
编码正数代表为真，负数代表为假，即1代表为黑，-1代表不为黑，数字0当做结束符。黑色、粉色、红色有且只有一个为真的合取范式(CNF)可以用pairwise编码如下表示：
-1 -2 0
-1 -3 0
-2 -3 0
1 2 3 0
根据step2中的约束，5个剩下模拟器都要满足有且只有一个正确选项的性质。依次类推，所有的5个模拟器的答案对应可以表示如下(共7个变量，20条子句)：



Step4.通过SAT求解器进行求解，我选用的crytominisat工具，使用命令cryptominisat test.cnf运行，最后的到的结果如下：



可以发现2 5 6为真是test.cnf的唯一解，也就是说答案选择2 5 6所对应的粉色、黄色、和棕色。正确答案求得！
       SAT求解器可以在零点几秒内求解10万变量和100万字句的解，求解能力非常强。所以答题给出的10s限制至少在SAT求解上不会耗费太多时间。可能会在图片分割处理部分消耗多一点的时间。另外提一下UC答题助手，它是一款辅助答题的软件。UC答题助手的一大特点是:个性化题准确率极高且给出多个正确答案(这是其他答题助手做不到的)，但是普通的题目正确率就没有个性化题目高。感觉它可能用得是和SAT相似的原理，但是对于普通题目的话，因为要分析出题目和答案的语义最后综合给出正确答案，正确率当然没有只用看答案的个性化题目高。