Recent Progresses in Local Search for SAT
Title: Recent Progresses in Local Search for SAT
Speaker:Kaile Su(Peking University)
Time:14:00-15:30, 8th April 2014
Venue: Lecture Room (334), 3rd Floor, Building #5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
Abstract:
In this talk, I will present some recent progresses in local search for SAT. In particular, I will introduce the main design and implementation of a world leading SAT solver CCASat, which currently one of the BEST local search solvers for SAT, placed first in Random SAT Track (one of three main tracks) in SAT Challenge 2102. A novel idea in CCASat is the strategy of configuration checking (CC), which is for the first time proposed for dealing with the cycling problem for MVC (Minimum Vertices Covering). The idea of CC is indeed leading a paradigm shift in local search for SAT. It becomes so influential that are used by near 40% (9 out of 24) solvers in the random SAT category of SAT Competition 2013, including a gold medal winner and a bronze medal winner.Bio:
Time:14:00-15:30, 8th April 2014
Venue: Lecture Room (334), 3rd Floor, Building #5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
Abstract:
In this talk, I will present some recent progresses in local search for SAT. In particular, I will introduce the main design and implementation of a world leading SAT solver CCASat, which currently one of the BEST local search solvers for SAT, placed first in Random SAT Track (one of three main tracks) in SAT Challenge 2102. A novel idea in CCASat is the strategy of configuration checking (CC), which is for the first time proposed for dealing with the cycling problem for MVC (Minimum Vertices Covering). The idea of CC is indeed leading a paradigm shift in local search for SAT. It becomes so influential that are used by near 40% (9 out of 24) solvers in the random SAT category of SAT Competition 2013, including a gold medal winner and a bronze medal winner.Bio:
苏开乐,博士,国家杰出青年科学基金获得者,浙江师范大学特聘教授,北京大学博士生导师。苏开乐长期从事逻辑与难解问题的算法实现研究,在主流国际计算机期刊和会议等发表论文50多篇,包括CCF A类论文18 篇。曾获国际计算机辑的主流会议AiML 2002最佳论文奖,SAT Challenge 2012奖。对最大可满足性问题、最大团问题和可满足性问题等三个难解问题,他与林翰、蔡少伟、罗川等合作分别提出了国际领先的经验算法 Inc(W)MaxSATz, NuMVC 和 CCASat。