Ajouter un attachement

Seuls les utilisateurs autorisés peuvent publier de nouveaux attachements.

Cette page (révision-288) a été modifiée pour la dernière fois le 06-avr.-2017 14:57 par hoyrup

Cette page a été créée le 20-juil.-2011 09:23 par cortier

Seuls les utilisateurs autorisés ont le droit de renommer des pages.

Seuls les utilisateurs authentifiés ont le droit de supprimer des pages.

Différences entre les versions et

En ligne 13, ajout de 17 lignes
!Thursday, April 20
%%(border: 1px solid #aaa; margin:1em 2.5%; padding:0.5em; background:#f9f9f9)
__On The Unreasonable Effectiveness of Boolean SAT Solvers.__ [Vijay Ganesh|https://ece.uwaterloo.ca/~vganesh/] (Univ. of Waterloo, Canada)
Modern conflict-driven clause-learning (CDCL) Boolean SAT solvers routinely solve very large industrial SAT instances in relatively short periods of time. This phenomenon has stumped both theoreticians and practitioners since Boolean satisfiability is an NP-complete problem widely believed to be intractable. It is clear that these solvers somehow exploit the structure of real-world instances. However, to-date there have been few results that precisely characterize this structure or shed any light on why these SAT solvers are so efficient.
In this talk, I will present results that provide a deeper empirical understanding of why CDCL SAT solvers are so efficient, which may eventually lead to a complexity-theoretic result. Our results can be divided into two parts. First, I will talk about structural parameters that can characterize industrial instances and shed light on why they are easier to solve even though they may contain millions of variables compared to small crafted instances with hundreds of variables. Second, I will talk about internals of CDCL SAT solvers, and describe why they are particularly suited to solve industrial instances.
Brief Bio:
Dr. Vijay Ganesh is an assistant professor at the University of Waterloo since 2012. Prior to that he was a research scientist at MIT, 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 reasoning 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, The Z3 string solver, MapleSAT, and MathCheck. He has also proved several decidability and complexity results relating to the SATisfiability problem for various mathematical theories. For his research, he has won over 21 awards including an ACM Test of Time Award at CCS 2016, two Google Faculty Research Awards in 2011 and 2013, and a Ten-Year Most Influential Paper Award at DATE 2008.
''14h00, room A006''
Version Date de modification Taille Auteur Modifications... Modifier la note
288 06-avr.-2017 14:57 123,784 ko hoyrup au précédent
287 07-mars-2017 11:58 121,481 ko hoyrup au précédent | au suivant
286 27-févr.-2017 09:55 121,481 ko hoyrup au précédent | au suivant
285 27-févr.-2017 09:54 121,479 ko hoyrup au précédent | au suivant
284 27-févr.-2017 09:54 121,478 ko hoyrup au précédent | au suivant
283 23-janv.-2017 13:51 120,348 ko hoyrup au précédent | au suivant
282 13-janv.-2017 10:55 120,344 ko hoyrup au précédent | au suivant
281 03-janv.-2017 11:01 119,012 ko hoyrup au précédent | au suivant
« Cette page (révision-288) a été modifiée pour la dernière fois le 06-avr.-2017 14:57 par hoyrup