State Key Laboratory of Computer Science,
Institute of Software, Chinese Academy of Sciences
Email: email@example.com; firstname.lastname@example.org
Ph.D. in Computer Science, Peking University (2012)
Research interests: constraint satisfaction, optimization, heuristic search, randomized algorithms.
You can also visit my DBLP and Google Scholar Citations.
- I proposed the configuration checking (CC) strategy, which is a simple yet effective idea for local search and has been successfully applied to several combinatorial problems. The basic idea: for a solution component (such as a variable in SAT or a vertex in graph problems), if its configuration (some circumstance information) remains the same as the last time it changed assignment, then it is forbidden to change its assignment back. This is an interesting alternative of the Tabu method.
- CC is a general algorithmic idea, and one can get different CC strategies by defining configuration in different ways. A typical CC strategy for SAT is to forbid flipping a variable if since the last time it was flipped, none of its neighboring variables has been flipped.
- CC is a main idea in several winning solvers in SAT Competitions: CCASat (1st in random track of SAT Challenge 2012), CSHCrandMC (1st in random SAT+UNSAT track, SAT Competition 2013), Ncca+ (3rd in random SAT track, SAT Competition 2013), BalancedZ (2nd in random SAT track, SAT Competition 2014), CSCCSat (3rd in random SAT track, SAT Competition 2014), and CCAnr+gluecose (2nd in Hard Combinatorial SAT track, SAT Competition 2014).
Highlights on My Solvers
- 2014.7.18 [Award]: In SAT Competition 2014, CCAnr+glucose placed second in "sequential, Hard-combinatorial SAT" track, CSCCSat (jointly developed with Chuan Luo, who is the main author) placed third in both "sequential, random SAT" and "parallel, random SAT" tracks.
- 2014.7.18 [Award]: In MaxSAT Evaluation 2014, Dist placed first in 4 categories and CCLS placed first in another category in "incomplete solvers" track.
- 2013.7.12 [Award]: In MaxSAT Evaluation 2013, CCLS (jointly developed with Chuan Luo) placed first in 4 categories in "incomplete solvers" track.
- 2012.6.20 [Award]: In SAT Challenge 2012, CCASat placed first in Random track (1 of the 3 main tracks). Special thanks to Chuan Luo for discussions and implementation helps on a weighting technique, and Kaile Su for funding support.
- 2010.3.20 [New Record]: EWLS established a new record, i.e., finding a smaller vertex cover with 3902 vertices (or equivalently, an independent set of 98 vertices), for the frb100-40 challenging problem - details can be found here. I also developed EWCC and NuMVC solvers which show better performance and also achieve this record. Special thanks to my supervisor Kaile Su for funding support.
- First Prize in both Medium Sized categories (2vs2 and 4vs4), China RoboCup Soccer Robot Competition 2007
- First Prize in Undergraduate Category, Guangdong Provincial Software Design Competition 2007
- Academic Top 10 Students, School of EECS, Peking University, 2011
- Best Paper Award, School of EECS, Peking University (10 winners), 2011
- Innovation Award (3 winners in School of EECS, 104 winners in the whole Peking University), 2011
- CCASat is “Best Sequential Solver” in Random Track, SAT Challenge 2012
- Distinguished Doctoral Dissertation Award from Peking University, 2012