SAT(Boolean Satisfiability Problem)와 SMT(Satisfiability Modulo Theories)

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

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

 

① SAT(Boolean Satisfiability Problem)는 가장 기본적인 결정 문제(determinant problem) 중 하나로, 주어진 불리언(참/거짓) 논리식이 참인 값을 가질 수 있는지를 판별하는 문제다.

② SAT 문제에서는 논리식이 불리언 변수로 구성된다. 이 변수들은 AND, OR, NOT 등의 불리언 연산자로 연결된다.

③ SAT를 이용해 회로 설계 검증, 소프트웨어 검증, 암호학 등에서 사용할 수 있다.

④ SAT 문제를 해결하기 위해 개발된 알고리즘 중 가장 유명한 게 DPLL(Davis-Putnam-Logemann-Loveland) 알고리즘이다.

⑤ SMT(Satisfiability Modulo Theories)는 SAT의 확장된 형태로 불리언 논리식 뿐만 아니라 다양한 수학적 이론들(정수론, 실수론, 배열 이론 등)을 포함한 논리식의 만족 가능성을 판별한다.

  ㉠ 이 제약 조건은 수학적 이론들, 예를 들어 실수, 정수, 배열, 비트 벡터 등에 대한 규칙과 관계를 포함한다.

  ㉡  SMT 솔버는 내부적으로는 SAT 솔버를 기반으로 하면서 추가적인 이론별 솔버를 통해 특정 수학적 이론에 관한 문제를 해결한다.

②③④⑤⑥⑦⑧⑨⑩⑪⑫⑬⑭⑮
㉠㉡㉢㉣㉤㉥㉦㉧㉨㉩㉪㉫㉬㉭
ⓐⓑⓒⓓⓔⓕⓖⓗⓘⓙⓚⓛⓜ