这学期授课全部由黄老师完成，解围老师担任助教。

黄老师上课很用心，也讲得很好，而且很积极与学生互动，经常阶段性地关心同学们有没有听懂，每次课都会留半小时左右的时间给同学们课后提问。

内容方面，前期主要是回顾和拓展了数理逻辑相关知识，后面会介绍该领域的一些基本知识和一些软件工具，印象最深的有SAT问题的求解、模型检测（NuSMV，LTL/CTL）（因为大作业做的是这两个hh）。知识方面个人觉得在理解上有一定难度，但是认真听老师讲课和认真独立完成作业对理解有很大帮助。虽然知识理解起来不容易，但是作业和小实验难度是OK的，个人觉得不属于简单，但是只要理解了就能很顺利地完成那种。

有9次平时作业（包括书面小作业和3次小实验好像）和一个大作业，大作业最后实现了DPLL算法来求解SAT和用NuSMV验证死锁（PPT上有说明），做两个是因为觉得这两个都属于工作量相对不大的那种。最后写得比较匆忙，平均每个花了两天时间，自我感觉不是很好，很多地方都没有完善，实验文档也写得很匆忙、不详细，以为有3.3就很感激了。

最后总评98，在科大本科最后一门知道成绩的课，也是在科大成绩最高的一门课，属于是喜出望外了！

黄老师，解老师，我的超人！

---------------------------------以下内容为2022秋季学期更新--------------------------------------------------------

第一次体会到简历match是什么感觉。将这门课的大作业搬到了简历上，多亏这个获得了一个实习offer，面试官聊得最多的就是SAT问题（中间还聊到了SMT问题但我当时没想起来），后面发现z3，SMT这些都用起来了。再次感谢黄老师！

12给黄老师，8分给解助教老师，平均一下。黄老师上课真的非常认真，每次讲完知识点都会说有没有讲清楚，如果有同学说没理解还会再讲一遍。最后大作业评价的问题也是黄老师一起解决的，真的是我在科大碰到的最负责的老师之一。黄老师的口头禅是“事实上”，但是这个词听多了还是容易没搞懂事实上是什么。

形式化方法这门课一定程度上是数理逻辑的后继，但是数理逻辑没学好影响不是很大（比如我）；此外内容上和人工智能的 logic agent 部分有一定重合，教授的时间也是重合的，所以一起上非常舒适。一个老师的课没听懂可以看另一个老师解释

顺便，我还是觉得我的工作被低估了（看到上面一个98的酸了，我做了没人实现过的 LALR+ROBDD constructor 也没有拿到这个成绩）

（桃子部分，不知道老师能不能看到）如果以后上课讲到 ROBDD 需要一个可视化的公式到 ROBDD 即时构建器，可以用我这个，到时候可以考虑出个 windows release；学到了这个部分想自己玩玩的同学有也可以来看看

这门课名字叫做形式化方法，我选这门课之前也不知道这门课是干啥的，只是因为这门课没有考试才选的，学完之后发现这门课真的不错。我觉得这门可以算作是对数理逻辑的扩展（这样说其实也不太准确，但是由于如果没学过这门课的内容，也不太好解释清楚，所以可以看作是数理逻辑的扩展）

这门课的内容挺难的，但是只要上课跟着老师的思路走，别玩手机，听懂是没有问题的，只要听懂了，课后的作业也比较简单。由于ppt是全英文的，而且内容比较难，所以不建议通过ppt异步学习。

老师上课氛围非常好，每次讲完一个点，都要问同学们听懂了没，如果没听懂可以马上问（可能因为今年是在3A的小教室，所以大家都比较积极地互动，如果改在3C大教室大家可能就会比较腼腆了）

给分也很不错，但是优秀率是有限的，所以老师的给分肯定没法让所有人满意，但是优秀率是给满了的，而且去年优秀率是直接超过了40%，只要认真做了，给分肯定不会差。

我觉得这门课唯一的问题就是ppt不太容易理解。就像我前面说的，ppt是全英文的，而且内容比较难，如果上课认真听了，看着还是比较轻松，但是如果上课摸鱼，自己看的时候会比较痛苦。幸好老师每节课都有录像，如果看不懂还可以自己看录像，建议以后也都把每节课录下来，不然自学真的比较痛苦。

这门课给我的收获还是很大的，让我对形式化的理论和应用有了初步的认知。课程的优点说得挺多了，我说些其他的感受：

• 大作业的评价方式似乎有些主观，可能无法让所有同学都满意。
• 上课总体来说是很不错的，不过有时候可能会过于纠结某些细节。
• 课程安排有待进一步的优化（前半部分节奏略慢）。

最后被卡绩了