Logic for Programmers를 집필하면서 나는 ‘겨’라고 부를 만한 것들을 많이 만들어냈다. 써놓고는 버린 코드 샘플과 섹션들이다. 같은 주제에 더 나은 예제를 찾아 버린 경우도 있고, 주제 자체를 통째로 버린 경우도 있었다. 하드 드라이브에서 썩게 두기 아까워서, 소프트웨어 연구에서 다양하게 활용되는 ‘Z3’라는 도구를 위해 만들어 둔 겨들 중 일부를 공유하려 한다.

먼저 이 도구가 정확히 무엇인지 설명하고, 그 다음 점점 더 흥미로운 순서대로 스크립트 몇 가지를 소개하겠다. 모든 예제는 Python 바인딩(pip install z3-solver)을 사용한다.

Z3란 무엇인가?

Z3는 SMT 솔버다.

좋아, 그럼 SMT는 뭔가?

SMT(“Satisfiability Modulo Theories”) 솔버는 수학과 기초적인 프로그래밍 개념을 이해하는 제약 솔버다. 변수 몇 개와 그 변수들이 들어간 식 몇 개를 넘기면, 모든 식을 만족하는 할당 집합, 즉 모델을 찾아주려 시도한다.

12살이 되어 처음으로 대수학 I을 듣는데 이런 문제를 마주했다고 상상해 보자:

4x + 2y == 14
2x - y  == 1
solve for x & y

원래는 이걸 연립방정식으로 푸는 법을 배워야 하지만, 공부를 스스로 포기하고 싶다면 Z3에 대신 풀게 할 수도 있다.

# pip install z3-solver
import z3

s = z3.Solver()
x, y = z3.Ints('x y')

s.add(4*x + 2*y == 14)
s.add(2*x - y  == 1)

result = s.check()
print(result)
if result == z3.sat:
    print(s.model())

이게 Z3를 사용하는 가장 일반적인 방식이다. 솔버를 생성하고, 제약을 추가한 뒤, 체크하는 것이다.¹ Ints('x y')는 두 개의 “상수”를 만든다. s.check()를 호출하면 솔버는 모든 제약을 만족하는 상수들의 값(모델)을 찾으려 한다. 여기서는 “sat” 다음에 [x = 2, y = 3]이 출력된다. 답이 여러 개라면 처음 찾은 하나를 반환하고, 하나도 없으면 “unsat”을 출력한다.

어쨌든 여기까지가 “만족 가능성(satisfiability)” 부분이다. “Modulo Theories” 부분은 Z3가 서로 다른 도메인, 즉 “이론(theories)”을 위한 전문화된 솔버들을 잔뜩 품고 있다는 사실에서 온다. 덕분에 배열이나 정규식, 한정 표현식 등이 포함된 제약도 처리할 수 있다.

이제부터는 소위 ‘쿨한 애들’처럼 Z3 API 전체를 네임스페이스로 불러오자.

스크립트 모음

내가 궁금했던 엉뚱한 수학 질문

서로 다른 네 양의 정수 a, b, c, d 중에서 a + b = c + d이고 a * b = c * d인 경우가 존재할까?

모든 제약을 가장 직접적으로 표현하면 이렇게 된다:

from z3 import *
s = Solver()

a, b, c, d = Ints('a b c d')
s.add(a > 0, b > 0, c > 0, d > 0)
s.add(a + b == c + d)
s.add(a * b == c * d)

# We can add many constraints in one `add` call
s.add(a != b, a != c, a != d, 
      b != c, b != d, c != d)

print(s.check())

이 코드는 “unsat”을 반환한다. 그런 쌍이 존재하지 않는다는 뜻이다. 돌이켜보면 충분히 예상할 수 있었던 결과다. 증명은 드롭다운을 참고하자.

그럼 서로 다른 두 삼중항, 즉 서로 다른 여섯 개 숫자로는 어떨까? 열다섯 개의 not-equals 문을 쓰고 싶지 않으니 약간의 문법적 설탕을 끌어오자:

• IntVector('lhs', 3)는 변수 리스트 [lhs__0, lhs__1, lhs__2]를 반환한다.
• Sum과 Product는 이름 그대로의 기능을 한다.²
• Distinct(l)은 l 안의 모든 값이 서로 달라야 함을 의미한다.

이를 이용하면 스크립트를 훨씬 확장 가능하게 만들 수 있다:

from z3 import *
n = 3
lhs = IntVector("lhs", n)
rhs = IntVector("rhs", n)

s = Solver()
for x in lhs + rhs: 
    s.add(x >= 0) 
s.add(sum(lhs) == sum(rhs))
s.add(Product(lhs) == Product(rhs))
s.add(Distinct(lhs + rhs))

if s.check() == sat:
    m = s.model()
    l = [m[l].as_long() for l in lhs]
    r = [m[r].as_long() for r in rhs]
    print(l, r)
    print(f"sum={sum(l)} prod={Product(l)}")
else:
    print("unsat")

이번에는 실제로 삼중항 쌍을 찾는다. [7, 8, 15]와 [14, 6, 10]은 합이 30, 곱이 840으로 같다.

직접 실행하면 다른 예제가 나올 수도 있다. 만족하는 모델 중 아무거나 달라고 했기 때문이다. 새로운 제약을 추가해 다른 모델을 찾을 수도 있고, 솔버를 옵티마이저로 바꿔 찾은 합이나 곱을 최소화할 수도 있다.

- s = Solver()
+ s = Optimize()
+ s.minimize(Sum(lhs))

이 코드는 [8, 2, 9]와 [4, 12, 3]을 반환한다. 합은 19, 곱은 144다.

연간 납입액 최소화하기

Z3의 옵티마이저는 MiniZinc 같은 전용 제약 솔빙 도구에 비해 오래 걸리지만, 그래도 간단한 문제는 충분히 다룰 수 있다.

연 1% 이자를 주는 은행 계좌가 있다. 20년 뒤에 10,000을 만들려면 매년 최소 얼마를 입금해야 할까? 입금은 이자가 지급된 뒤에 이루어진다고 가정하자.

그러니 1년 차에는 C달러가 있고, 2년 차에는 C*1.01 + C달러가 있는 식이다. SMT에서는 상수의 값을 재할당할 수 없지만, 여기서 Python 추상화가 약간 새어 나온다. 예를 들어 이렇게 쓴다고 하자

x = Int('foo')
x = x + x
s.add(x < 6)

Python 변수 x를 SMT 상수 foo에 할당하는 것처럼 보이지만, 실제로 x에는 “foo의 값”이라는 표현식이 할당된다. x = x + x라는 줄은 x에 “foo의 값 + foo의 값”이라는 표현식을 할당한다는 뜻이며, 따라서 다음 줄은 foo + foo < 6이라는 제약을 추가하게 된다.

이는 복리를 이렇게 계산할 수 있다는 뜻이다:

years = 20
goal = 10000

r = RealVal('1.01')
c = Real('c')
balance = c

for t in range(1, years):
    balance = balance*r+c

이번에는 Int 대신 Real을 쓰고 있다. Real은 무한 정밀도의 부동소수점 같은 것이다.³ r은 Z3가 풀어야 할 대상이 아니라 고정된 값이므로 RealVal이어야 한다. 이렇게 하면 20년 뒤 balance의 최종 값을 계산하게 된다.

그렇다고는 해도 이 방식으로는 14년 차에 balance가 얼마인지 알 수 없다. 중간 결과를 보고 싶다면 balance를 20개짜리 Real 배열로 만들어, balance[0]을 시작값으로 두고 balance[n] == balance[n-1]*r + c가 되도록 하면 된다. 전체 모델은 다음과 같다:

from z3 import * # type: ignore

years = 20
goal = 10000

r = RealVal('1.01')
balance = RealVector('balance', years)
c = Real('c')

opt = Optimize()
opt.minimize(c)

opt.add(balance[0] == c)
for t in range(1, years):
    opt.add(balance[t] == balance[t-1] * r + c)

if opt.check(balance[years-1] >= goal) == sat:
    m = opt.model()
    print(f"c = {m[c].as_decimal(2)}")
    for x, i in enumerate(balance):
        print(f"balance[{x}] = {m[i].as_decimal(2)}")
else:
    print("unsat")

이 코드는 최적 입금액이 C=453.4임을 찾아낸다. 최적화는 워낙 느려서 Z3의 인기 있는 용법은 아니지만, 그래도 꽤 멋진 기능이다.⁴

이는 또 유용한 트릭을 보여준다. check()를 추가 제약과 함께 호출할 수 있다는 것이다. 나도 비교적 최근까지는 이게 가능한 줄 몰랐다! 같은 문제의 여러 인스턴스를 풀 때 유용해 보이지만, 내가 본 바로는 사람들은 하나의 솔버를 새로운 제약으로 ‘파라미터화’하기보다 매번 새로운 솔버 객체를 만드는 쪽을 선호한다.

난수 생성기 역공학

이 책에서 내가 꼭 하고 싶었던 것 중 하나는 소개하는 각 주제가 유용한 응용 사례를 갖도록 하는 것이었다. 모든 프로그래머에게 끌릴 필요는 없고, “이걸 배우면 어딘가 누군가에게 도움이 되겠구나”라고 생각할 만큼만 유용하면 된다. 그래서 난수 생성기(RNG)의 값을 역공학하는 예제를 쓰게 됐다.

소프트웨어의 대부분의 난수 생성기는 사실 의사 난수다. 결정론적 수학 알고리즘을 이용해 대부분의 사용 사례에 “충분히 무작위한” 수열을 생성한다. 이에 대해서는 여기에서 더 자세히 다뤘다. 그런 알고리즘 중 하나가 선형 합동 생성기, 즉 LCG다. LCG는 고정된 상수(a,c,m)와 시작 시드 X를 가지며, 다음 값을 이렇게 계산한다:

X = (a * X + c) % m

예를 들어 a = 6, m = 59, c = 0이라면 1에서 시작하는 수열은 1, 6, 36, 39, 57 등으로 이어진다. 물론 대부분의 수열은 훨씬 더 큰 값을 사용한다. 수열과 m을 받아 (a, c)를 역산하는 SMT 문제를 작성해 보자.

from z3 import *
s = Solver()

modulus = 2**31
sequence = [4096, 618876929, 113892918, 1048278319]

a = Int('a')
c = Int('c')

s.add(0 <= a, a < modulus)
s.add(0 <= c, c < modulus)

for i in range(len(sequence) - 1):
    s.add(sequence[i+1] == c + (a * sequence[i]) % modulus)

if s.check() == sat:
    model = s.model()
    print(f"a = {model[a]}")
    print(f"c = {model[c]}")

이 코드는 a = 22695477, c = 1을 반환하는데, 이는 예전 Borland C++ 컴파일러의 RNG다. 장난감 같은 예제일 뿐이지만, 같은 접근 방식은 선형 되먹임 시프트 레지스터나 메르센 트위스터에도 통한다.

정리 증명하기

Z3 저장소에서는 Z3를 정리 증명기라고 부른다. 즉, 수학 정리를 참이라고 증명할 수 있어야 한다는 뜻이다.

이는 “논리적 쌍대성”이라는 성질에 기반해 동작한다. “덧셈은 교환법칙을 만족한다”는 정리, 즉 모든 a, b ∈ Real: a + b = b + a를 예로 들어보자. 이는 “!(a + b == b + a)인 a, b가 존재하지 않는다”고 말하는 것과 논리적으로 동치다. 따라서 Z3에게 부정을 풀어보라고 요청할 수 있다. 반례를 찾지 못하면 그 정리는 참인 것이다.

from z3 import *

s = Solver()

a, b = Reals('a b')
theorem = a + b == b + a

if s.check(Not(theorem)) == sat:
    print(f"Counterexample: {s.model()}")
else:
    print("Theorem true")

# Prints Theorem true

보통 정리에는 “만약 a != 0이라면, 그러면 a * b == 1인 b가 존재한다” 같은 조건이 붙는다. 수학자는 이를 a != 0 => some b: a*b == 1이라고 쓴다. Z3에서는 p => q를 Implies(p, q)라고 쓰며, 이는 평소처럼 부정하면 된다.

from z3 import *
s = Solver()

a, b = Reals('a b')
theorem = Implies(a != 0, Exists(b, a*b == 1))
if s.check(Not(theorem)) == sat:
    print(f"Counterexample: {s.model()}")
else:
    print("Theorem true")

이 코드는 “Theorem true”를 반환한다. 정리를 증명할 수 있다는 점 덕분에 SMT 솔버는 형식 검증에 절대적으로 필수적인 도구가 된다. 프로그래밍 함수를 Z3 식들의 집합으로 변환할 수 있다면, 그 함수가 기대하는 성질을 가진다는 것을 증명할 수 있다.

주식 고르기

