한동안 저는 Z3와 더 넓게는 SMT 솔빙에 매료되어 있었습니다. 최근 육아 휴직 중에 정규식 크로스워드 퍼즐의 존재가 떠올랐고, Z3 기반 솔버를 작성하며 nerdsniped되는 것을 스스로 허용했습니다.

처음에는 오후 정도면 가볍게 솔버 하나 뚝딱 만들 수 있을 거라 생각했습니다. 하지만 막상 해보니 Z3 성능을 이해하고 디버깅하는 데 빠져들었고, 예상보다 훨씬 더 많은 것을 Z3와 SMT에 대해 배우게 됐습니다. 이 글에서는 제가 접근한 방식과 초기 솔버를 설명한 뒤, 이후 탐구했던 개선 방법과 여러 변형을 깊이 다뤄보겠습니다.

모든 코드는 github에서 볼 수 있습니다. 따라 해보거나 최종 결과를 확인하고 싶다면 참고하세요.

정규식 크로스워드

간단히 복습하자면, 정규식 크로스워드는 (아직 정해지지 않은) 문자들로 채워진 격자로 구성되며, 이 문자들을 결정해야 합니다. 이 문자들은 주어진 정규식들에 의해 제약을 받으며, 격자를 채운 뒤 각 행이나 열이 해당 정규식과 일치해야 합니다. 저는 특히 regexle 변형을 풀기로 했는데, 이 변형은 육각형 격자를 사용합니다. 다만 제 코드 대부분은 다른 변형에도 쉽게 적용할 수 있습니다.

정규식을 DFA로

Z3 같은 제약 솔버로 퍼즐을 풀려면 “이 문자 시퀀스가 이 정규식과 일치한다”는 제약을 인코딩할 방법을 찾아야 합니다. 그리고 모든 단서를 assert한 뒤, 모든 제약을 만족하는 격자를 요청하면 됩니다.

제가 가장 먼저 떠올린 아이디어는 정규식이 정규 언어¹를 기술한다는 사실에 기대는 것이었고, 따라서 결정적 유한 오토마톤으로 인식할 수 있다는 점이었습니다. 그러면 정규식을 DFA로 인코딩하고, Z3에서 정규식 매칭을 그 전이 함수로 표현할 수 있습니다².

즉, 세 글자 문자열 S = [c0, c1, c2]와 해당 정규식에 대한 전이 테이블 T : State × Char → State가 있다면, “정규식이 S와 일치한다”는 것을 다음과 같이 표현할 수 있습니다:

state_0 = init_state
state_1 = T(state_0, c0)
state_2 = T(state_1, c1)
state_3 = T(state_2, c2)
assert(state_3 in accept_states)

정규식을 DFA로 변환하기

조금 검색해보니 qntm의 greenery 라이브러리를 발견했는데, 정확히 제가 찾던 것이었습니다. 정규식을 다루기 위한 비교적 단순한 파이썬 라이브러리로, 정규식 구문과 DFA(라이브러리에서는 FSM이라고 부릅니다) 사이의 변환을 포함합니다. FSM을 만들어 주고, 전반적으로 원시 성능보다는 단순성과 사용 편의성, 실험 용이성에 최적화되어 있는데, 우리에게는 전혀 문제되지 않습니다. 무거운 작업은 어차피 Z3가 할 테니까요.

한 가지 복잡한 점은 greenery가 임의의 유니코드 문자에 대한 정규식을 처리한다는 것입니다. 거대한 룩업 테이블을 피하기 위해 전이를 문자 범위 단위로 표현하는데, 다루기가 조금 더 까다로웠습니다. 이 프로젝트에서는 알파벳을 영문 대문자(A-Z)로 가정해도 괜찮다고 판단했기에, greenery의 구조를 평탄한 numpy 전이 테이블로 변환하는 헬퍼를 작성했습니다:

ALPHABET = string.ascii_uppercase

def flatten_fsm(fsm):
    nstate = len(fsm.states)
    nvocab = len(ALPHABET)

    assert fsm.states == set(range(nstate))
    state_map = np.full((nstate, nvocab), -1, dtype=np.int32)
    for st, map in fsm.map.items():
        for i, c in enumerate(ALPHABET):
            for cc, dst in map.items():
                if cc.accepts(c):
                    state_map[st, i] = dst
                    break
    return state_map

또 단일 정규식에 대한 여러 표현과 분석 결과를 함께 묶기 위해 작은 dataclass도 정의했습니다:

@dataclass
class Regex:
    pattern: str
    parsed: greenery.Pattern

    # 2d: (state, vocab) -> new state
    transition: np.ndarray
    # 1d: state -> bool
    accept: np.ndarray

    @classmethod
    def from_pattern(cls, pattern: str):
        parsed = greenery.parse(pattern)
        fsm = parsed.to_fsm().reduce()

        transition = flatten_fsm(fsm)
        nstate = transition.shape[0]
        accept = np.zeros((nstate,), bool)
        for st in fsm.finals:
            accept[st] = True

        return cls(
            pattern=pattern,
            parsed=parsed,
            transition=transition,
            accept=accept,
        )

Z3로 매핑하기

이제 조각들을 맞추기 위해 각 단서에 대한 전이 함수를 Z3에 알려주고, 격자의 각 문자에 대해 Z3 변수를 정의한 뒤, 해당 전이 함수를 이용해 문자들에 적절한 제약을 추가해야 합니다.

저는 상태와 문자 모두를 정수(integer)로 표현하기로 했습니다(값이 범위 내에 있음을 보장하는 assertion을 추가하면서). 가장 단순해 보였기 때문입니다. 그런 다음 상태와 문자 사이의 전이 함수 관계를 인코딩해야 합니다.

Z3는 함수 타입을 지원하며, 이를 식과 assertion에서 선언하고 다룰 수 있습니다. 따라서 적절한 타입의 함수를 선언하고, 전이 테이블의 각 항목에 대해 assertion을 이용해 Z3에 그 동작을 알려줬습니다:

def build_func(solv: z3.Solver, clue: Clue):
    ctx = solv.ctx
    state_func = z3.Function(
        clue.name + "_trans",
        z3.IntSort(ctx),
        z3.IntSort(ctx),
        z3.IntSort(ctx),
    )
    pat = clue.pattern

    for (state, char), next_state in pat.all_transitions():
        solv.add(state_func(state, char) == next_state)

    return state_func

이 정의가 주어지고, (문자 리스트로 표현된) 문자열이 주어지면, “정규식 매칭” 제약을 쉽게 표현할 수 있습니다:

