SMT & SAT (Satisfiability modulo theories & Boolean satisfiability problem)

几年前好像在哪里看到过说随机生成的SMT问题随着规模的增加变得几乎不可解决，而人写的问题，很多可以被优化过的求解器快速的地解决，可能是问题中隐含着一个更小更简单的问题。今天不知为何这个东西突然出现在思考其他问题的过程中，想，这可以类比为随机生成计算机程序。