The satisfiability problem (SAT) is arguably the most famous among difficult algorithmic problems. We will review the reasons of its wide popularity: there is $1M prize for proving that SAT is easy or hard; many problems in practice are stated easily in terms of SAT; SAT has numerous applications in various branches of Computer Science, there is an annual conference and competitions devoted to SAT; the longest section in the Art of Computer Programming by Donald Knuth is devoted to SAT.
We will show that is surprisingly easy to use SAT solvers in practice. To do this, we will implement together short programs for solving a few brain teasers. We will then give an overview of the main algorithmic techniques used by the state-of-the-art SAT solvers. We will also show how SAT is used in formal verification.
Speaker: Dr. Alexander Kulikov
Agenda:
00:00 - Introduction
00:41 - Satisfiability (SAT)
01:47 - Example
03:12 - The Art of Computer Programming
03:46 - Handbook of Satisfiability
04:45 - More Resources
05:24 - Mathematical Proofs and SAT
06:54 - This talk
07:34 - Solving Puzzles Using SAT Solvers
17:20 - Let’s Run It!
26:20 - Under the Hood: Algorithms Used in SAT Solvers
34:12 - Reductions: Every Hard Problem is SAT
49:44 - Formal Verification: Proving Unsatisfiability
51:10 - Conclusion
Presentation: drive.google.com/file/d/1dtxV...
#algorithm #SAT #computerscience