课程主页: https://www.coursera.org/learn/automated-reasoning-sat
在Coursera平台上，有一门非常有趣的课程，名为《自动推理：可满足性》。这门课程的主要目标是让学员掌握如何应用可满足性（SAT/SMT）工具来解决广泛的问题。课程通过多个基本示例，带领学生体验可满足性的实际应用，包括适用于海报打印的矩形拟合、调度问题、解谜游戏，以及程序的正确性验证等。
这门课程的结构非常清晰，分为几个模块，使得学习者可以逐步深入理解可满足性的基础。第一部分介绍SAT和SMT的基本知识以及诸多具体应用。接下来的模块则深入探讨可满足性理论和算法，特别是关于CNF（合取范式）基础的内容，以及如何利用基本的解析规则和DPLL算法来判断命题公式的可满足性。这些概念的介绍不仅非常基础，而且与目前的SAT求解器的实现和优化紧密相关。
在学习的后半部分，课程对SAT和SMT的相关算法进行了详细讲解，首先讲述了如何将任意命题公式转换为CNF，并展示了Tseitin变换的线性大小特性，接着介绍了如何通过线性优化中的单纯形法扩展SAT到SMT，帮助学生更好地理解这些理论与实践的结合。
总的来说，这门课程不仅涵盖了可满足性问题的基本概念与应用，还深入探讨了背后的理论，适合对计算机科学、数学和逻辑有兴趣的学习者。通过这门课程，您将获得解决复杂问题的工具，更上层楼。
对于希望在人工智能或计算机科学领域有所成就的学生而言，这门课程提供了必不可少的知识基础，是值得参加的课程。
课程主页: https://www.coursera.org/learn/automated-reasoning-sat