logic21

KO | EN

gitlite — search

#python #react #ai #typescript #android #rust #linux #macos #awesome #kubernetes #awesome-list #vue #mcp #openai

(★ 22)

No description available.

logic21 Latest Version Download

Download Latest Version (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# CS402 Introduction to Logic for Computer Science, Spring 2021, 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 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.

## 1. Important Announcements

#### [May 18] [Homework4](https://github.com/hongseok-yang/logic21/blob/master/Homework/sheet4.pdf) 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](https://github.com/hongseok-yang/logic21/blob/master/Homework/sheet3.pdf) is out.

The homework assignment 3 is out. Submit your solutions in KLMS by 6:00pm on 14 May 2021 (Friday).

#### [April 5] [Homework2](https://github.com/hongseok-yang/logic21/blob/master/Homework/sheet2.pdf) is out.

The homework assignment 2 is out. Submit your solutions in KLMS by 6:00pm on 16 April 2021 (Friday).

#### [March 15] [Homework1](https://github.com/hongseok-yang/logic21/blob/master/Homework/sheet1.pdf) is out.

The homework assignment 1 is out. Submit your solutions in KLMS by 6:00pm on 31 March 2021 (Wednesday).

#### [February 22] Policy for handling late submissions.

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.

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 22] 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.

## 2. Logistics

#### Evaluation

* Homework (40%). In-class oral tests (30%). Programming assignment and report (20%). One critical survey (10%).

#### Teaching Staffs

