-
-
Notifications
You must be signed in to change notification settings - Fork 18
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
5 changed files
with
71 additions
and
7 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
--- | ||
date: '2023-11-19' | ||
lang: 'en' | ||
slug: '/2023-11-19' | ||
--- | ||
|
||
[[3-SAT]] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,52 @@ | ||
--- | ||
lang: 'en' | ||
slug: '/DCB869' | ||
--- | ||
|
||
import Tabs from '@theme/Tabs'; | ||
import TabItem from '@theme/TabItem'; | ||
|
||
<Tabs groupId='lang' queryString> | ||
<TabItem value='en' label='English ๐บ๐ธ' lang='en-US' default> | ||
<div lang='en-US'> | ||
|
||
The 3-SAT (3-Satisfiability) problem is a classic problem in computer science, particularly in the field of computational complexity theory. It's a specific type of Boolean satisfiability problem (SAT), which is foundational in the study of algorithmic logic and has significant implications in various areas like cryptography, artificial intelligence, and algorithm design. | ||
|
||
Here's a basic overview of what the 3-SAT problem entails: | ||
|
||
1. **Boolean Variables** โ The problem involves a set of Boolean variables. Each variable can take on one of two values: true or false. | ||
|
||
2. **Clauses** โ The heart of the problem lies in a series of clauses. Each clause is a disjunction (logical OR) of exactly three literals. A literal is either a variable or its negation. For example, a clause might be $(x \lor \neg y \lor z)$, where $x, y,$ and $z$ are Boolean variables, and $\neg y$ represents the negation of $y$. | ||
|
||
3. **Satisfiability** โ The question posed by the 3-SAT problem is whether there exists an assignment of values to the variables that makes the entire Boolean expression true. In other words, can we assign true/false values to each variable in such a way that every clause has at least one true literal? | ||
|
||
4. **NP-Completeness** โ The 3-SAT problem is famously known for being NP-complete, which means two things: | ||
- It's in NP (nondeterministic polynomial time), meaning that if a solution exists, it can be verified quickly (in polynomial time). | ||
- Every problem in NP can be reduced to it in polynomial time. This makes 3-SAT a central problem in complexity theory, as finding a polynomial-time algorithm for it (if one exists) would imply P = NP, solving a major open question in computer science. | ||
|
||
The importance of 3-SAT and other SAT problems lies in their applicability to real-world scenarios where complex decision-making is required. They are used in various domains like electronic design automation, model checking, software verification, scheduling, and more. The challenge in solving these problems efficiently has driven much of the research in algorithm development and complexity theory. | ||
|
||
</div> | ||
</TabItem> | ||
<TabItem value='ko' label='ํ๊ตญ์ด ๐ฐ๐ท' lang='ko-KR'> | ||
<div lang='ko-KR'> | ||
|
||
3-SAT(3-๋ง์กฑ๊ฐ๋ฅ์ฑ) ๋ฌธ์ ๋ ์ปดํจํฐ ๊ณผํ, ํนํ ๊ณ์ฐ ๋ณต์ก์ฑ ์ด๋ก ๋ถ์ผ์์์ ๊ณ ์ ์ ์ธ ๋ฌธ์ ์ด๋ค. ์ด๋ Boolean ๋ง์กฑ ๊ฐ๋ฅ์ฑ ๋ฌธ์ (SAT)์ ํน์ ์ ํ์ผ๋ก, ์๊ณ ๋ฆฌ์ฆ ๋ ผ๋ฆฌ ์ฐ๊ตฌ์ ์ํธํ, ์ธ๊ณต์ง๋ฅ, ์๊ณ ๋ฆฌ์ฆ ์ค๊ณ์ ๊ฐ์ ๋ค์ํ ๋ถ์ผ์์ ์ค์ํ ์๋ฏธ๋ฅผ ๊ฐ์ง๊ณ ์๋ค. | ||
|
||
3-SAT ๋ฌธ์ ์ ๊ธฐ๋ณธ ๊ฐ์๋ ๋ค์๊ณผ ๊ฐ๋ค: | ||
|
||
1. **Boolean ๋ณ์** โ ์ด ๋ฌธ์ ์๋ Boolean ๋ณ์๋ค์ ์งํฉ์ด ํฌํจ๋๋ค. ๊ฐ ๋ณ์๋ ์ฐธ ๋๋ ๊ฑฐ์ง, ๋ ๊ฐ์ง ๊ฐ ์ค ํ๋๋ฅผ ๊ฐ์ง ์ ์๋ค. | ||
|
||
2. **Clause** โ ๋ฌธ์ ์ ํต์ฌ์ ์ฌ๋ฌ Clause๋ค์ ์๋ค. ๊ฐ Clause์ ์ ํํ ์ธ ๊ฐ์ ๋ฆฌํฐ๋ด์ ๋ ผ๋ฆฌํฉ(๋๋ ์ฐ์ฐ)์ด๋ค. ๋ฆฌํฐ๋ด์ ๋ณ์ ๋๋ ๊ทธ ๋ถ์ ์ด๋ค. ์๋ฅผ ๋ค์ด, ํ๋์ Clause์ $(x \lor \neg y \lor z)$์ผ ์ ์๋๋ฐ, ์ฌ๊ธฐ์ $x, y,$ ๊ทธ๋ฆฌ๊ณ $z$๋ Boolean ๋ณ์์ด๋ฉฐ, $\neg y$๋ $y$์ ๋ถ์ ์ ๋ํ๋ธ๋ค. | ||
|
||
3. **๋ง์กฑ ๊ฐ๋ฅ์ฑ** โ 3-SAT ๋ฌธ์ ์์ ์ ๊ธฐ๋๋ ์ง๋ฌธ์ ๋ณ์์ ๊ฐ์ ํ ๋นํ์ฌ ์ ์ฒด Boolean ํํ์์ ์ฐธ์ผ๋ก ๋ง๋ค ์ ์๋์ง์ ์ฌ๋ถ์ด๋ค. ์ฆ, ๊ฐ ๋ณ์์ ์ฐธ/๊ฑฐ์ง ๊ฐ์ ํ ๋นํ์ฌ ๋ชจ๋ Clause์ ์ ์ด๋ ํ๋์ ์ฐธ ๋ฆฌํฐ๋ด์ด ์๊ฒ ํ ์ ์๋๊ฐ? | ||
|
||
4. **NP-์์ ์ฑ** โ 3-SAT ๋ฌธ์ ๋ NP-์์ ์ด๋ผ๊ณ ์ ๋ช ํ๋ฉฐ, ์ด๋ ๋ ๊ฐ์ง๋ฅผ ์๋ฏธํ๋ค: | ||
- NP(๋น๊ฒฐ์ ์ ๋คํญ ์๊ฐ)์ ์ํ๋ค๋ ๊ฒ, ์ฆ ํด๊ฒฐ์ฑ ์ด ์กด์ฌํ๋ค๋ฉด ๋น ๋ฅด๊ฒ(๋คํญ ์๊ฐ ์์) ํ์ธ๋ ์ ์๋ค. | ||
- NP์ ์ํ๋ ๋ชจ๋ ๋ฌธ์ ๊ฐ ๋คํญ ์๊ฐ ์์ ์ด ๋ฌธ์ ๋ก ํ์๋ ์ ์๋ค๋ ๊ฒ์ด๋ค. ์ด๋ 3-SAT์ ๋ํ ๋คํญ ์๊ฐ ์๊ณ ๋ฆฌ์ฆ์ ์ฐพ๋ ๊ฒ(๋ง์ฝ ์กด์ฌํ๋ค๋ฉด)์ด ์ปดํจํฐ ๊ณผํ์์ ์ฃผ์ํ ๋ฏธํด๊ฒฐ ์ง๋ฌธ์ธ P = NP๋ฅผ ํด๊ฒฐํ ์ ์์์ ์๋ฏธํ๋ค. | ||
|
||
3-SAT ๋ฐ ๊ธฐํ SAT ๋ฌธ์ ๋ค์ ์ค์์ฑ์ ๋ณต์กํ ์์ฌ๊ฒฐ์ ์ด ํ์ํ ์ค์ ์๋๋ฆฌ์ค์ ์ ์ฉ๋ ์ ์๊ธฐ ๋๋ฌธ์ด๋ค. ์ด๋ค์ ์ ์ ์ค๊ณ ์๋ํ, ๋ชจ๋ธ ์ฒดํน, ์ํํธ์จ์ด ๊ฒ์ฆ, ์ค์ผ์ค๋ง ๋ฑ ๋ค์ํ ๋ถ์ผ์์ ์ฌ์ฉ๋๋ฉฐ, ์ด๋ฌํ ๋ฌธ์ ๋ค์ ํจ์จ์ ์ผ๋ก ํด๊ฒฐํ๋ ๋์ ์ ์๊ณ ๋ฆฌ์ฆ ๊ฐ๋ฐ๊ณผ ๋ณต์ก์ฑ ์ด๋ก ์ฐ๊ตฌ๋ฅผ ํฌ๊ฒ ์ด์ง์์ผฐ๋ค. | ||
|
||
</div> | ||
</TabItem> | ||
</Tabs> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters