SAT(Boolean Satisfiability Problem)

※ 이 글은 chatGPT를 기반으로 작성한 글입니다.

※ Coursera의 Automated Reasoning: satisfiability 강의를 기반으로 작성한 글입니다.

① SAT는 수리논리학에서 중요한 개념으로 명제 논리의 만족 가능성(Satisfiability in Propositional Logic) 문제를 나타낸다.

  ㉠ 즉 SAT 문제는 주어진 명제 논리 공식에 대해 그 공식을 참으로 만드는 변수 값이 존재하는 지를 확인하는 것이다.

② SAT 문제의 특징은 다음과 같다.

  ㉠ 공식이 만족 가능(satisfiable)하다는 것은 그 공식이 참이 되도록 하는 변수 값이 존재한다는 것이다.

  ㉡ 공식이 비만족 가능(unsatisfiable)하다는 것은 어떤 변수 값을 할당해도 공식을 참으로 만들 수 없다는 것이다.

  ㉢ SAT 문제는 결정 문제의 한 예시이다. 즉, '이 공식은 만족 가능한가?' 라는 질문에 '예' 또는 '아니오'로 답할 수 있는 문제이다.

  ㉣ SAT는 최초로 NP 완전(NP-Complete) 문제임이 증명된 문제이다.

③ 예를 들어 명제 논리 공식 \( ¬((P ∧ Q) → (P ∨ R))\)은 P가 참이고, Q가 참일 때 참이 된다.

④ 진리표를 이용한 방법은 효과적이지만, 변수(명제)의 개수가 증가함에 따라 지수적으로 증가하기 때문에 항상 효과적이지는 않다.

  ㉠ 그러나 SAT Solver를 이용해 10000개의 변수를 초과하는 명제에 대해서도 10초 만에 풀 수 있게 되었다.