This is a webpage of the course "CS402 Introduction to Logic for Computer Science", which is offered at the KAIST CS department in the spring of 2021. The webpage will contain links to course-related materials and announcements.
CS402 is a course on logic with emphasis on its use for computer science. Its goal is to expose students to the computational aspects of logic, in particular, key mathematical results and algorithms behind modern SAT solvers and theorem provers. The course involves a large amount of mathematics and theoretical computer science, in particular, computational complexity, verification, and programming languages. We assume that students are fluent in reading and proving mathematical theorems, and that they understand basic concepts from computability and complexity course, such as decidability, NP-completeness and reduction.
[May 18] Homework4 is out.
The homework assignment 4 is out. Submit your solutions in KLMS by 6:00pm on 2 June 2021 (Wednesday).
We remind the students that we adopt a very strict policy for handling dishonest behaviours. If a student is found to copy answers from peers or other sources in her or his submission for this homework assignment, he or she will get F.
[May 2] Homework3 is out.
The homework assignment 3 is out. Submit your solutions in KLMS by 6:00pm on 14 May 2021 (Friday).
We remind the students that we adopt a very strict policy for handling dishonest behaviours. If a student is found to copy answers from peers or other sources in her or his submission for this homework assignment, he or she will get F.
[April 5] Homework2 is out.
The homework assignment 2 is out. Submit your solutions in KLMS by 6:00pm on 16 April 2021 (Friday).
We remind the students that we adopt a very strict policy for handling dishonest behaviours. If a student is found to copy answers from peers or other sources in her or his submission for this homework assignment, he or she will get F.
[March 15] Homework1 is out.
The homework assignment 1 is out. Submit your solutions in KLMS by 6:00pm on 31 March 2021 (Wednesday).
We remind the students that we adopt a very strict policy for handling dishonest behaviours. If a student is found to copy answers from peers or other sources in her or his submission for this homework assignment, he or she will get F.
We will adopt the following scheme for handling late submissions for homework assignments and critical surveys. The scheme assumes that the total marks are 100.
- <= One day late (by the midnight of the next day): -10
- <= Two days late: -20
- <= Three days late: -30
- <= Four days late: -40
- More than four days late: -100.
We adopt a very strict policy for handling dishonest behaviours. If a student is found to copy answers from peers or other sources in her or his submission for any assignment, he or she will get F.
- Homework (40%). In-class oral tests (30%). Programming assignment and report (20%). One critical survey (10%).
- Lecturer: Prof Hongseok Yang (email: hongseok00@gmail.com, office hour: 6:00pm - 7:00pm Monday in ZOOM. You can find more information about it in KLMS.)
- TA: Hyoungjin Lim (email: lmkmkr@kaist.ac.kr, office hour: 5:00pm - 6:00pm Tuesday in ZOOM. Detailed information is announced in KLMS.)
- TA: Jungmin Park (email: qkrclrl701@kaist.ac.kr, office hour: 5:00pm - 6:00pm Thursday in ZOOM. Detailed information is announced in KLMS.)
- Place: ZOOM.
- Q&A sessions: 9:00am - 10:15am on Wednesday except for national holidays. Look at "5. Tentative Plan".
- In-class oral tests: Four sessions on chosen Mondays, with two scheduled during the mid-term and final exam periods. Look at "4. In-class Oral Tests".
- Recorded lectures: Online lectures available from Youtube. The schedule to watch these lectures and the links to them can be found in "5. Tentative Plan".
- We will use KLMS.
Submit your solutions in KLMS. We will create submission folders for all the homework assignments in KLMS.
- Homework1 - Deadline: 6:00pm on 31 March 2021 (Wednesday).
- Homework2 - Deadline: 6:00pm on 16 April 2021 (Friday).
- Homework3 - Deadline: 6:00pm on 14 May 2021 (Friday).
- Homework4 - Deadline: 6:00pm on 2 June 2021 (Wednesday).
We will run four in-class oral tests using ZOOM. During these tests, students will be randomly chosen and asked questions about topics covered by the course. We allocate 7.5% of the total marks of the course to each test. If a student does not attend one of the tests, she or he will get 0 for that test. The four tests will be scheduled on the following dates:
- 03/29(Mon) - In-class oral test at ZOOM from 9:00am - 10:15am.
- 04/19(Mon) (Midterm Exam Week) - In-class oral test at ZOOM from 9:00am - 10:30am.
- 05/17(Mon) - In-class oral test at ZOOM from 9:00am - 10:15am.
- 06/14(Mon) (Final Exam Week) - In-class oral test at ZOOM from 9:00am - 10:30am.
We adopt the following policy for these tests.
- We do attendance check at 9:30am, but if a student is called before this attendence check but is absent, she or he will get 0.
- In these tests, students will have to answer questions using their microphones. Also, they will have to turn on their cameras, at least when we do attendance check. Thus, students are strongly advised to ensure that their microphones and cameras work properly before these oral tests. If a student cannot use a microphone and a camera because of a special circumstance, she or he has to explain the circumstance to the teaching staffs before the test and arrange a way to participate in the test.
- During these tests, students do not have to answer in English, although questions will be asked in English.
- 03/01(Mon) - NO ZOOM MEETING. National Holiday.
- 03/03(Wed) - [ZOOM Lecture] History of Mathematical Logic in Computer Science (Ch1). (video).
- 03/03-03/10 - Propositional Logic (Ch2) and Equivalences and Normal Forms (Ch3).
- Watch video1 and video2.
- 03/10(Wed) - [Q&A] ZOOM Q&A session (whiteboard1, whiteboard2, whiteboard3, whiteboard4).
- 03/10-03/17 - Equivalences and Normal Forms (Ch3) and Polynomial-Time Formula Classes (Ch4).
- 03/17-03/24 - Polynomial-Time Formula Classes (Ch4).
- 03/24-03/31 - Polynomial-Time Formula Classes (Ch4) and Resolution (Ch5).
- 03/31-04/07 - Resolution (Ch5) and The DPLL Algorithm (Ch6).
- 04/07-04/14 - The DPLL Algorithm (Ch6) and The Compactness Theorem (Ch7).
- Watch video1 and video2.
- 04/14(Wed) - [Q&A] ZOOM Q&A session (whiteboard1, whiteboard2, whiteboard3).
- 04/14-04/21 - The Compactness Theorem (Ch7) and First-Order Logic (Ch8).
- Watch video1.
- 04/19(Mon) - [Oral Test] ZOOM in-class oral test on Ch5 - Ch7.
- 04/21(Wed) - NO ZOOM MEETING. Midterm Exam Period.
- 04/21-04/28 - First-Order Logic (Ch8) and Normal Forms for First-Order Logic (Ch9).
- 04/28-05/05 - Normal Forms for First-Order Logic (Ch9) and Herbrand's Theorem and Ground Resolution (Ch10).
- 05/05-05/12 - Herbrand's Theorem and Ground Resolution (Ch10) and Applications of Herbrand's Theorem (Ch11).
- 05/12-05/26 - Applications of Herbrand's Theorem (Ch11) and Resolution for First-Order Logic (Ch12).
- Watch video1 and video2.
- 05/17(Mon) - [Oral Test] ZOOM in-class oral test on Ch8 - Ch11. (whiteboard1, whiteboard2, whiteboard3, whiteboard4).
- 05/19(Wed) - NO ZOOM MEETING. National Holiday.
- 05/26(Wed) - [Q&A] ZOOM Q&A session.
- 05/26-06/02 - Resolution for First-Order Logic (Ch12) and Compactness for First-Order Logic (Ch13).
- 06/02-06/09 - Decidable Theories (Ch14).
- 06/14(Mon) - [Oral Test] ZOOM in-class oral test on Ch12 - Ch14.
- 06/16(Wed) - NO ZOOM MEETING. Final Exam Period.
The recorded online lectures are based on the following lecture notes and slides, which are minor variants of Prof Christoph Haase's version of Prof James Worrell's lecture notes and slides. The lecture notes are self-contained and explain key concepts clearly and briefly. Reading them is a recommended way to study the topics that we cover throughout the course.
- History of Mathematical Logic in Computer Science. (note, slides).
- Propositional Logic. (note, slides).
- Equivalences and Normal Forms. (note, slides).
- Polynomial-Time Formula Classes. (note, slides).
- Resolution. (note, slides).
- The DPLL Algorithm. (note, slides).
- The Compactness Theorem. (note, slides).
- First-Order Logic. (note, slides).
- Normal Forms for First-Order Logic. (note, slides).
- Herbrand's Theorem and Ground Resolution. (note, slides).
- Applications of Herbrand's Theorem. (note, slides).
- Resolution for First-Order Logic. (note, slides).
- Compactness for First-Order Logic. (note, slides).
- Decidable Theories. (note, slides).
One important part of this course is to study an assigned topic for oneself, and write a survey about it, which also contains critiques or original thoughts of the student. This assignment accounts for the 10% of the total marks of this course. In order to get full marks, a student has to show in his or her write-up that she or he has understood the topic well, carried out in-depth studies on the topic, and thought hard and originally about it. Our evaluation adopts the following criterion: the clarity of writing (20%), the level of understanding a topic and existing work about it (40%), and the demonstration of original thoughts and insights (40%). Here are the details of this assignment.
- Don't postpone this assignments until the last moment.
- A submission should be at most 3 pages not including bibliography.
- Topic: MaxSAT Solver.
- Deadline: 23:59 of the 3rd of May in 2021 (Monday). Summit in KLMS.
- Thinking about the following questions may help you.
- What is a MaxSAT solver?
- What are the most popular algorithms used for efficient modern MaxSAT solvers? Are the ideas from the DPLL algorithm and clause learning used in those solves? If so, why? If not, why not?
- What are the common applications of MaxSAT solvers? What would be a new interesting application for those solvers? For that application, do you expect that the algorithms for MaxSAT solvers or the interfaces to the solvers should be changed? If yes, how?
- How well do modern MaxSAT solvers perform? What are the most popular MaxSAT solvers?
- What do you think should be the next step in the work on MaxSAT solvers?
Implement a SAT solver using the DPLL algorithm with clause learning, which we cover in the course.
23:59 of the 24th of May in 2021 (Monday). Summit both your implementation and report in KLMS.
Python 2.7 and 3.x.
- Follow DIMACS input/output requirements. You can learn about these requirements at the following URL: http://www.satcompetition.org/2009/format-benchmarks2009.html. This is the format used in the SAT competition.
- Assume that the input is always in CNF format.
The main file of your solver should be named as follows:
solvepy2.py --- if you are using python 2.7 solvepy3.py --- if you are usin python 3.x
We plan to write a script that runs your solver with a cnf formula stored in a file (according to DIMACS format). The script searches for the solvepy2.py or solvepy3.py file in your submission, and runs something like
python2 solvepy2.py "testn.cnf" --- when solvepy2.py is found, python3 solvepy3.py "testn.cnf" --- when solvepy3.py is found.
Here "testn.cnf" is just an example name of a file containing a cnf formula in DIMACS format. Of course, different test cases will use different names.
The output should specify SATISFIABLE/UNSATISFIABLE using s and give a partial assignment using v. So, if your solver is run
python3 solvepy3.py "test1.cnf"
but "test1.cnf" is unsatisfiable and your solver finds this out, it should return
s UNSATISFIABLE
in the standard output. On the other hand, if your solver is run
python3 solvepy3.py "test2.cnf"
but "test2.cnf" is satisfiable and your solver finds a satisfying partial assignment (2, 5, -7) meaning that variables 2 and 5 have the value 1 and the variable 7 has the value -1 in the found partial assignment, then your solver should return
s SATISFIABLE v 2 5 -7 0
Here 0 indicates the end of the found partial assignment. The description of a found partial assignment can be across multiple lines. For instance, in the above case, the solver may return
s SATISFIABLE v 2 5 v -7 0
A zip file named "dpll.zip" containing two files:
- Source code of your implementation. Make sure that you follow the specifications described above. We plan to write a script that compiles and runs your code on some test cases automatically. Locate a solvepy*.py file on the root of the zip file.
- 1-2 page summary on what you did. The report must be written by a word processor and submitted in a pdf format.(its file name doesn't matter) The report should contain brief explanation of your algorithm and code.
The following webpages contain benchmark problems in DIMACS format: https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html and http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html. Those problems have a little bit different format described in the DIMACS format above; clause can be expressed on several lines, ill-formatted end lines. Therefore, you may need to modify your code or the problems to test them. However, the test cases for grading will strictly obey the DIMACS format above. I uploaded a zip file [https://github.com/hongseok-yang/logic21/blob/master/Others/Test_Case.zip] containing some test cases we used before. If you implemented the dpll algorithm in the lecture correctly, then your code will return a result in 1 minute (tested in i7 7700HQ). These file are just samples. We will try cases with various difficulty. Though your code returns the reuslt in 1 minute for the samples, it doesn't guarantee that your code will get a full score.
Make sure that your implementation handles corner cases correctly. There will be a timeout for each test case to check that you implemented the dpll algorithms in the lecture properly.
Reading the lecture notes is the recommended way to study the topics that we cover. Another useful book is Bradley and Manna's book "The Calculus of Computation", which also presents logic from the perspective of computation.