logic24

KO | EN

gitlite — search

#hacktoberfest #react #llm #android #deep-learning #linux #macos #nodejs #cli #awesome-list #pytorch #openai #ios #open-source

(★ 12)

No description available.

logic24 Latest Version Download

Download Latest Version (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# 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

#### [May 17] [Homework4](https://github.com/hongseok-yang/logic24/blob/master/Homework/sheet4-questions.pdf) is out.

The homework assignment 4 is out. Submit your solutions in KLMS by 6:00pm on 31 May 2024 (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.

#### [May 16] No lecture on 21 May 2024 (Tuesday).

There will not be a lecture on 21 May 2024 (Tuesday). On the whole day of 21 May, Hongseok will have to be in the interview panel for applicants to the KAIST
graduate program.

#### [May 6] [Homework3](https://github.com/hongseok-yang/logic24/blob/master/Homework/sheet3-questions.pdf) is out.

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

#### [March 30] [Homework2](https://github.com/hongseok-yang/logic24/blob/master/Homework/sheet2-questions.pdf) is out.

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

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

The homework assignment 1 is out. Submit your solutions in KLMS by 6:00pm on 29 March 2024 (Friday).

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

* 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 on Monday in the room 3403 in the E3-1 building.)
* TA: Taeyoung Kim (Email: taeyoungkim21@kaist.ac.kr. Office hour: 4:00pm - 5:00pm on Wednesday in the room 3419 in the E3-1 building.)
* TA: Jaehui Hwang (Email: hwcmi62@kaist.ac.kr. Office hour: 4:00pm - 5:00pm on Wednesday in the room 3419 in the E3-1 building.)

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

* [Homework1](https://github.com/hongseok-yang/logic24/blob/master/Homework/sheet1-questions.pdf) - Deadline: 6:00pm on 29 March 2024 (Friday).
* [Homework2](https://github.com/hongseok-yang/logic24/blob/master/Homework/sheet2-questions.pdf) - Deadline: 6:00pm on 12 April 2024 (Friday).
* [Homework3](https://github.com/hongseok-yang/logic24/blob/master/Homework/sheet3-questions.pdf) - Deadline: 6:00pm on 17 May 2024 (Friday).
* [Homework4](https://github.com/hongseok-yang/logic24/blob/master/Homework/sheet4-questions.pdf) - Deadline: 6:00pm on 31 May 2024 (Friday).

## 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) - Polynomial-Time Formula Classes (Ch4). 
* 03/26(Tue) - Resolution (Ch5). 
* 03/28(Thu) - Resolution (Ch5). 
* 04/02(Tue) - The DPLL Algorithm (Ch6). 
* 04/04(Thu) - The DPLL Algorithm (Ch6). 
* 04/09(Tue) - The Compactness Theorem (Ch7). 
* 04/11(Thu) - Lower Bounds for Resolution.
* 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) - Resolution for First-Order Logic (Ch12). 
* 05/16(Thu) - Compactness for First-Order Logic (Ch13). 
* 05/21(Tue) - __**[NO LECTURE]**__ Interview for KAIST graduate admission.
* 05/23(Thu) - Decidable Theories (Ch14). 
* 05/28(Tue) - Decidable Theories (Ch14). 
* 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.

* History of Mathematical Logic in Computer Science. ([note](https://github.com/hongseok-yang/logic24/blob/master/Notes/lecture1-notes.pdf), [slides](https://github.com/hongseok-yang/logic24/blob/master/Slides/lecture1-slides.pdf)).
* Propositional Logic. ([note](https://github.com/hongseok-yang/logic24/blob/master/Notes/lecture2-notes.pdf), [slides](https://github.com/hongseok-yang/logic24/blob/master/Slides/lecture2-slides.pdf)).
* Equivalences and Normal Forms. ([note](https://github.com/hongseok-yang/logic24/blob/master/Notes/lecture3-notes.pdf), [slides](https://github.com/hongseok-yang/logic24/blob/master/Slides/lecture3-slides.pdf)).
* Polynomial-Time Formula Classes. ([note](https://github.com/hongseok-yang/logic24/blob/master/Notes/lecture4-notes.pdf), [slides](https://github.com/hongseok-yang/logic24/blob/master/Slides/lecture4-slides.pdf)).
* Resolution. ([note](https://github.com/hongseok-yang/logic24/blob/master/Notes/lecture5-notes.pdf), [slides](https://github.com/hongseok-yang/logic24/blob/master/Slides/lecture5-slides.pdf)).
* The DPLL Algorithm. ([note](https://github.com/hongseok-yang/logic24/blob/master/Notes/lecture6-notes.pdf), [slides](https://github.com/hongseok-yang/logic24/blob/master/Slides/lecture6-slides.pdf)).
* Lower Bounds for Resolution. ([note](https://github.com/hongseok-yang/logic24/blob/master/Notes/lecture6b-notes.pdf)).
* The Compactness Theorem. ([note](https://github.com/hongseok-yang/logic24/blob/master/Notes/lecture7-notes.pdf), [slides](https://github.com/hongseok-yang/logic24/blob/master/Slides/lecture7-slides.pdf)).
* First-Order Logic. ([note](https://github.com/hongseok-yang/logic24/blob/master/Notes/lecture8-notes.pdf), [slides](https://github.com/hongseok-yang/logic24/blob/master/Slides/lecture8-slides.pdf)).
* Normal Forms for First-Order Logic. ([note](https://github.com/hongseok-yang/logic24/blob/master/Notes/lecture9-notes.pdf), [slides](https://github.com/hongseok-yang/logic24/blob/master/Slides/lecture9-slides.pdf)).
* Herbrand's Theorem and Ground Resolution. ([note](https://github.com/hongseok-yang/logic24/blob/master/Notes/lecture10-notes.pdf), [slides](https://github.com/hongseok-yang/logic24/blob/master/Slides/lecture10-slides.pdf)).
* Applications of Herbrand's Theorem. ([note](https://github.com/hongseok-yang/logic24/blob/master/Notes/lecture11-notes.pdf), [slides](https://github.com/hongseok-yang/logic24/blob/master/Slides/lecture11-slides.pdf)).
* Resolution for First-Order Logic. ([note](https://github.com/hongseok-yang/logic24/blob/master/Notes/lecture12-notes.pdf), [slides](https://github.com/hongseok-yang/logic24/blob/master/Slides/lecture12-slides.pdf)).
* Compactness for First-Order Logic. ([note](https://github.com/hongseok-yang/logic24/blob/master/Notes/lecture13-notes.pdf), [slides](https://github.com/hongseok-yang/logic24/blob/master/Slides/lecture13-slides.pdf)).
* Decidable Theories. ([note](https://github.com/hongseok-yang/logic24/blob/master/Notes/lecture14-notes.pdf), [slides](https://github.com/hongseok-yang/logic24/blob/master/Slides/lecture14-slides.pdf)).
* Automatic Structures. ([slides](https://github.com/hongseok-yang/logic24/blob/master/Slides/lecture15-slides.pdf)).

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

* Follow DIMACS input/output requirements. You can learn about these requirements at the KLMS or [Archive](https://web.archive.org/web/20190325181937/https://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.

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

* [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.  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:

* [https://github.com/hongseok-yang/logic24/blob/master/Others/Test_Case.zip](https://github.com/hongseok-yang/logic24/blob/master/Others/Test_Case.zip).

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:

* [https://github.com/hongseok-yang/logic21](https://github.com/hongseok-yang/logic21).

logic24

logic24 Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

logic24

logic24 Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

Download README