BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Boolean Satisfiability: From Theoretical Hardness to Practical Suc
 cess  
DTSTART:20110621T101500
DTSTAMP:20260506T180557Z
UID:aeace5c31b6b3de4714d476a1ad66e178da3b9bd6370f7aa342a00ba
CATEGORIES:Conferences - Seminars
DESCRIPTION:Prof. Sharad Malik\, Princeton University\nBoolean Satisfiabil
 ity (SAT) is the problem of checking if a propositional logic formula can 
 ever evaluate to true. This problem has long enjoyed a special status in c
 omputer science. On the theoretical side\, it was the first problem to be 
 classified as being NP-complete. On the practical side\, SAT manifests its
 elf in several important application domains such as the design and verifi
 cation of hardware and software systems\, as well as applications in artif
 icial intelligence. Thus\, there is strong motivation to develop practical
 ly useful SAT solvers. However\, the NP-completeness is cause for pessimis
 m\, since it seems unlikely that we will be able to scale the solutions to
  large practical instances. While attempts to develop practically useful S
 AT solvers have persisted for almost half a century\, for the longest time
  it was a largely academic exercise with little hope of seeing practical u
 se. Fortunately\, several relatively recent research developments have ena
 bled us to tackle instances with even millions of variables and constraint
 s - enabling SAT solvers to be effectively deployed in practical applicati
 ons. The problem is even (erroneously?) considered to be significantly tam
 ed. This talk will explore this transition from theoretical hardness to pr
 actical success\, including a description of the key ideas used in modern 
 SAT solvers and future research directions.  Prof. Malik's homepage
LOCATION:BC 01 https://plan.epfl.ch/?room==BC%2001
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR