Study of SAT-based constraint optimization problem solving and its parallel distributed processing

对约束满足和优化问题的SAT技术及其并行/分布式实现进行了研究，发表论文105篇，演讲67次。此外，还开发了世界领先的软件，包括基于SAT的CSP/COP求解器Sugar，该软件在2008年和2009年的CSP求解器竞赛中获得全球约束类别的冠军，CDCL类型的SAT求解器GlueMiniSat在2011年的SAT应用竞赛中获得UNSAT类别的冠军，以及部分Max-SAT求解器QMaxSAT，该软件在2010年和2011年的Max-SAT应用类别评估中获得冠军。

We conducted the research on SAT technologies for Constraint Satisfaction and Optimization Problems and their parallel/distributed implementations, and published 105 refereed papers and made 67 presentations. In addition, world's leading softwares were developed including a SAT-based CSP/COP solver Sugar which won at the 2008 and 2009 CSP Solver Competitions in global constraint categories, a CDCL type SAT solver GlueMiniSat which won at the 2011 SAT Competition in Applications UNSAT category, and a partial Max-SAT solver QMaxSAT which won at the 2010 and 2011 Max-SAT evaluation in Application category.