4月8日：苏开乐博士讲Recent Progresses in Local Search for SAT
来源：会议讲座
作者：
时间：2014-04-09
SKLCS Seminar
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 is
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.
个人简历：苏开乐，博士，国家杰出青年科学基金获得者，浙江师范大学特聘教授，北京大学博士生导师。苏开乐长期从事逻辑与难解问题的算法实现研究，在主流 国际计算机期刊和会议等发表论文50多篇，包括CCF A类论文18 篇。曾获国际计算机辑的主流会议AiML 2002最佳论文奖，SAT Challenge 2012奖。对最大可满足性问题、最大团问题和可满足性问题等三个难解问题，他与林翰、蔡少伟、罗川等合作分别提出了国际领先的经验算法 Inc(W)MaxSATz, NuMVC 和 CCASat。
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 is
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.
个人简历：苏开乐，博士，国家杰出青年科学基金获得者，浙江师范大学特聘教授，北京大学博士生导师。苏开乐长期从事逻辑与难解问题的算法实现研究，在主流 国际计算机期刊和会议等发表论文50多篇，包括CCF A类论文18 篇。曾获国际计算机辑的主流会议AiML 2002最佳论文奖，SAT Challenge 2012奖。对最大可满足性问题、最大团问题和可满足性问题等三个难解问题，他与林翰、蔡少伟、罗川等合作分别提出了国际领先的经验算法 Inc(W)MaxSATz, NuMVC 和 CCASat。