이 Z3 예제들을 만들던 시기에 나는 MiniZinc 같은 일반 제약 솔버를 위한 예제도 함께 만들고 있었다. 그 과정에서 나온 겨 일부를 뉴스레터에 공유하기도 했다. 그중 몇 개를 Z3 연습 삼아 형식화했는데, 그중 하나가 특히 흥미로웠다.⁵

하루 동안의 주가 목록이 주어졌을 때, 주식 한 주를 샀다가 나중에 한 주를 팔아 얻을 수 있는 최대 이익을 구하라.

충분히 간단해 보인다:

arr = [3,1,4,1,5,9,2,6,5,3,5,8]
buy, sell = Ints('i j')
opt.add(buy < sell)
opt.maximize(arr[sell] - arr[buy])

그런데 이렇게 하면 이런 오류가 난다:

TypeError: list indices must be integers or slices, not ArithRef

문제는 Z3가 SMT 변수를 이용해 Python 배열을 인덱싱할 수 없다는 것이다. 대신 Z3에는 “배열 이론”이 있어서 배열 자체를 Z3 변수로 추가할 수 있다:

from z3 import *
opt = Optimize()

arr = [3,1,4,1,5,9,2,6,5,3,5,8]
arr_z3 = Array('A', IntSort(), IntSort())
for i, v in enumerate(arr):
    opt.add(Select(arr_z3, i) == v)

buy, sell = Ints('i j')
opt.add(buy < sell)

opt.maximize(Select(arr_z3, sell) - Select(arr_z3, buy))
if opt.check() == sat:
    m = opt.model()
    buy_val = m.evaluate(arr_z3[buy])
    sell_val = m.evaluate(arr_z3[sell])
    profit = m.evaluate(sell_val - buy_val)
    print(f"buy at {m[buy]} for {buy_val}")
    print(f"sell at {m[sell]} for {sell_val}")
    print(f"profit: {profit}")

여기까지는 좋다. 하지만 이제 새로운 문제가 생긴다:

buy at 21237 for -2
sell at 21238 for 0
profit: 2

무슨 일이 일어나고 있는지 이해하려면 SMT 배열이 실제로 “무엇”인지 이해해야 한다. 배열은 사실 키-값 맵에 더 가깝다. 키 “sort”(기본적으로 타입)와 값 sort를 가진다. 그래서 우리의 “배열” arr_z3는 정수를 정수에 매핑한다. 배열은 또한 Select(A, i)와 Store(A, i, val)(새 배열을 반환하는) 연산자를 가져야 한다.⁶ SMT 연산은 모든 가능한 입력에 대해 전체(total)여야 하므로, Select(A, i)는 i가 무엇이든 값을 반환해야 한다. 이 모든 것은 배열이 우리가 의도적으로 제약하는 것 외에는 “길이”나 “경계”라는 개념이 없다는 뜻이다. 다음은 유효한 Z3 프로그램이다:

arr = Array('A', IntSort(), IntSort())
s = Solver()
s.check(Select(arr, 3) > Select(arr, -9))
print(s.model())

내 환경에서는 [A = Store(K(Int, -1), 3, 0)]이 출력되는데, 이는 “모든 정수를 -1에 매핑하되 3만 0에 매핑하는 배열”이라는 뜻이다.

이로써 Z3가 왜 21237에 주식을 살 수 있었는지 설명이 된다. 문제를 제대로 모델링하려면 buy와 sell을 우리가 값을 명시적으로 정의한 인덱스 범위로 제한해야 한다.

 opt.add(buy < sell)
+ opt.add(0 <= buy, sell < len(arr))

이제야 최대 이익 8을 올바르게 반환한다.

(무한 배열이 도대체 어디에 쓰일까? 모든 문자열을 정수에 매핑하는 배열은 String -> Int 함수와 동치다. 즉 Z3가 제약을 만족하는 함수를 찾을 수 있다는 뜻이다! 다만 나는 실전에서 진지하게 써본 적은 없다.)

책에 넣은 내용

나는 SMT 예제에 세 가지 목표를 세웠다. 논리를 처음 접하는 사람도 이해할 수 있어야 하고, 일부 독자가 실제 업무에서 마주할 법한 실용적인 문제처럼 보여야 하며, SMT 솔버가 그 문제를 푸는 데 적합한 도구여야 한다는 것이었다. 그리고 위의 예제들은 대부분 이 중 최소 하나를 만족하지 못한다:

