今年计算机领域的一项国际比赛：民科战胜官科

   年终盘点，我今年最大的亮点是夺得SAT Race 2015的主类（main track)冠军,详见http://baldur.iti.kit.edu/sat-race-2015/sr15.pdf。SAT中文叫可满足性问题，是非常经典的NP问题，被喻为世界七大数学难题之一。该问题不仅有很强的理论价值，而且还有很强的实用价值。在我们现实生活中如密钥破解、故障诊断、软硬件验证等之类的问题都可以转变成SAT问题。由于其实用性，从2002年开始，国际上每年都要举行SAT比赛，其目的是要看谁能开发出世界上最快的SAT求解器。根据问题性质不同，SAT比赛又分为多个栏目，其中，竞争最为激烈的一个栏目是工业类或者说主类，被认为最有意义的一类，该类冠军一直由洋人把持，今年意外地落到我手中，感到非常自豪。

   不难发现，参加今年比赛的队伍中，绝大多数或多或少都得到了各种各样的经费的资助。我可能是比较另类的一个，没有得到任何经费的资助，靠自费研制SAT求解器夺冠。所以，我把自己定义为民科。但有可能有人不服，说我至少工资不是自给的。即使是这样，我也至少算半个民科吧。