def assert_matches(solv: z3.Solver, clue: Clue, chars: list[z3.AstRef]):
    state_func = self.build_func(solv, clue)
    pat = clue.pattern

    # Create constants for each state
    states = z3.IntVector(clue.name + "_state", 1 + nchar, ctx=solv.ctx)

    # Express the transition requirement
    for i, ch in enumerate(chars):
        solv.add(state_func(states[i], ch) == states[i + 1])

    # Each state must be valid
    for st in states:
        solv.add(0 <= st)
        solv.add(st < pat.nstate)
    # State zero is the initial state
    solv.add(states[0] == 0)

    # The final state must be accepting
    solv.add(z3.Or([
        states[-1] == i
        for i, ok in enumerate(pat.accept) if ok
    ])

하나로 합치기

이러한 기본 요소들을 갖추면 이제 문자 격자를 정의하고 적절한 assertion을 추가하기만 하면 됩니다. 저는 여전히 regexle을 테스트 케이스 소스로 사용하고 있었습니다. regexle은 육각형 격자에서 동작하는데, 육각형 격자와 세 가지 단서 축 사이의 좌표 매핑이 사실 이 작업에서 가장 어려운 부분 중 하나였습니다! 그 부분은 넘어가고, 코드는 매우 단순합니다:

def make_char(solv: z3.Solver, name: str) -> z3.ExprRef:
    ch = z3.Int(name, solv.ctx)
    solv.add(0 <= ch)
    solv.add(ch < len(ALPHABET))
    return ch

grid = [
    [make_char(solv, f"grid_{x}_{y}") for y in range(maxdim)]
    for x in range(maxdim)
]

for clue in all_clues:
    coords = word_coords(clue.axis, clue.index)
    chars = [grid[x][y] for x, y in coords]

    assert_matches(
        solv,
        clue,
        chars,
    )

솔버 성능

이 시점에서 모든 조각을 맞춘 뒤 크로스워드를 풀 수는 있었지만, 속도가 … 고통스러울 정도로 느렸습니다. 3x3 퍼즐 중 일부는 제 M1 MacBook Air에서 Z3 시간으로 10분 이상이 걸렸습니다! Z3가 여러 코어를 사용하도록 하는 방법을 알아냈고, 이는 약간의 상수 배수만큼 빨라지긴 했지만, 근본적으로 너무 느리다는 느낌이 들었습니다.

막연한 내부적 감각으로, Z3라면 이런 퍼즐을 밀리초 단위로 풀어야 한다고 예상했습니다. 그래서 왜 솔버가 이렇게 느린지, 어떻게 하면 빨라질 수 있는지 디버깅하고 이해하는 데 시간을 쓸 수밖에 없었습니다.

당시 저는 완전한 Z3 초보자라서 무엇을 시도하거나 어디를 봐야 할지 잘 몰랐습니다. 그 뒤로 이어진 모험 동안 엄청나게 많은 것을 배우게 됐습니다. 결국 예상했던 속도에 도달하긴 했지만, 그 과정에서 헛다리도 많았고 놀라운 일도 많았습니다.

이 프로젝트 이전에도 SMT 솔버의 성능이 악명 높을 정도로 불투명하고 불안정하다는 막연한 인식은 있었습니다. 그럼에도 불구하고 제가 생각했던 꽤 단순한 문제에서도 그 말이 얼마나 사실인지에 스스로 놀랐습니다. 지금도 제가 마주한 여러 동작을 완전히 이해하지 못하고 있습니다.

먼저 가장 큰 영향을 준 두 가지 변경 사항을 공유하겠습니다. 제가 보기엔 빠르고 안정적인 솔버를 만든 변경들입니다. 그 다음에는 헛발질이었던 시도들과 다른 기묘한 현상들을 공유하겠습니다.

상태 가지치기

앞에서 언급했듯 저는 (당시에는) Z3 전문가가 아니었지만, 정규식에 대해서는 꽤 잘 알고 있었습니다. 그래서 제 첫 아이디어는 도메인 특화 분석을 통해 추가 제약을 생성해 Z3를 돕는 것이었습니다.

동기를 부여하는 예로, 지금 이 글을 쓰는 시점의 오늘의 regexle에 나온 정규식 (NR|Q|I)+를 생각해 봅시다. 답에는 N, R, Q, I 글자만 들어갈 수 있다는 것이 즉시 자명합니다. 하지만 제 코드는 모든 칸에 대해 A-Z라는 알파벳을 하드코딩하고, 다른 모든 글자를 배제하는 일을 Z3에 맡깁니다. 실제 가능한 알파벳을 감지해서 Z3 문제에 인코딩하면 어떨까요?

사람이라면 정규식 소스를 보고 그 특성을 쉽게 감지합니다. 코드로도 비슷한 분석을 작성할 수 있겠지만, 일반적으로 문제는 그리 단순하지 않습니다. 하지만 이미 가지고 있는 전이 테이블에 대해 비슷한 분석을 수행할 수 있다는 것을 깨달았습니다. 게다가 저는 이제 과학자이기도 하므로, 몇 줄의 numpy 트릭으로 이를 해보기로 했습니다.

FSM에서 어떤 상태가 “dead” 상태인지는 그 상태에서 어떤 전이 시퀀스를 따라가도 수용 상태에 도달할 수 없는 경우로 정의합니다. greenery의 분석 패스 덕분에 최소화된 FSM에서 작업하므로, dead 상태는 최대 하나뿐이며, 그 상태에서 나가는 모든 간선은 자기 자신으로 돌아오는 셀프 루프라는 것을 알고 있습니다. 그 조건을 찾으면 dead 상태를 쉽게 감지할 수 있습니다:

# Method on the above class `Regex`
@cached_property
def dead_states(self) -> set[int]:
    looped = self.transition == np.arange(self.nstate)[:, None]
    return set(np.flatnonzero(looped.all(-1) & ~self.accept))

(dead 상태는 0개 또는 1개뿐이라는 점에 유의하세요. 하지만 set[int]를 사용하면 두 경우를 집합을 순회함으로써 균일하게 처리할 수 있어, int | None을 쓰는 것보다 조금 더 깔끔하다고 느꼈습니다)

dead 상태가 주어지면, dead 문자는 어떤 시작 상태에서 출발하든 항상 dead 상태로 전이되는 문자로 정의할 수 있습니다:

@cached_property
def dead_vocab(self) -> set[int]:
    dead = set()
    for d in self.dead_states:
        dead |= set(np.flatnonzero((self.transition == d).all(0)))
    return dead

또 주어진 상태에서 시작했을 때 dead가 되는 문자들도 물을 수 있습니다:

def dead_from(self, state: int) -> set[int]:
    dead = set()
    for d in self.dead_states:
        dead |= set(np.flatnonzero((self.transition == d)[state]))
    return dead

이 정보를 갖추면 Z3에 몇 가지 제약을 더 줄 수 있습니다:

for d in pat.dead_vocab:
    for ch in chars:
        solv.add(ch != d)

for d in pat.dead_from(0):
    solv.add(chars[0] != d)

for d in pat.dead_states:
    for st in states:
        solv.add(st != d)

이 제약들은 엄밀히 말하면 중복(redundant)되지만, 우리의 희망은 문제 구조에 대한 우리의 지식이 Z3보다 이러한 사실들을 더 쉽게 찾아내고, Z3가 탐색 공간 중 “흥미로운” 부분에 더 빨리 집중하도록 돕는 것입니다.

실제로 저는 이 가지치기 연습이 Z3 같은 범용 증명기/솔버를 사용하면서도 도메인 특화 휴리스틱으로 성능을 높이는 흥미로운 사례라고 느꼈습니다. 제 느낌으로는 솔버가 마법은 아니며, 도메인 특화 분석을 이용해 추가 구조를 연역할 수 있다면 솔버에 중요한 부스트를 주는 경우가 꽤 흔하다는 것입니다.

원한다면 특정 퍼즐에 대해 이러한 제약이 중복된다는 것을 Z3에 검증하도록 요청하는 것도 비교적 간단할 것이며, 이는 유용한 정확성 검사가 될 것입니다. 이 토이 프로젝트에서는 굳이 그렇게까지 하진 않았습니다.

전이 함수를 명시적으로 정의하기

위에서 각 정규식에 대한 전이 테이블을 Z3 함수로 인코딩하고, 각 (상태, 문자) 쌍에 대한 점별 assertion으로 그 동작을 고정한다고 설명했습니다. 결국 전이를 해석되지 않은 함수 대신 명시적인 식으로 표현하면 더 나은 성능을 얻을 수 있다는 것을 발견했습니다. 그렇게 하면 Z3가 탐색에 의존하기보다 관계를 등식적으로 추론하도록 유도한 것이 아닌가 추측하지만, 솔직히 명확하진 않습니다.

우리는 (상태, 문자) 입력을 분석하는 if-then 사다리 형태로 전이 테이블을 나타내는 파이썬 함수를 작성하겠습니다. 먼저 단일 변수에 대한 “match” 혹은 “switch” 문을 효과적으로 수행하는 헬퍼부터 시작하겠습니다:

def build_match(
    var: z3.AstRef,
    test: list[z3.AstRef],
    result: list[z3.AstRef],
) -> z3.AstRef:
    """Return a Z3 `if` ladder comparing var against each `test` value.

    If `var == test[i]`, the ladder evaluates to `result[i]`. If no
    `test` matches, evaluate to `result[-1]`; it is anticipated that
    normally the list of tests will be exhaustive.
    """
    expr = result[-1]
    for test_, then_ in zip(test[:-1], result[:-1], strict=True):
        expr = z3.If(var == test_, then_, expr)
    return expr

이제 상태와 문자에 해당하는 Z3 식이 주어지면, 새로운 상태를 계산하는 명시적인 식을 만들 수 있습니다:

def build_next_state(
    self, clue: Clue, st: z3.AstRef, ch: z3.AstRef
) -> z3.AstRef:
    pat = clue.pattern
    by_state = [
        build_match(
            ch,
            self.alphabet,
            [self.states[out] for out in pat.transition[i]],
        )
        for i in range(pat.nstate)
    ]

    return build_match(
        st,
        self.states[: pat.nstate],
        by_state,
    )

이제 이전에 state_func(states[i], ch) == states[i + 1] 라고 썼던 곳에, 대신 각 전이에 대한 전체 식을 임베드할 수 있습니다:

for i, ch in enumerate(chars):
    solv.add(self.build_next_state(clue, states[i], ch) == states[i + 1])

이 접근 방식은 상당한 속도 향상을 가져왔고, 특히 성능을 훨씬 더 일관되게 만들었습니다. 퍼즐 크기가 커질수록 기존의 점별 assertion 방식보다 “느린 퍼즐”이 훨씬 적게 나타났습니다.

불행히도 이 직접적인 접근 방식에는 상당한 단점이 있었습니다. 거대한 Z3 if-then 사다리를 구성하는 비용이 엄청나서, 문제를 구성하는 데 걸리는 시간이 실제로 푸는 데 걸리는 시간보다 훨씬 길어졌습니다!

식 공유하기

두 마리 토끼를 모두 잡을 수 있을까요? 꽤 많은 탐색과 실험 끝에 동일한 성능을 얻으면서도 식을 한 번만 구성하는 방법을 찾을 수 있었습니다. 사실 서로 다른 두 가지 전략을 찾았는데, 여러 Z3 기능을 잘 보여줍니다.

Z3 람다 식 사용하기

Z3 함수 객체를 사용하는 대신, 큰 if 사다리를 z3.Lambda 식으로 감싸 명시적으로 인스턴스화하는 방법을 쓸 수 있으며, 이를 통해 서로 다른 파라미터로 여러 번 인스턴스화할 수 있습니다. 위의 build_next_state 함수를 이용하면 아주 작은 변경으로 이를 할 수 있습니다:

st = z3.Int("st")
ch = z3.Int("ch")

lambda_ = z3.Lambda([st, ch], self.build_funcexpr(clue, st, ch))

for i, ch in enumerate(chars):
    solv.add(lambda_[states[i], ch] == states[i + 1])

Z3 함수와 macro-finder 사용하기

다른 옵션을 탐색하던 중, SMT-LIB 명세를 읽다가 SMT-LIB에서 명시적인 본문(body)을 가진 함수를 정의할 수 있다는 점을 알게 됐습니다:

(define-fun double ((x Int)) Int (* x 2))

;; evaluates to `8`
(simplify (double 4))

Z3는 이러한 도구에 대한 접근을 제공하므로, 이를 사용해 봤습니다:

state_expr = self.build_funcexpr(clue, st, ch)
solv.add(z3.ForAll([st, ch], state_func(st, ch) == state_expr))

이 접근 방식은 올바른 해를 생성한다는 점에서는 동작했지만, 제가 시도한 접근 중 가장 느린 것 중 하나였습니다!

하지만 더 많은 탐색 끝에 해결책을 찾았습니다! Z3에는 “macro-finder”라는 이름의 “전술(tactic)”이 있습니다. Z3 전술은 핵심 SMT 솔버 외부에서 사용자가 직접 단순화 혹은 변환 패스를 지시할 수 있게 해주는 변환입니다. macro-finder는 여러 변환을 구현하지만, 가장 기본적으로는 함수의 의미를 “정의”하는 forall assertion을 찾아 그 함수의 호출을 해당 정의로 사실상 복사-붙여넣기 합니다. 본질적으로 우리의 forall 변형을 “매번 명시적 식” 변형으로 변환하지만, C++로 구현되어 Z3 코어에 더 가깝게 동작하므로 매우 효율적으로 수행됩니다.

세 가지 접근 방식(명시적 식, Z3 lambda, 그리고 forall+macro-finder) 모두 Z3에서의 풀이 시간은 비슷했으며, z3.Lambda와 macro-finder 접근 방식 모두 문제를 정의하는 런타임 측면에서도 비슷하게 빨랐습니다.

헛발질

이제 동작하지 않았거나 적어도 필요하지 않았던 것들을 파헤쳐 보겠습니다. 그 과정에서 더 많은 Z3 기능과 놀라운 성능 동작들에 대해 배우게 될 것입니다. 원한다면 제 마무리 생각으로 바로 건너뛰어도 됩니다.

Z3 EnumSort

Z3는 정수에 대해 많은 것을 알고 있으며, 서로 다른 정수 산술 조각들에 대해 많은 서로 다른 솔버를 가지고 있습니다. 궁금했습니다. 다른 데이터 타입을 사용해 정수 로직을 전혀 호출하지 않으면 솔버 속도를 높일 수 있을까요?

그래서 상태와 문자를 SMT-LIB 열거 타입(파이썬에서는 z3.EnumSort로 노출됨)으로 교체해 봤습니다.

상태와 문자에 대한 열거 sort를 정의해, 정확히 N개의 서로 다른 값만 가지는 것 외에는 아무런 동작도 없는 새로운 타입을 만들 수 있습니다:

nstates = max(c.pattern.nstate for c in all_clues)
state_sort, states = z3.EnumSort(
    "State",
    [f"S{i}" for i in range(nstates)],
)

char_sort, alphabet = z3.EnumSort("Char", list(ALPHABET))

나머지 코드도 최소한만 바뀝니다. 전이 함수의 선언에서 IntSort를 교체하고, 특정 상태나 문자를 인코딩할 때마다 i 대신 states[i]나 alphabet[i]로 교체하면 됩니다.

EnumSort 성능

처음 EnumSort로 바꿨을 때 엄청난 속도 향상을 봤습니다!

하지만 제가 그 속도 향상의 이유를 최소한 부분적으로는 잘못 짚었다는 것이 드러났습니다. 같은 플롯에 두 개의 새로운 패널을 추가했습니다. 하나는 여전히 점별 함수 정의를 사용하지만 잠시 후에 언급할 작은 변경을 가한 것이고, 다른 하나는 위에서 설명한 z3.Lambda 인코딩을 사용한 것입니다:

현재 코드에서는 점별 함수 정의에서 IntSort가 더 빠르며, 전이 함수를 명시적으로 인코딩했을 때의 속도 향상이 다른 어떤 변경보다도 큽니다.

기묘한 성능 불안정성

“(old)”와 “(new)” 사이에 무엇을 바꿨을까요?

정수를 이용해 상태를 표현할 때 추가 assertion으로 정수에 경계를 둡니다. 위에서 제가 처음 작성한 경계 코드입니다:

# Each state must be valid
for st in states:
    solv.add(0 <= st)
    solv.add(st < pat.nstate)

다른 표현을 실험하기 위해 코드를 리팩터링하던 중, 실수로 동작을 현재 단서만을 위한 경계가 아니라 모든 단서에 대한 최대 상태 수를 이용해 상태를 제한하도록 바꿔버렸습니다:

max_nstate = max(clue.pattern.nstate for clue in all_clues)

for st in states:
    solv.add(0 <= st)
    solv.add(st < max_nstate)

적어도 제 버전의 Z3에서는 두 번째 접근 방식, 즉 더 느슨한 경계가 훨씬 더 빠릅니다! 이 변경이 IntSort 플롯에서 “(old)”와 “(new)” 사이의 유일하게 의미 있는 차이라고 생각합니다!

게다가 점별 함수 정의에서 EnumSort가 왜 더 느린지도 실제로 이해하지 못했습니다. Z3 트레이스와 통계를 살펴보니, Enum 경우에 Z3가 xfer(st, ch) == st_next assertion을 통해 등식적으로 추론하는 데 어떻게든 어려움을 겪어 약간의 탐색과 백트래킹이 더 필요한 것처럼 보이지만, 왜 그런지는 모르겠습니다.

Z3 정규식 사용하기

표현의 전체 행렬을 지원하도록 리팩터링하고, 프로파일링하고 플롯을 만드는 와중에, 문제를 해결하는 완전히 다른 접근 방식도 시도해 봤습니다!

알고 보니 Z3는 정규식 이론도 지원합니다! 상태 기계 장치를 완전히 우회하고, 정규식 단서를 Z3 정규식으로 직접 인코딩할 수 있습니다.

Z3에는 정규식 파서가 함께 제공되지 않지만, 대신 z3.Re(char), z3.Range(start, end), z3.Star(re) 등과 같은 패턴을 구성하는 콤비네이터가 있습니다. 그래서 간단한 변환 레이어를 작성해 greenery Pattern AST를 재귀적으로 순회하며 Z3 정규식으로 변환했습니다. 거기서부터 각 미지의 문자를 Z3 문자열 객체로 선언하고, 각 단서를 다음과 같이 assert하면 됩니다:

re = greenery_to_z3(clue.pattern)

string = z3.Concat(chars)
solv.add(z3.InRe(string, re))

따지고 보면 훨씬 더 간단합니다! 빠를까요? … 그럭저럭 괜찮습니다.

한편으로, 특히 큰 퍼즐에서는 이 글에서 논의한 모든 트릭을 동원하면 훨씬 더 빠르게 퍼즐을 풀 수 있습니다. 다른 한편으로, Z3 정규식을 사용하는 솔버는 제가 고려하거나 구현한 것 중 단연 가장 단순하며, 저의 초기 순진한 시도보다 거의 10배 빠릅니다.

패턴이 일반화된다고 생각합니다. Z3가 여러분의 문제 도메인에 대해 일급 지원을 제공한다면, 거기서 시작하는 것이 좋습니다! 하지만 Z3는 무엇보다도 매우 범용적인 도구이며 많은 서로 다른 문제 유형에 대해 균일한 인터페이스를 제공하는 것이 가장 큰 장점입니다. 노력을 투자하고, 실험하고, 도메인 특화 전문성을 발휘할 의지가 있다면, 여러분 쪽의 복잡성을 추가하는 대가로 인스턴스를 더 빠르게 풀 가능성이 높습니다.

결론

재밌는 프로젝트였습니다! 원래는 재미로 하는 nerdsniping으로 오후 한때 즐길 생각이었는데, 실제로 초기 스크립트는 한두 시간 만에 뚝딱 만들었습니다. 하지만 최적화하고 Z3를 더 이해하고 싶은 욕구를 떨칠 수 없었고, 그 이후로 리팩터링하고, 변형을 탐색하고, 벤치마크를 돌리고, 플롯을 만들고 하는 데 다소 과한 시간을 썼습니다. 하지만 그렇게 하면서 Z3와 SMT-LIB에 대해 훨씬, 훨씬 더 잘 이해하게 됐으니, 결국 그게 원래 목표였죠! 앞으로 Z3를 “실전”에 배치할 더 많은 기회를 찾고 싶습니다.

Z3를 다루면서 얻은 몇 가지 성찰/교훈으로 마무리하겠습니다.

Z3는 내가 생각했던 것보다 훨씬 더 많은 기능을 지원한다.

저는 지금까지 Z3를 정수, 비트 벡터, 그리고 때때로 배열을 포함하는 문제를 위한 솔버로 스치듯 접해왔습니다. Z3가 지원하는 많은 새로운 데이터 타입과 이론에 대해 배웠는데, 여기에는 다음이 포함됩니다:

• 문자열, 시퀀스, 정규식
• 대수적 데이터 타입
• 해석되지 않은 함수, 재귀 함수 포함

Z3 전술(tactics) 시스템도 처음 접했는데, 이는 기반 SMT 솔버의 범위를 넘어서는 문제를 해결하는 데에도, 특정 클래스의 문제에 최적화하기 위해 커스텀 재작성/단순화 전략을 구현하는 데에도 사용할 수 있습니다. 제가 가장 좋아하는 Z3 기반 도구인 Alive2가 Alive2가 생성하는 특정 종류의 식에 최적화하기 위해 Z3 전술을 많이 사용한다는 것을 알게 됐습니다.

Z3 성능은 확실히 때때로 꽤 불안정하고 예측 불가능하다.

앞서 언급했듯이, 이 특성에 대해 어렴풋이 들어서 알고는 있었지만, 이 프로젝트를 통해 정말 체감이 됐습니다. 이 문제에 대해 제가 고안한 인코딩과 접근 방식의 다양한 조합을 조정함으로써, 도메인 특화 가지치기 최적화는 차치하고도 솔버를 100배 더 빠르거나 느리게 만들 수 있었습니다. 그리고 일부 성능 동작은 당혹스러웠는데, 예를 들어 정수 범위 경계를 약간 느슨하게 하는 것만으로 10배 속도 향상을 얻은 경우가 그렇습니다!

더 예측 가능한 성능을 위해 Z3 열거형을 사용하세요

성능에 관한 약간의 전술적/구체적인 조언입니다.

Z3에 “N가지 가능성 중 하나”를 나타내고 싶은 문제를 인코딩하는데, 그 가능성들이 자연스러운 수학적 해석을 갖지 않는 경우(예를 들어 정수로 취급해 합산하는 경우가 아니라면), 정수를 이용해 레이블을 붙이는 대신 새로운 열거 sort를 선언하는 것을 제안합니다.

제 경험에 비추어 보면 이 변경이 종종 아무런 차이를 만들지 않지만, 때때로 모든 산술 및 숫자의 다른 특성에 대한 Z3의 전문화된 지식과 솔버를 우회함으로써 불가사의한 성능 불안정성과 10배의 속도 저하를 피할 수 있습니다.

다만 사용성 측면에서의 한 가지 주의사항이 있습니다. 새로운 sort는 Z3 Context당 전역이므로, 예를 들어 “State”라는 이름의 EnumSort를 선언했다면, 프로그램을 재시작하거나 완전히 새로운 context 객체를 생성하지 않고는 같은 이름에 다른 값 집합을 가진 다른 sort를 재선언할 수 없습니다.

Z3 문서는 혼재되어 있지만, 존재는 한다

처음에는 Z3 내부나 전략, 표면적인 사용법을 넘어서는 깊은 질문에 답해주는 좋은 문서를 찾기가 꽤 어려웠지만, 결국 꽤 많은 목록을 모았습니다. “전문가에게 물어보기”가 여전히 Z3를 사용하는 가장 효과적인 방법이라고 생각합니다(이 프로젝트를 진행하면서 질문에 답해준 Hillel Wayne에게 감사드립니다!). 하지만 제가 찾은 다른 훌륭한 링크들은 다음과 같습니다:

• Microsoft의 Z3 Guide. 전술 목록과 솔버 옵션을 포함합니다.
• Programming Z3, Z3 개발자들이 쓴 논문.
• Z3 Internals는 Z3가 내부적으로 어떻게 동작하는지에 대한 훌륭한 세부 정보를 담고 있습니다.