2012年6月19日,第15届可满足性测试的理论与应用国际会议(SAT 2012)在意大利举行。其间,揭晓了布尔可满足性问题求解挑战赛(SAT Challenge)的比赛结果。588888纽约国际官方网站软件研究所苏开乐教授指导的博士生蔡少伟等人设计的求解器CCASat在随机组给出的600道挑战性难题解出了其中的70.5%,夺得该组第一名。这是亚洲国家和地区在SAT会议主办的可满足性问题求解系列比赛中所取得的首个冠军。
随机组是这次比赛的三个主线组(main track)之一。在与同组来自哥伦比亚大学、布朗大学、乌尔姆大学、IBM华生研究中心等知名高校和研究机构的学者竞争中,CCASat遥遥领先于其他求解器,最终夺冠。随机组第二名和第三名分别解出了全部题目中的53.5%和51%,而去年比赛金牌得主Sparrow2011解出了50.5%的题目,位居第四。
引人瞩目的是,CCASat是基于单个自主创新的算法,而在其他两个主线组夺冠的求解器,都是基于已有求解器的组合。
布尔公式可满性判定问题(Boolean satisfiability)是计算机算法的基本问题,同时具有重要的应用价值。为了促进这个问题求解技术的研究与应用,一系列针对SAT求解器的评估与竞赛相继推出,其中SAT会议自2002年开始举办的比赛是国际上最具影响力的SAT比赛。
随机组冠军获奖证书