/logic24

CS402 Introduction to Logic for Computer Science, Spring 2024, KAIST

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 2024. 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.

1. Important Announcements

[February 24] Policy for handling late submissions.

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.

  1. <= One day late (by the midnight of the next day): -10
  2. <= Two days late: -20
  3. <= Three days late: -30
  4. <= Four days late: -40
  5. More than four days late: -100.

[February 24] Honour code.

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.

2. Logistics

2.1. Evaluation

  • Homework (20%). Programming assignment and report (30%). Final exam (50%).

2.2. Teaching Staffs

2.3. Place and Time

  • Place: 2445 in E3-1.
  • Time: 10:30 - 12:00 on Tuesday and Thursday.

2.4. Final Exam

  • Place: 2445 in E3-1.
  • Time: 10:00 - 11:45 on 13 June 2024 (Thursday).

2.5. Online Discussion

  • We will use KLMS.

3. Homework

Submit your solutions in KLMS. We will create submission folders for all the homework assignments in KLMS.

4. Tentative Plan

  • 02/27(Tue) - History of Mathematical Logic in Computer Science (Ch1).
  • 02/29(Thu) - Propositional Logic (Ch2).
  • 03/05(Tue) - Equivalences and Normal Forms (Ch3).
  • 03/07(Thu) - Equivalences and Normal Forms (Ch3).
  • 03/12(Tue) - Polynomial-Time Formula Classes (Ch4).
  • 03/14(Thu) - Polynomial-Time Formula Classes (Ch4).
  • 03/19(Tue) - Polynomial-Time Formula Classes (Ch4).
  • 03/21(Thu) - Resolution (Ch5).
  • 03/26(Tue) - Resolution (Ch5).
  • 03/28(Thu) - The DPLL Algorithm (Ch6).
  • 04/02(Tue) - The DPLL Algorithm (Ch6).
  • 04/04(Thu) - Lower Bounds for Resolution.
  • 04/09(Tue) - The Compactness Theorem (Ch7).
  • 04/11(Thu) - The Compactness Theorem (Ch7).
  • 04/16(Tue) [NO LECTURE] Midterm exam period.
  • 04/18(Thu) [NO LECTURE] Midterm exam period.
  • 04/23(Tue) - First-Order Logic (Ch8).
  • 04/25(Thu) - First-Order Logic (Ch8).
  • 04/30(Tue) - Normal Forms for First-Order Logic (Ch9).
  • 05/02(Thu) - Herbrand's Theorem and Ground Resolution (Ch10).
  • 05/07(Tue) - Herbrand's Theorem and Ground Resolution (Ch10).
  • 05/09(Thu) - Applications of Herbrand's Theorem (Ch11).
  • 05/14(Tue) - [NO LECTURE] Interview for KAIST graduate admission.
  • 05/16(Thu) - Applications of Herbrand's Theorem (Ch11).
  • 05/21(Tue) - Resolution for First-Order Logic (Ch12).
  • 05/23(Thu) - Compactness for First-Order Logic (Ch13).
  • 05/28(Tue) - Compactness for First-Order Logic (Ch13).
  • 05/30(Thu) - Decidable Theories (Ch14).
  • 06/04(Tue) - Decidable Theories (Ch14).
  • 06/06(Thu) - [NO LECTURE] National holiday.
  • 06/11(Tue) - [NO LECTURE] Final exam period.
  • 06/13(Thu) - Final exam.

5. Lecture Notes and Slides

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.

6. Programming Assignment and Report

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.

6.1. Evaluation

  • 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.

6.2. Deadline

  • 23:59 of the 20th of May in 2024 (Monday). Summit both your implementation and report in KLMS.

6.3. Programming Language to Use

  • Python 3.7-10.

6.4. Formats of Input and Output

6.5. Input Interface

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.

6.6. Output Interface

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

6.7. What to Submit in KLMS?

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.

6.8. Test Cases

The following webpages contain benchmark problems in DIMACS format:

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.

6.9. Final Remark

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.

7. Study Materials

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: