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 2023. 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.
The lecture on 1 June (Thursday) will be the last lecture of this course. In that lecture, I plan to cover quantified boolean formulas, polynomial hierarchy, and polynomial space, which are the topics requested by one student of the course. These topics covered in the lecture will not be assessed in the final exam.
[May 14] Homework4 is out.
The homework assignment 4 is out. Submit your solutions in KLMS by 6:00pm on 30 May 2023 (Tuesday).
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 30] Homework3 is out.
The homework assignment 3 is out. Submit your solutions in KLMS by 6:00pm on 12 May 2023 (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 2] Homework2 is out.
The homework assignment 2 is out. Submit your solutions in KLMS by 6:00pm on 14 April 2023 (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 2023 (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.
We will adopt the following scheme for handling late submissions for homework assignments, programming project, and the report of the programming project. 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. In homework submissions and reports, if a student quotes descriptions from certain sources (research papers or Wikipedia or other information from the web), the student will have to make explicit that these descriptions are quoted, and to mention the sources of those descriptions explicitly. Otherwise, the student's descriptions will be regarded as plagiarism, and his or her submission will be penalised harshly. The copy and paste of an automatically generated text from ChatGPT or other language models will also be regarded as plagiarism.
- Homework (20%). Programming assignment and report (30%). Final exam (50%).
- Lecturer: Prof Hongseok Yang (Email: hongseok00@gmail.com. Office hour: 4:00pm - 5:00pm on Thursday in the room 3403 in the E3-1 building.)
- TA: Taeyoung Kim (Email: taeyoungkim21@kaist.ac.kr. Office hour: 3:00pm - 4:00pm on Wednesday in the room 3415 in the E3-1 building.)
- TA: Sangho Lim (Email: lim.sang@kaist.ac.kr. Office hour: 3:00pm - 4:00pm on Monday in the room 3415 in the E3-1 building.)
- Place: 2443 in E3-1.
- Time: 10:30 - 12:00 on Tuesday and Thursday.
- Place: 2443 in E3-1.
- Time: 9:30 - 11:30 on 15 June 2023 (Thursday).
- 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 2023 (Friday).
- Homework2 - Deadline: 6:00pm on 14 April 2023 (Friday).
- Homework3 - Deadline: 6:00pm on 12 May 2023 (Friday).
- Homework4 - Deadline: 6:00pm on 30 May 2023 (Tuesday).
- 02/28(Tue) - History of Mathematical Logic in Computer Science (Ch1).
- 03/02(Thu) - Propositional Logic (Ch2).
- 03/07(Tue) - Equivalences and Normal Forms (Ch3).
- 03/09(Thu) - Equivalences and Normal Forms (Ch3).
- 03/14(Tue) - Polynomial-Time Formula Classes (Ch4).
- 03/16(Thu) - Polynomial-Time Formula Classes (Ch4).
- 03/21(Tue) - Polynomial-Time Formula Classes (Ch4).
- 03/23(Thu) - Resolution (Ch5).
- 03/28(Tue) - Resolution (Ch5).
- 03/30(Thu) - The DPLL Algorithm (Ch6).
- 04/04(Tue) - The DPLL Algorithm (Ch6).
- 04/06(Thu) - The Compactness Theorem (Ch7).
- 04/11(Tue) - The Compactness Theorem (Ch7).
- 04/13(Thu) - First-Order Logic (Ch8).
- 04/18(Tue) [NO LECTURE] Midterm exam period.
- 04/20(Thu) [NO LECTURE] Midterm exam period.
- 04/25(Tue) - First-Order Logic (Ch8).
- 04/27(Thu) - Normal Forms for First-Order Logic (Ch9).
- 05/02(Tue) - Herbrand's Theorem and Ground Resolution (Ch10).
- 05/04(Thu) - Herbrand's Theorem and Ground Resolution (Ch10).
- 05/09(Tue) - Applications of Herbrand's Theorem (Ch11).
- 05/11(Thu) - Applications of Herbrand's Theorem (Ch11).
- 05/16(Tue) - Resolution for First-Order Logic (Ch12).
- 05/18(Thu) - Compactness for First-Order Logic (Ch13).
- 05/23(Tue) - Compactness for First-Order Logic (Ch13).
- 05/25(Thu) - Decidable Theories (Ch14).
- 05/30(Tue) - Decidable Theories (Ch14).
- 06/01(Thu) - Quantified Boolean Formulas, Polynomial Hierarchy, and Polynomial Space.
- 06/06(Tue) - [NO LECTURE] National holiday.
- 06/08(Thu) - [NO LECTURE] All the course materials are covered.
- 06/13(Tue) - [NO LECTURE] Final exam period.
- 06/15(Thu) - Final exam.
The 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).
- Quantified Boolean Formulas, Polynomial Hierarchy, and Polynomial Space. (note).
Here are two tasks that you will have to do.
- Implement a SAT solver using the DPLL algorithm with clause learning, which we cover in the course, and also using optimisations for SAT solving that you devise or can find in the literature. Your implementation should not use any external python libraries directly related to SAT solving.
- Write a report that describes what you implemented, the design decision behind your implementation, and the rationale behind those decisions. The report should be at most 4 pages excluding the bibliography and figures. For instance, you can describe a list of possible optimisations for SAT solving, analyse the cons and pros of those optimisations, explain why you decide to choose only some of these optimisations, and justify your decision with experiments.
- Implementation (20%). Report (10%).
- The submitted implementation will be marked automatically using our script.
- The submitted report will be marked based on the level of originality and experimental or theoretical thoroughness in the analysis of the submitted implementation and its design decision, in a broad context of efficient SAT solving.
- 23:59 of the 22nd of May in 2023 (Monday). Summit both your implementation and report in KLMS.
- Python 3.7-10.
- 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:
- solvepy3.py
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 solvepy3.py file in your submission, and runs something like
- 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.
- A report on your implementation, its design decision, and the rationale behind or justification of the decision. The report must be written by a word processor and submitted in a pdf format. (Its file name doesn't matter.) The report should be at most 4 pages without including the bibliography and figures.
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. In the course webpage, we uploaded a zip file that contains some test cases we used before. To see the file, follow the below link:
If you implemented the DPLL algorithm in the lecture correctly, then your code will return a result in 1 minute for every cases in the above zip file (tested in i7 7700HQ). Note that these cases are just examples, not necessarily ones that we will use to test your code for marking; we will certainly try new test cases with various difficulty. Thus, even when your code finds a right answer to every provided case within 1 minute, it may perform badly on the real test cases, and fail to get good marks.
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. Finally, start this programming project as early as possible.
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. Knuth's book "The Art of Computer Programming, 4B" describes the techniques behind modern SAT solvers in detail. Finally, the webpage of the same course for the spring 2021 contains links to recorded lectures. Here is the link to the webpage: