SAT

충족가능성 문제 SATisfiability problem

명제 논리식이 주어졌을 때, 전체 명제를 참으로 만드는 각 명제의 참/거짓을 찾는 문제
줄여서 SAT 문제라 함
최초로 발견된 NP 완전 문제(모든 NP 문제는 다항 시간에 SAT 문제로 바꿀 수 있음)
- 동시에 모든 SAT 문제는 최대 3개의 변수만 갖는 3-SAT 문제의 결합으로 다항 시간에 바꿀 수 있음
- 모든 NP 문제 → SAT 문제 → 3-SAT 문제
- 3-SAT 문제도 여전히 NP지만, 빨리 푸는 알고리즘이 집중적으로 개발됨
- NP 문제가 있을 때 충분히 빠른 전용 알고리즘이 없다면, 3-SAT으로 바꿔서 풂
최대 2개의 변수만 갖는 2-SAT 문제는 P 문제

SMT Satisfiability Modulo Theories

SMT(Satisfiability Modulo Theories)
- 논리식이 어떤 이론(Theory) 위에서 참이 될 수 있는지를 판단하는 문제
- → "논리적 제약 조건 + 수학적 이론 = 참 가능한가?"
SMT가 사용하는 이론의 예시
- 선형 산술: 정수나 실수 계산
- 배열 이론: 배열의 인덱스와 값 관련 제약
- 비트벡터 이론: 하드웨어 및 암호화 모델링
- 함수 이론: 함수 및 등호 관계 추론

SMT 활용 분야

프로그램 검증:
- 프로그램이 사양(조건)을 항상 만족하는지 자동으로 증명
- 버그나 보안 결함을 사전에 검출
모델 체킹:
- 시스템의 모든 가능한 상태를 논리식으로 표현하여, 오류 상태가 존재하는지를 탐색
스케줄링 / 최적화
- 시간표, 자원 배분 등의 문제를 논리식으로 정형화하여 최적해를 구함
제약 기반 문제 해결
- 퍼즐, 조합 문제(예: 수학 게임, 논리 퍼즐)를 논리 제약으로 표현하고 해답을 도출
AI/자동 reasoning
- 복잡한 추리 문제의 해결

Z3

Z3는 Microsoft Research에서 개발한 고성능 SMT Solver
다양한 수학 이론 위에서 주어진 논리 조건이 만족 가능한지(SAT/UNSAT)를 자동으로 판단
다양한 이론 지원: 정수, 실수, 배열, 비트벡터, 논리 등 복합 이론 처리 가능
모델 생성: 조건을 만족하는 구체적인 값(모델)을 출력함
다양한 언어 지원: Python, C++, Java, SMT-LIB 표준
강력한 최적화 엔진: 조건을 만족하면서 특정 값을 최소화/최대화 가능

설치:

!pip install z3-solver

임포트:

from z3 import *

산수 문제 풀기

x, y = Ints('x y') # 정수 x, y를 정의
s = Solver() # Solver 초기화
s.add(x > 0, x + y == 10, y < 5) # 조건 추가

s.check() # 조건을 충족하는지 확인

m = s.model() # 해 구하기
m # 해 확인

m.eval(x) # x의 값 얻기
m.eval(y) # y의 값 얻기

논리적 조건 확인

age = Int('age') # 나이
entered = Bool('entered') # 영화관 입장 여부 (True/False)

s = Solver() # Solver 설정
s.add(
    Implies(entered, age >= 18), # 규칙: 입장한 사람은 18세 이상이어야 함
    And(entered == True, age == 16), # 입장했지만 16세인 경우도 있음
)

s.check() # 검증(unsat → 충족 못함)

PSAT 언어논리 문제

논리 문제

a, b, c, d, e = Bools('A B C D E')
s = Solver()
s.add(
    Implies(a, b), # A가 채택되면 B도 채택
    Implies(Not(a), And(Not(d), Not(e))), # A가 채택되지 않으면 D와 E 역시 채택되지 않는다
    Implies(b, Or(c, Not(a))), # B가 채택된다면, C가 채택되거나 혹은 A는 채택되지 않는다
    Implies(Not(d), And(a, Not(c))), # D가 채택되지 않는다면, A는 채택 C는 채택되지 않는다
)
s.check() # 확인 → sat (만족하는 경우가 있음)
s.model() # 만족하는 사례 1개

s.push() # 임시 저장
s.add(Not(a)) # A가 채택되지 않는 경우가 있는가?
s.check() # unsat → 그런 경우는 없음
s.pop() # 임시 저장한 시점으로 되돌리기

# Not(a)를 Not(b), Not(c), Not(d), Not(e)로 바꿔가면서 확인

최적화 (1) 변수

# 비용 행렬
cost = [
    [9, 999, 6], # 작업0
    [6, 5, 8], # 작업1
    [7, 4, 3], # 작업2
]

# 각 작업이 어떤 작업자(0~2)에게 할당되는지를 나타내는 변수
jobs = Ints('job0 job1 job2')

최적화 (2) 조건

opt = Optimize() # 최적화 준비

opt.add(jobs[0] >= 0, jobs[0] <= 2) # job0은 0~2번 작업자에게 할당
opt.add(jobs[1] >= 0, jobs[1] <= 2) # job1도
opt.add(jobs[2] >= 0, jobs[2] <= 2) # job2도

opt.add(Distinct(jobs)) # 할당된 작업자는 모두 달라야함

최적화 (3) 풀기

# 비용
costs = []
for j in range(3):
    for w in range(3):
        costs.append(If(jobs[j] == w, cost[j][w], 0)) # j번 작업을 w가 할 때 비용

total_cost = Sum(costs) # 비용 합계
opt.minimize(total_cost) # 비용 합계가 최소가 되도록
opt.check() # 만족하는가?
m = opt.model() # 만족하는 사례
m # 결과 보기
m.eval(total_cost) # 비용