| Title: | Current issues in Max-SAT solving |
| Date: |
September 11, 2008 (Thursday)
|
| Time: |
2:30 p.m. - 3:30 p.m.
|
| Venue: |
Room 121, 1/F, Ho Sin-hang Engineering Building,
The Chinese University of Hong Kong, Shatin, N.T. |
| Speaker: |
Prof. Javier Larrosa
Associate Professor Universitat Politecnica de Catalunya Barcelona, Spain |
SAT is the most famous NP-complete problem. Given a boolean formula in conjunctive normal form, the goal is to find an assignment that satisfies all its clauses. Max-SAT is the optimization version of SAT and the goal is to maximize the number of satisfied clauses. Many optimization problems arising in scheduling, bioinformatics, electronic markets, circuit design and many other domains can be naturally modelled as Max-SAT.
In the last 5 years Max-SAT solvers have evolved from the implementation of very naive ideas to modern and sophisticated pieces of software. The main reason of the breakthrough is the development of a true Max-SAT logic. In this talk I will present such a logic and review how it is exploited by modern Max-SAT solvers.
BIOGRAPHY:
Professor Larrosa obtained his Ph.D. in Computer Science at "Universitat Politecnica de Catalunya" (Barcelona, Spain) in 1998. After a post doctoral stay at the University of California, Irvine (USA) he returned to Barcelona where he currently carries out his research. His main topic of research is the development of algorithms for combinatorial optimization problems for deterministic graphical models. His work has been frequently published in prestigious journals and conference proceedings such as AIJ, JAIR, IJCAI, AAAI, ECAI, etc.
Enquiries: Miss Temmy So at tel 2609 8444
For more information, please refer to http://www.cse.cuhk.edu.hk/seminar