|
所在平台: Coursera |
课程主页: https://www.coursera.org/learn/automated-reasoning-sat
课程评论：没有评论
课程名称：自动推理：可满足性 课程概述：本课程将教您如何应用可满足性（SAT/SMT）工具来解决广泛的问题。课程包括多个基础示例，例如：为海报印刷适配矩形、调度问题、解谜游戏以及程序正确性等。此外，还将介绍相关的理论基础，包括用作命题可满足性的基本方法——归结法，以及如何通过CDCL框架来扩展解决大型公式和使用单纯形法来处理线性不等式。 课程的轻松学习方法是观看讲座并完成相应的测验。这样可以初步了解这个主题。更有趣的方式是将此课程用作基础，在多个问题上实际应用SAT/SMT工具，例如在荣誉作业中提出的问题。 课程大纲： 1. SAT/SMT基础与示例：该模块从头开始介绍可满足性（SAT）和理论模块的可满足性（SMT），并给出如何应用SAT的多个示例。 2. SMT应用：该模块展示了线性不等式的可满足性模块（SMT）的多个应用实例。 3. 基于CNF的SAT理论与算法：该模块描述了一种称为归结法的规则，如何用来判断合取范式（CNF）形式的命题公式是否不可满足。同时介绍DPLL算法及其与归结法的关系，最后展示当前SAT求解器如何实现和优化DPLL算法。 4. SAT/SMT的理论与算法：该模块分为两个部分。第一部分介绍将任意命题公式转换为CNF的过程，并说明Tseitin变换如何以线性大小对原公式进行转换。第二部分扩展SAT到SMT，特别是处理线性不等式，展示了线性优化中的单纯形法如何为这一任务服务，并详细解释了单纯形法的原理。 本课程适合对自动推理及应用感兴趣的学习者，无论是理论学习还是实际应用。
Name:SAT/SMT basics, SAT examples
Description:This module introduces SAT (satisfiability) and SMT (SAT modulo theories) from scratch, and gives a number of examples of how to apply SAT.
Name:SMT applications
Description:This module shows a number of applications of satisfiability modulo the theory of linear inequalities (SMT)
Name:Theory and algorithms for CNF-based SAT
Description:This module describes how a rule called Resolution serves to determine whether a propositional formula in conjunctive normal form (CNF) is unsatisfiable. It is shown how an approach called DPLL does the same job, and how it is related to resolution. Finally, it is shown how current SAT solvers essentially implement and optimize DPLL.
Name:Theory and algorithms for SAT/SMT
Description:This module consists of two parts. The first part is about transforming arbitrary propositional formulas to CNF, leading to the Tseitin transformation doing this job such that the size of the transformed formula is linear in the size of the original formula. The second part is about extending SAT to SMT, in particular to dealing with linear inequalities. It is shown how the Simplex method for linear optimization serves for this job; the Simplex method itself is explained in detail.
In this course you will learn how to apply satisfiability (SAT/SMT) tools to solve a wide range of problems. Several basic examples are given to get the flavor of the applications: fitting rectangles to be applied for printing posters, scheduling problems, solving puzzles, and program correctness. Also underlying theory is presented: resolution as a basic approach for propositional satisfiability, the CDCL framework to scale up for big formulas, and the simplex method to deal with linear inequallities. The light weight approach to following this course is just watching the lectures and do the corresponding quizzes. To get a flavor of the topic this may work out fine. However, the much more interesting approach is to use this as a basis to apply SAT/SMT yourself on several problems, for instance on the problems presented in the honor's assignment.
