Otomatik Akıl Yürütme: Sınanabilirlik

Bu kursta, çok çeşitli problemleri çözmek için sınanabilirlik (SAT/SMT) araçlarını nasıl uygulayacağınızı öğreneceksiniz. Uygulamaların mantığını kavramak için birkaç temel örnek verilmiştir: poster basımı için dikdörtgenleri sığdırma, çizelgeleme problemleri, bulmaca çözme ve program doğruluğu. Ayrıca, temel teori de sunulmaktadır: önermesel sınanabilirlik için temel bir yaklaşım olarak çözümleme (resolution), büyük formülleri ölçeklendirmek için CDCL çerçevesi ve doğrusal eşitsizliklerle başa çıkmak için simpleks yöntemi. Automated Reasoning: satisfiability kursunu takip etmenin zahmetsiz yolu sadece dersleri izlemek ve ilgili testleri çözmektir. Konu hakkında fikir edinmek için bu yöntem gayet iyi çalışabilir. Ancak, çok daha ilginç olan yaklaşım, bunu SAT/SMT'yi kendiniz birkaç problem üzerinde, örneğin onur ödevinde sunulan problemler üzerinde uygulamak için bir temel olarak kullanmaktır.