On Solving String Equations via Powers and Parikh Images

이 논문은 문자열을 위한 거듭제곱 연산자, 일반화된 파라키 이미지, 그리고 등식 분해 기법을 니켈 변환의 확장으로 결합하여 복잡한 문자열 방정식 및 SMT 입력을 해결하는 새로운 접근법을 제시합니다.

핵심

1. 문제 상황: 거대한 레고 성의 방정식

상상해 보세요. 두 개의 거대한 레고 성이 있습니다.

• 왼쪽 성: "A 레고 3 개 + B 레고 + C 레고..."
• 오른쪽 성: "C 레고 5 개 + D 레고 + D 레고..."

이 두 성이 완전히 똑같아야 한다 (방정식) 고 가정합니다. 여기서 문제는 레고 조각들이 **알 수 없는 변수 (x, y, z)**로 되어 있다는 점입니다. "x 는 몇 개의 레고로 만들어져야 왼쪽과 오른쪽이 같아질까?"를 찾아내는 게 목표입니다.

기존 컴퓨터 프로그램들은 이 변수들이 서로 얽혀 있거나 (x 가 x 에 의존함), 같은 패턴이 수천 번 반복될 때 (x 가 'aaaaa...'처럼 길어질 때) 머리가 아파서 포기하거나 너무 느리게 작동했습니다.

2. 해결책: 세 가지 마법 도구

이 논문은 이 난제를 해결하기 위해 세 가지 강력한 도구를 합쳤습니다.

① '압축 마법' (Powers / Powers Operator)

비유: "수천 개의 같은 레고 블록을 '1 개의 압축된 상자'로 바꾸기"

만약 방정식 속에 x 가 aaaaa... (a 가 1000 개) 처럼 반복된다면, 컴퓨터는 하나하나 세느라 지칩니다.
이 연구는 **"이건 그냥 a 가 1000 번 반복된 거야"**라고 표시하는 지수 (Power) 개념을 도입했습니다.

• 기존: 레고 1000 개를 하나하나 비교.
• 새로운 방법: "이건 a 의 1000 제곱 (a^1000) 이야"라고 한 번에 처리.
  이렇게 하면 길이가 아무리 길어도 컴퓨터가 순식간에 "아, 이건 반복되는 패턴이구나"라고 파악할 수 있어 속도가 빨라집니다.

② '자르기 마법' (Equality Decomposition)

비유: "긴 줄을 길이에 맞춰 정확하게 자르기"

두 줄의 문자열 길이가 다를 때, 어떻게 같아질 수 있을까요? 예를 들어, 왼쪽은 A + B이고 오른쪽은 B + C라면, A와 C가 같아야 합니다.
하지만 더 복잡한 경우, A + B + C와 B + C + D처럼 길이가 다를 수 있습니다. 이때는 길이를 계산해서 긴 쪽에서 짧은 쪽만큼 잘라내야 합니다.

• 방법: "왼쪽이 오른쪽보다 3 칸 더 길어. 그럼 왼쪽의 앞 3 칸을 잘라내서 '미지의 문자 (o)'로 표시하고, 나머지를 비교하자."
  이렇게 방정식을 잘게 쪼개면 (Decomposition), 복잡한 문제를 단순한 조각들로 나누어 쉽게 풀 수 있습니다.

③ '빈도수 분석 마법' (Parikh Images)

비유: "레고 색상의 개수만 세어보기 (위치 무시)"

때로는 두 성의 모양이 너무 복잡해서 하나하나 비교하는 게 불가능할 때가 있습니다. 이때는 색상만 세어보는 전략을 씁니다.

• 전략: "왼쪽 성에는 빨간 레고가 5 개, 파란 레고가 3 개야. 오른쪽 성에는 빨간 레고가 2 개, 파란 레고가 3 개야."
• 결과: "빨간 레고 개수가 다르잖아! 그럼 이 두 성은 절대 같을 수 없어!"
  기존 방법들은 '색상 개수'만 세는 단순한 방식이라 놓치는 경우가 많았지만, 이 연구는 색상 순서와 위치까지 고려한 더 정교한 분석을 통해 "아, 이 조합은 절대 불가능해!"라고 빠르게 결론 내릴 수 있게 했습니다.

---

3. 실제 효과: ZIPT 라는 새로운 로봇

저희는 이 세 가지 마법을 합쳐 ZIPT라는 새로운 프로그램 (프로토타입) 을 만들었습니다.

• 기존 프로그램 (Z3, cvc5 등): 복잡한 반복문이나 서로 얽힌 변수가 나오면 "도저히 못 풀겠어"라고 포기하거나 시간이 너무 오래 걸렸습니다.
• ZIPT: 위의 세 가지 마법을 써서, 기존에 풀지 못했던 난이도 높은 문제들도 빠르게 해결했습니다. 특히 레고 (문자열) 가 기하급수적으로 늘어나는 문제에서도 압도적인 성능을 보여줬습니다.

4. 요약: 왜 이 연구가 중요할까요?

소프트웨어가 해킹당하거나, 중요한 데이터가 유출되는 것을 막기 위해선 컴퓨터가 복잡한 규칙을 정확히 이해해야 합니다.
이 연구는 **"컴퓨터가 복잡한 문자열 규칙을 이해할 때, 단순히 하나하나 비교하는 게 아니라, 패턴을 압축하고, 잘게 나누고, 색상 (빈도) 을 분석하는 똑똑한 방법"**을 제시했습니다.

결국, 더 안전하고 빠른 소프트웨어를 만드는 데 필수적인 '논리 엔진'을 업그레이드한 셈입니다. 마치 복잡한 미로를 풀 때, 하나하나 길을 찾는 대신 지도를 보고 shortcuts(단축로) 를 찾아내는 것과 같습니다.

기술 요약

이 논문은 **"파워 (Powers) 와 파라키 이미지 (Parikh Images) 를 통한 문자열 방정식 해결"**이라는 주제로, 기존 SMT(Satisfiability Modulo Theories) 솔버가 처리하기 어려운 복잡한 문자열 방정식을 해결하기 위한 새로운 접근법을 제시합니다.

주요 내용은 다음과 같습니다.

1. 문제 정의 (Problem)

현대적인 SMT 솔버 (Z3, cvc5 등) 는 길이 제약, 정규 표현식, 포함 관계 등을 처리할 수 있지만, 긴 반복된 부분 문자열이나 상호 의존적인 문자열 변수가 포함된 방정식을 해결하는 데에는 여전히 한계가 있습니다.

• 예시: $x^3 x^3 x^4 b x^5 b \simeq x^5 x^5 x^5 x^5 x^4 bb$ 와 같은 방정식이나, 변수들이 서로를 참조하거나 자기 자신을 참조하는 ($x = axb$ 형태) 복잡한 구조는 기존 기술로는 해결이 어렵거나 비효율적입니다.
• 기존 방법론은 이러한 경우 무한한 분해 과정을 겪거나, 불만족 (unsatisfiable) 인 경우를 감지하지 못해 실패합니다.

2. 방법론 (Methodology)

저자들은 **니켈슨 변환 (Nielsen Transformations)**을 기반으로 하되, 이를 세 가지 핵심 기법으로 확장하여 해결 워크플로우를 구축했습니다.

A. 니켈슨 그래프 확장 (Nielsen Graph Expansion)

문자열 방정식의 만족 여부를 결정하기 위해 니켈슨 그래프를 사용합니다.

• 각 노드는 문자열 방정식 집합과 정수 부등식 집합으로 구성됩니다.
• **생성 규칙 (Generating Rules)**과 **재작성 규칙 (Rewriting Rules)**을 적용하여 노드를 분기하거나 단순화합니다.
• 이 과정은 재귀적으로 수행되며, 만족 가능한 노드를 찾거나 모든 경로가 모순임을 증명하여 종료합니다.

B. 세 가지 핵심 확장 기법

1. 등식 분해 (Equality Decomposition):

   • 기존 방법은 방정식의 첫 번째 토큰 (token) 만을 비교할 수 있었으나, 이 기법은 **패딩 (padding)**을 사용하여 방정식을 더 작은 부분 방정식으로 분해합니다.
   • 양변의 길이를 계산하여 차이가 나는 만큼 새로운 심볼릭 문자 (symbolic character) 를 추가하고, 이를 통해 방정식을 $u_1 \simeq v_1$과 $u_2 \simeq v_2$ 형태로 분할합니다. 이는 니켈슨 규칙을 적용할 수 있는 위치를 넓혀줍니다.

2. 명시적 파워 표현 (Explicit Power Representation):

   • 긴 반복 문자열 (예: $x = a^m$) 을 처리하기 위해 **파워 토큰 ($u^m$)**을 도입합니다.
   • 변수 $x$가 $x = axb$와 같은 자기 참조 구조를 가질 때, 무한한 분해 대신 $x = (w_1 w_2)^m w_1$과 같은 일반해 형태로 직접 치환하여 문제를 축소합니다.
   • 이를 통해 무한한 분기 (branching) 를 방지하고, 긴 반복 패턴을 효율적으로 처리합니다.

3. 일반화된 파라키 이미지 (Generalized Parikh Images):

   • 기존 파라키 이미지는 개별 문자의 등장 횟수만 고려하여 불만족을 판별했으나, 이 논문은 문자 시퀀스 (패턴) 단위로 확장합니다.
   • **경계 없는 패턴 (Unbordered Patterns)**을 정의하고, 문자열 내에서의 상대적 위치 정보를 유지하면서 상/하한 추정을 수행합니다.
   • 이를 통해 단순한 문자 개수 비교로는 감지하지 못하는 모순 (예: $xaxaabbby \simeq xyabababx$) 을 효과적으로 발견합니다.

3. 주요 기여 (Key Contributions)

• 새로운 알고리즘 프레임워크: 니켈슨 변환에 등식 분해, 파워 도입, 일반화된 파라키 이미지를 통합한 새로운 문자열 솔빙 프레임워크를 제안했습니다.
• 복잡한 의존성 해결: 자기 참조 변수와 상호 의존 변수가 포함된 방정식을 효율적으로 해결할 수 있는 메커니즘을 제공했습니다.
• 불만족성 증명 강화: 단순한 문자 카운팅을 넘어 패턴 기반의 파라키 이미지를 사용하여 기존 솔버가 놓치던 불만족 사례를 탐지합니다.
• ZIPT 프로토타입 구현: Z3 솔버의 사용자 전파 (user-propagation) 프레임워크를 활용하여 프로토타입 ZIPT를 구현했습니다.

4. 실험 결과 (Results)

• 벤치마크: SMT-LIB 의 woorpje 벤치마크 세트 (QF_S 트랙, 총 409 개 문제) 를 사용하여 평가했습니다.
• 성능 비교: Z3, cvc5, OSTRICH, Z3-Noodler, Z3str3 등 최신 솔버들과 비교했습니다.
  • Track 01, 04: 거의 모든 문제를 해결하여 기존 솔버들과 유사하거나 더 나은 성능을 보였습니다.
  • Track 02 (중요): 이 트랙은 지수적으로 큰 모델을 가진 문제들로 구성되어 있습니다. ZIPT 는 파워 도입 (Power Introduction) 기법 덕분에 다른 솔버들이 실패하거나 시간 초과를 겪는 문제를 성공적으로 해결했습니다. (예: 200 개 문제 중 200 개 해결, cvc5 는 191 개, OSTRICH 는 198 개 등)
  • Track 03: 195 개 문제를 해결하여 기존 솔버들보다 우수한 성능을 입증했습니다.
• 결론: 특히 반복 구조와 자기 의존성이 강한 문제에서 ZIPT 가 압도적인 우위를 보였습니다.

5. 의의 및 결론 (Significance)

이 논문은 문자열 방정식 해결 분야에서 다음과 같은 의의를 가집니다:

1. 이론적 확장: 니켈슨 변환에 현대적인 기법 (파워, 파라키 이미지) 을 성공적으로 통합하여 이론적 한계를 확장했습니다.
2. 실용적 가치: 실제 보안 분석 및 형식 검증에서 발생할 수 있는 복잡한 문자열 제약 조건을 해결할 수 있는 강력한 도구를 제공합니다.
3. 효율성: 무한한 분해 과정을 피하고 파워 토큰을 통해 문제를 압축함으로써, 기존 솔버가 처리하지 못했던 지수적 복잡도 문제를 다룰 수 있게 되었습니다.

저자들은 향후 파라키 이미지 분석을 더 정교하게 다듬고, 정규 표현식 등 SMT-LIB 표준의 다른 문자열 함수들을 지원하여 범위를 확장할 계획이라고 밝혔습니다.