[pl-seminar] Talk today: On The Unreasonable Effectiveness of Boolean SAT Solvers

[Aws Albarghouthi <aws@xxxxxxxxxxx>]

Exciting talk today on at noon (4310) on why SAT solvers happen to
work in practice.

http://www.cs.wisc.edu/events/3402

======
On The Unreasonable Effectiveness of Boolean SAT Solvers

Monday, June 19, 2017 -
12:00pm to 1:00pm
CS 4310

Speaker Name:

Vijay Ganesh

Speaker Institution:

University of Waterloo

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. Second, I will talk about internals of CDCL SAT solvers,
and describe why they are particularly suited to solve industrial
instances.

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,
medals, and distinctions 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.



-- 
Aws