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.

Biography:

蘇開樂，博士，國家杰出青年科學基金獲得者，浙江師范大學特聘教授，北京大學博士生導師。蘇開樂長期從事邏輯與難解問題的算法實現研究，在主流國際計算機期刊和會議等發表論文50多篇，包括CCF A類論文18 篇。曾獲國際計算機輯的主流會議AiML 2002最佳論文獎，SAT Challenge 2012獎。對最大可滿足性問題、最大團問題和可滿足性問題等三個難解問題，他與林翰、蔡少偉、羅川等合作分別提出了國際領先的經驗算法 Inc(W)MaxSATz, NuMVC 和 CCASat。