Het vervulbaarheidsprobleem The Satisfiability Problem

Het vervulbaarheidsprobleem (SAT) is misschien wel het bekendste van alle moeilijke algoritmische problemen. We bekijken waarom het zo populair is: er staat een prijs van $1M op het bewijs dat SAT makkelijk of moeilijk is; veel problemen uit de praktijk zijn eenvoudig in termen van SAT te formuleren; SAT heeft talloze toepassingen in allerlei takken van de informatica; er is een jaarlijkse conferentie met wedstrijden die aan SAT gewijd zijn; en het langste hoofdstuk in The Art of Computer Programming van Donald Knuth gaat over SAT. We laten zien dat het verrassend makkelijk is om SAT-solvers in de praktijk te gebruiken. Daarvoor schrijven we samen korte programma's die een paar breinbrekers oplossen. Daarna geven we een overzicht van de belangrijkste algoritmische technieken die de modernste SAT-solvers gebruiken. Ook laten we zien hoe SAT wordt gebruikt bij formele verificatie. Spreker: Dr. Alexander Kulikov Agenda: 00:00 - Introductie 00:41 - Vervulbaarheid (SAT) 01:47 - Voorbeeld 03:12 - The Art of Computer Programming 03:46 - Handbook of Satisfiability 04:45 - Meer bronnen 05:24 - Wiskundige bewijzen en SAT 06:54 - Deze talk 07:34 - Puzzels oplossen met SAT-solvers 17:20 - Laten we het draaien! 26:20 - Onder de motorkap: algoritmes in SAT-solvers 34:12 - Reducties: elk moeilijk probleem is SAT 49:44 - Formele verificatie: onvervulbaarheid bewijzen 51:10 - Conclusie Presentatie: https://drive.google.com/file/d/1dtxV9AJi1UF3iW6XPtBN2qPbKMkLiNOv/view #algorithm #SAT #computerscience

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: https://drive.google.com/file/d/1dtxV9AJi1UF3iW6XPtBN2qPbKMkLiNOv/view #algorithm #SAT #computerscience