Speaker:Ìý, Electrical and ComputerÌýEngineering, University of À¶Ý®ÊÓƵ
Abstract:ÌýOver the last two decades, softwareÌýengineering has witnessed a silent revolution in the form ofÌýBoolean SAT solvers. These solvers are now integral to many analysis,Ìýsynthesis, verification, and testing approaches. This is largelyÌýdue to a dramatic improvement in the scalability of theseÌýsolvers vis-a-vis large real-world formulas. What is surprising is that theÌýBoolean satisfiability problem is NP-complete, believed to beÌýintractable in general, and yet these solvers easily solveÌýinstances containing millions of variables and clauses in them. How canÌýthat be?
In my talk, I will addressÌýthis question of why SAT solvers are so efficient through the lensÌýof machine learning as well as ideas from (parameterized) proofÌýcomplexity. I will argue that SAT solvers are best viewed as proof systems,Ìýcomposed of prediction engines that optimize some metricÌýcorrelated with solver running time. These prediction engines can beÌýbuilt using ML techniques, whose aim is to structure solver proofs inÌýan optimal way. Thus, two major paradigms of AI, namely machineÌýlearning and logical deduction, are brought together in a principledÌýway to design efficient SAT solvers. A result of my research is theÌýMapleSAT solver, that has been the winner of several recentÌýinternational SAT competitions, and is now widely used in industry and academia.
Speaker Bio:ÌýDr. Vijay Ganesh is anÌýassociate professor at the University of À¶Ý®ÊÓƵ. Prior to joiningÌýÀ¶Ý®ÊÓƵ in 2012, he was a research scientist at MITÌý(2007-2012) and completed his PhD in computer science from Stanford University inÌý2007. Vijay's primary area of research is the theory and practice ofÌýautomated mathematical reasoning algorithms aimed at softwareÌýengineering, formal methods, security, and mathematics. In thisÌýcontext, he has led the development of many SAT/SMT solvers, mostÌýnotably, STP, Z3 string, MapleSAT, and MathCheck. He has alsoÌýproved several decidability and complexity results in the context ofÌýfirst-order theories. He has won over 25 awards, honors, and medalsÌýto-date for his research, including an ACM Impact Award at ISSTAÌý2019, ACM Test of Time Award at CCS 2016, an Ontario Early ResearcherÌýAward 2016, two Google Faculty Research Awards in 2011 and 2013, and aÌýTen-Year Most Influential Paper citation at DATE 2008.
Vijay is a faculty affiliate of À¶Ý®ÊÓƵ's Computational Mathematics centre.
Zoom Link:Ìý
Meeting ID: 973 5811 2053
Passcode: 673203
(you will be able to join the meeting from 3:20pm)