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

       2018年的新风口是各大平台的答题赢奖金活动，其中今日头条旗下的西瓜视频算是用户量非常不错的一个平台。当时头条为了防止模拟器多开自动答题情况（还有组团答题），推出了个性化题。所谓的个性化题就是不同的用户看到的题目相同，当时每个人的选项不同或者选项位置不同，这样实现了一题多解的效果。

       对于令人棘手的个性化题目，我们使用已有的研究知识，可以用可满足性工具（SAT）求解正确答案，理论上可保持高正确率。首先拿一个题目分析吧（图片出自互联 ）。

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

可以发现2 5 6为真是test.cnf的唯一解，也就是说答案选择2 5 6所对应的粉色、黄色、和棕色。正确答案求得！

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