• 숫자 삼중항을 찾는 것이 업무인 사람은 없다.
• RNG 역공학을 시연하려면 PRNG와 LCG를 설명하는 데 많은 시간을 써야 한다.
• 일반적인 제약 솔버(같은 장에서 다룬다)는 SMT 솔버보다 수치 최적화 문제를 훨씬 빠르게 풀 수 있다.

결국 나는 세 가지 예제로 정착했다:

1. 제약 솔버가 할 수 없는 최적화 문제. 대부분의 솔버는 숫자만 다루므로 “가장 긴 공통 부분 문자열 찾기”는 좋은 선택이다.
2. 아주 간단한 수학적 성질 증명, 주로 (3)을 위한 동기 부여 차원
3. 간단한 Python 함수 형식 검증

또한 Z3가 “머신 정수”에 대한 제약을 풀 수 있음을 보여주는 간단한 스크립트도 작성했다. 머신 정수는 비트벡터로 표현된다.

이 선택들이 정말 좋은 선택이었는지는 피드백을 통해 알게 될 것이다!

다른 예제와 Z3 자료

책에는 넣지 않은 예제가 몇 가지 더 있다:

• 테스트 케이스를 통과하는 다항식 도출하기
• LinkedIn Queens 풀기

다른 사람들이 만든 예제:

• Andrew Helwer의 Firewall Equivalence
• Nelson Elhage의 Crossword Solver
• Hakan Kjellerstrand의 퍼즐과 토이 모델

추가 자료:

• 개발자가 만든 z3py 튜토리얼
• Microsoft Research의 온라인 Z3 가이드. SMT-LIB 튜토리얼에서는 Python SDK에서 지원하지 않는 최신 Z3 기능도 볼 수 있다.
• Z3가 따르는 SMT-Lib 표준.

Nelson Elhage에게 피드백에 감사드린다. 이 글이 마음에 들었다면 내 뉴스레터에 가입해 보자! 매주 새로운 에세이를 올리고 있다.

내 책 Logic for Programmers는 이제 콘텐츠가 완성되었다! 기술 검토자의 피드백을 기다리는 동안 여기에서 현재 베타 버전과 향후 업데이트를 20% 할인된 가격에 만나볼 수 있다.

업데이트 2026-02-26

Jeremy Salwen이 정리 예제들이 결과가 sat이 아니면 반드시 unsat일 것이라고 가정하고 있지만, SMT 솔버는 둘 다 반환하지 못하고 실패할 수도 있다고 지적했다. Mea Culpa! 대신 검사를 이렇게 작성해야 한다:

result = s.check(Not(theorem))
if result == sat:
    print(f"Counterexample: {s.model()}")
elif result == unknown:
    print("Could not prove or disprove theorem")
else:
    print("Theorem true")

이것이 z3.prove 편의 함수가 대략 정의된 방식이다.

1. Python API는 smtlib로 컴파일되는 느슨한 레이어다. 솔버에 실제로 전달되는 내용을 보고 싶다면 스크립트 끝에 print(s.sexpr())를 추가하면 된다. [return]
2. 이들은 Python API가 제공하는 더 높은 수준의 편의 함수라는 점에 유의하자. 실제로 생성되는 Z3 코드는 Prod(lhs)를 (* (lhs__0 lhs__1 lhs__2))로 인라인한다. [return]
3. 엄밀히 말하면 이는 대수적 수(algebraic)다. Real에는 2의 제곱근은 넣을 수 있지만, Pi 같은 건 넣을 수 없다. [return]
4. Z3의 코어 엔진은 C++로 되어 있는데도, 손으로 작성한 Python 이진 탐색이 최적의 c를 약 1000배 더 빠르게 찾는다! Z3의 최적화는 정말 느리다. [return]
5. 그 뉴스레터와 이 글 사이에 Abdul Rahman Sibahi가 A Dumb Introduction to z3를 썼는데, 여기에는 뉴스레터의 잔돈 세기 문제에 대한 Z3 변환이 포함되어 있다. 그래서 나는 그걸 쓸 필요가 없었다! [return]
6. Python API는 A[i]를 select(A, i)로 desugar하므로, 최적화 목표를 arr_z3[sell] - arr_z3[buy]로 쓰고 제약 루프를 [arr_z3[i] == arr[i] for i in range(len(arr))])로 쓸 수도 있다. 나는 투명성을 위해 명시적으로 select를 사용했다. [return]