* Lecturer: [Prof Hongseok Yang](https://cs.kaist.ac.kr/people/view?idx=552&kind=faculty&menu=160) (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 and Time

* 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".

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

* [Homework1](https://github.com/hongseok-yang/logic21/blob/master/Homework/sheet1.pdf) - Deadline: 6:00pm on 31 March 2021 (Wednesday).
* [Homework2](https://github.com/hongseok-yang/logic21/blob/master/Homework/sheet2.pdf) - Deadline: 6:00pm on 16 April 2021 (Friday).
* [Homework3](https://github.com/hongseok-yang/logic21/blob/master/Homework/sheet3.pdf) - Deadline: 6:00pm on 14 May 2021 (Friday).
* [Homework4](https://github.com/hongseok-yang/logic21/blob/master/Homework/sheet4.pdf) - Deadline: 6:00pm on 2 June 2021 (Wednesday).

## 4. In-class Oral Tests

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.

1. 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.
2. 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.
3. During these tests, students do not have to answer in English, although questions will be asked in English.

## 5. Tentative Plan

* 03/01(Mon) - __**NO ZOOM MEETING.**__ National Holiday.
* 03/03(Wed) - __**[ZOOM Lecture]**__ History of Mathematical Logic in Computer Science (Ch1). ([video](https://youtu.be/DCTZ4bYxiA0)).
* 03/03-03/10 - Propositional Logic (Ch2) and Equivalences and Normal Forms (Ch3). 
  * Watch [video1](https://youtu.be/nN1m27usYbA) and [video2](https://youtu.be/eLSouMjDcRc).
  * 03/10(Wed) - __**[Q&A]**__ ZOOM Q&A session ([whiteboard1](https://github.com/hongseok-yang/logic21/blob/master/Others/21Mar10-QABoard1.png), [whiteboard2](https://github.com/hongseok-yang/logic21/blob/master/Others/21Mar10-QABoard2.png), [whiteboard3](https://github.com/hongseok-yang/logic21/blob/master/Others/21Mar10-QABoard3.png), [whiteboard4](https://github.com/hongseok-yang/logic21/blob/master/Others/21Mar10-QABoard4.png)).
* 03/10-03/17 - Equivalences and Normal Forms (Ch3) and Polynomial-Time Formula Classes (Ch4). 
  * Watch [video1](https://youtu.be/3y7EvaWR_RA) and [video2](https://youtu.be/hhlyh4EjmRc).
  * 03/17(Wed) - __**[Q&A]**__ ZOOM Q&A session.
* 03/17-03/24 - Polynomial-Time Formula Classes (Ch4). 
  * Watch [video1](https://youtu.be/ZuNTTZAseUg) and [video2](https://youtu.be/ZULtqGkJBNk).
  * 03/24(Wed) - __**[Q&A]**__ ZOOM Q&A session.
* 03/24-03/31 - Polynomial-Time Formula Classes (Ch4) and Resolution (Ch5). 
  * Watch [video1](https://youtu.be/Ta0Orl0EK6I) and [video2](https://youtu.be/dZ6amsVpIS4).
  * 03/29(Mon) - __**[Oral Test]**__ ZOOM in-class oral test on Ch1 - Ch4.
  * 03/31(Wed) - __**[Q&A]**__ ZOOM Q&A session.
* 03/31-04/07 - Resolution (Ch5) and The DPLL Algorithm (Ch6). 
  * Watch [video1](https://youtu.be/EkXhCXVRnh8) and [video2](https://youtu.be/1LXIcu-89_Q).
  * 04/07(Wed) - __**[Q&A]**__ ZOOM Q&A session.
* 04/07-04/14 - The DPLL Algorithm (Ch6) and The Compactness Theorem (Ch7). 
  * Watch [video1](https://youtu.be/G-BJ9GgGYNA) and [video2](https://youtu.be/Jqj6_yEv_Nw).
  * 04/14(Wed) - __**[Q&A]**__ ZOOM Q&A session ([whiteboard1](https://github.com/hongseok-yang/logic21/blob/master/Others/21Apr14-QABoard1.png), [whiteboard2](https://github.com/hongseok-yang/logic21/blob/master/Others/21Apr14-QABoard2.png), [whiteboard3](https://github.com/hongseok-yang/logic21/blob/master/Others/21Apr14-QABoard3.png)).
* 04/14-04/21 - The Compactness Theorem (Ch7) and First-Order Logic (Ch8). 
  * Watch [video1](https://youtu.be/J5Xn2wVRAeo).
  * 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). 
  * Watch [video1](https://youtu.be/yj2g0bTj6v8) and [video2](https://youtu.be/nCenMVr8JkQ).
  * 04/28(Wed) - __**[Q&A]**__ ZOOM Q&A session.
* 04/28-05/05 - Normal Forms for First-Order Logic (Ch9) and Herbrand's Theorem and Ground Resolution (Ch10). 
  * Watch [video1](https://youtu.be/uddtGotfn6w) and [video2](https://youtu.be/JWjBqqNT8mY).
  * 05/05(Wed) - __**NO ZOOM MEETING.**__ National Holiday.
* 05/05-05/12 - Herbrand's Theorem and Ground Resolution (Ch10) and Applications of Herbrand's Theorem (Ch11). 
  * Watch [video1](https://youtu.be/Za3Ib8-XicQ) and [video2](https://youtu.be/wKehLsDALjE).
  * 05/12(Wed) - __**[Q&A]**__ ZOOM Q&A session.
* 05/12-05/26 - Applications of Herbrand's Theorem (Ch11) and Resolution for First-Order Logic (Ch12). 
  * Watch [video1](https://youtu.be/j9F0c3JWQ7E) and [video2](https://youtu.be/BK55oZY2WeM).
  * 05/17(Mon) - __**[Oral Test]**__ ZOOM in-class oral test on Ch8 - Ch11. ([whiteboard1](https://github.com/hongseok-yang/logic21/blob/master/Others/21May17-Test1.png), [whiteboard2](https://github.com/hongseok-yang/logic21/blob/master/Others/21May17-Test2.png), [whiteboard3](https://github.com/hongseok-yang/logic21/blob/master/Others/21May17-Test3.png), [whiteboard4](https://github.com/hongseok-yang/logic21/blob/master/Others/21May17-Test4.png)).
  * 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). 
  * Watch [video1](https://youtu.be/SzGiRIQTIDE) and [video2](https://youtu.be/SfRAdnDC2jw).
  * 06/02(Wed) - __**[Q&A]**__ ZOOM Q&A session.
* 06/02-06/09 - Decidable Theories (Ch14). 
  * Watch [video1](https://youtu.be/Gz2kXyywx7w) and [video2](https://youtu.be/H20s0lbXMvA).
  * 06/09(Wed) - __**[Q&A]**__ ZOOM Q&A session.
* 06/14(Mon) - __**[Oral Test]**__ ZOOM in-class oral test on Ch12 - Ch14.
* 06/16(Wed) - __**NO ZOOM MEETING.**__ Final Exam Period.

## 6. Lecture Notes and Slides

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](https://github.com/hongseok-yang/logic21/blob/master/Notes/lecture1-notes.pdf), [slides](https://github.com/hongseok-yang/logic21/blob/master/Slides/lecture1-slides.pdf)).
* Propositional Logic. ([note](https://github.com/hongseok-yang/logic21/blob/master/Notes/lecture2-notes.pdf), [slides](https://github.com/hongseok-yang/logic21/blob/master/Slides/lecture2-slides.pdf)).
* Equivalences and Normal Forms. ([note](https://github.com/hongseok-yang/logic21/blob/master/Notes/lecture3-notes.pdf), [slides](https://github.com/hongseok-yang/logic21/blob/master/Slides/lecture3-slides.pdf)).
* Polynomial-Time Formula Classes. ([note](https://github.com/hongseok-yang/logic21/blob/master/Notes/lecture4-notes.pdf), [slides](https://github.com/hongseok-yang/logic21/blob/master/Slides/lecture4-slides.pdf)).
* Resolution. ([note](https://github.com/hongseok-yang/logic21/blob/master/Notes/lecture5-notes.pdf), [slides](https://github.com/hongseok-yang/logic21/blob/master/Slides/lecture5-slides.pdf)).
* The DPLL Algorithm. ([note](https://github.com/hongseok-yang/logic21/blob/master/Notes/lecture6-notes.pdf), [slides](https://github.com/hongseok-yang/logic21/blob/master/Slides/lecture6-slides.pdf)).
* The Compactness Theorem. ([note](https://github.com/hongseok-yang/logic21/blob/master/Notes/lecture7-notes.pdf), [slides](https://github.com/hongseok-yang/logic21/blob/master/Slides/lecture7-slides.pdf)).
* First-Order Logic. ([note](https://github.com/hongseok-yang/logic21/blob/master/Notes/lecture8-notes.pdf), [slides](https://github.com/hongseok-yang/logic21/blob/master/Slides/lecture8-slides.pdf)).
* Normal Forms for First-Order Logic. ([note](https://github.com/hongseok-yang/logic21/blob/master/Notes/lecture9-notes.pdf), [slides](https://github.com/hongseok-yang/logic21/blob/master/Slides/lecture9-slides.pdf)).
* Herbrand's Theorem and Ground Resolution. ([note](https://github.com/hongseok-yang/logic21/blob/master/Notes/lecture10-notes.pdf), [slides](https://github.com/hongseok-yang/logic21/blob/master/Slides/lecture10-slides.pdf)).
* Applications of Herbrand's Theorem. ([note](https://github.com/hongseok-yang/logic21/blob/master/Notes/lecture11-notes.pdf), [slides](https://github.com/hongseok-yang/logic21/blob/master/Slides/lecture11-slides.pdf)).
* Resolution for First-Order Logic. ([note](https://github.com/hongseok-yang/logic21/blob/master/Notes/lecture12-notes.pdf), [slides](https://github.com/hongseok-yang/logic21/blob/master/Slides/lecture12-slides.pdf)).
* Compactness for First-Order Logic. ([note](https://github.com/hongseok-yang/logic21/blob/master/Notes/lecture13-notes.pdf), [slides](https://github.com/hongseok-yang/logic21/blob/master/Slides/lecture13-slides.pdf)).
* Decidable Theories. ([note](https://github.com/hongseok-yang/logic21/blob/master/Notes/lecture14-notes.pdf), [slides](https://github.com/hongseok-yang/logic21/blob/master/Slides/lecture14-slides.pdf)).

## 7. Critical Survey

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.

1. Don't postpone this assignments until the last moment.
2. A submission should be at most 3 pages not including bibliography.
3. Topic: MaxSAT Solver.
4. Deadline: __**23:59 of the 3rd of May in 2021 (Monday). Summit in KLMS.**__
5. Thinking about the following questions may help you.
   1. What is a MaxSAT solver? 
   2. 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?
   3. 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?
   4. How well do modern MaxSAT solvers perform? What are the most popular MaxSAT solvers?
   5. What do you think should be the next step in the work on MaxSAT solvers?

## 8. Programming Assignment and Report

#### 8.1. Topic

Implement a SAT solver using the DPLL algorithm with clause learning, which we cover in the course.

#### 8.2. Deadline

__**23:59 of the 24th of May in 2021 (Monday).**__ Summit both your implementation and report in KLMS.

#### 8.3. Programming Language to Use

Python 2.7 and 3.x.

#### 8.4. Format of Input and Output

1. Follow DIMACS input/output requirements. You can learn about these requirements at the following URL: [http://www.satcompetition.org/2009/format-benchmarks2009.html](http://www.satcompetition.org/2009/format-benchmarks2009.html). This is the format used in the SAT competition. 
2. Assume that the input is always in CNF format.

#### 8.5. Input Interface

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.

#### 8.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

#### 8.7. What to Submit in KLMS?

A zip file named "dpll.zip" containing two files:

1. 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.
2. 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.

#### 8.8. Test Cases

The following webpages contain benchmark problems in DIMACS format: [https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html](https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html) and [http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html](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.

#### 8.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.

## 9. 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.

logic21

logic21 Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

logic21

logic21 Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

Download README