Tuesday, November 29, 10:10 - 12:00.
Room 1509, on 15F, National Institute of Informatics,
2-1-2 Hitotsubashi, Chiyoda-ku, Tokyo 101-8430, Japan
Inoue laboratory will hold a seminar on the state-of-the-art SAT technologies
on Tuesday, November 29th.
In the seminar, talks are given by Prof. Laurent Simon from LRI, France
and Prof. Hidetomo Nabeshima from University of Yamanashi,
who have both developed winning SAT solvers of the SAT 2011 Competition.
Specifically, the SAT solver glucose developed by Prof. Simon won
the first prizes at the 2009 and 2011 SAT competitions, and
the SAT solver glueminisat developed by Prof. Nabeshima won
the first prize of the UNSAT class and got the second prize of the
UNSAT+SAT class (for which glucose won) at the 2011 SAT competition.
| 10:10 - 10:15 | Opening by Katsumi Inoue (NII) |
| 10:15 - 11:15 |
"Towards a New Era of SAT Solvers"
Speaker: Laurent Simon (LRI, University of Paris 11, France) Abstract: Since the first complete SAT solvers (DPLL-62, based on classical backtrack-search), major breakthroughs were observed in the practical - and theoretical - study of SAT. Nowadays, SAT solvers can be used in many critical systems, from very hard problems (Formal Verification, Biology, Cryptology) with potentially long runs, to more reactive applications (where a SAT solver can be called many times per second). In this talk, we will review the progresses made since the first breakthrough of 2001, with the introduction of CDCL solvers, called "modern solvers". We will show how the field is slowly moving from a "complete" version of Solvers to a more "uncomplete" one. We will end the talk by some open questions on the future of SAT Solvers. |
| 11:15 - 12:00 |
"GlueMiniSat 2.2.5: A Fast SAT Solver with An Aggressive Acquiring Strategy of Glue Clauses"
Speaker: Hidetomo Nabeshima (University of Yamanashi, Japan) Abstract: The state-of-the-art SAT solvers have many successful results in the research of software and hardware verification, planning, scheduling, constraint satisfaction and optimization, and so on. GlueMiniSat 2.2.5 is a SAT solver based on literal blocks distance (LBD) proposed by Audemard and Simon which is an evaluation criteria to predict learnt clauses quality in CDCL solvers. The effectiveness of LBD was shown in their SAT solver Glucose 1.0 at SAT 2009 competition. GlueMiniSat uses a slightly modified concept of LBD, called pseudo LBD, and has an aggressive restart strategy to promote the generation of good learnt clauses. GlueMiniSat shows good performance for unsatisfiable SAT instances. In the last SAT competition, GlueMiniSat took the first and second places in sequential SAT solvers for UNSAT and SAT+UNSAT classes of the application category, respectively. Moreover, GlueMiniSat won the second place for UNSAT class in the category including parallel SAT solvers. |