Rust 바인딩으로 z3 SMT 솔버를 가볍게 익혀 보며, 1차 방정식, 다변수, 여러 해 찾기, 최적화(동전 거스름돈), push/pop, 스도쿠, 간단한 페이지 레이아웃까지 예제로 소개합니다. Sort(타입), 상수, SMT-LIB2 같은 기본 용어도 함께 다룹니다.
최근에 재미있는 글을 하나 봤다: Many Hard Leetcode Problems are Easy Constraint Problems. 그래서 생각했다. 나도 이런 걸 배워야겠다! 딱히 다른 할 일도 없고. 예전 글에서도 솔버(흔히 정리 증명기라고 부르는 것들)가 필요했었는데, 그땐 착실한 알고리즘으로 증명하려 했다. 당시에도 z3를 슬쩍 보긴 했지만, 개념이 너무 불투명해서 포기했다. 그런데 이제 보니 조금은 쉽게 다가갈 수 있을 것 같다.
명확히 해두자. 이 글을 쓰는 시점에서 나는 z3 관련 글을 고작 이틀 읽었을 뿐이다. 전문가가 전혀 아니며, 위 글의 첫 번째 예제인 거스름돈 문제 정도보다 복잡한 건 아직 안 만들어봤다. 그러니 이 글은 바닥 지식도 거의 없고, 정리 증명기 이론도 모르고, “unification(통일화)”가 뭔지도 모르는 상태에서 쓰는 글이다. 아마 당신이 나보다 더 많이 알 가능성이 크다.
z3는 여러 인기 언어용 바인딩을 제공한다. 나는 z3의 Rust 바인딩을 사용할 것이다. 파이썬이나 자바스크립트보다 러스트가 더 편해서다. 다만 내가 z3를 이해하려고 참고한 예제는 두 문서에 잘 정리되어 있다.
솔버는 일종의 … 도구? 라이브러리? 로, 규칙과 제약을 집어넣으면 도구가 그냥 … 해결해준다. 수작업으로 만든 맞춤 알고리즘보다 빠르거나 최적화되어 있지는 않겠지만, 규칙을 즉석에서 바꾸며 시도하기가 훨씬 쉽다.
현실의 다양한 문제에 쓰인다. 대표적으로 스케줄링과 자원 배분 문제. 예를 들어 학교 시간표를 생각해 보자: 메리는 아버지를 돌봐야 해서 화요일엔 일할 수 없다; 존은 멀리 살아서 10시 이전엔 수업을 할 수 없다; 3-A 반은 너드라서 수학 시간이 두 배다; 시의 규정상 12시 이후 야외 활동 금지; 수잔과 사라는 서로 싫어하니 같은 반을 맡기지 말 것; 등등. 선생 둘에게 일주일 동안 맡길 수도 있지만, 솔버에 던져도 된다!
MiniZinc 홈페이지에는 좋은 예제가 여럿 있다: 좌석 배치, 근무표, 차량 경로, 격자 색칠.
그런데 왜 시작 글에서 언급된 MiniZinc가 아니라 z3를 골랐냐고? 홈페이지도 MiniZinc가 더 화려하고, 심지어 그 글에서도 MiniZinc를 언급했는데. 답은 간단하다. z3에는 Rust 바인딩이 있다. 정말 그게 전부다.
z3와 그 API 문서를 보면 전문 용어가 엄청 나온다. 배경지식 없이는 정말 진입 장벽이 높다. 개념이 등장할 때마다 내가 이해한 대로 설명하겠지만, 특히 두 가지가 눈에 띈다.
첫째는 Sort. 배열이나 함수 선언(이건 뒤에 다룬다)에서 보게 되는데, 정렬(sorting)과는 1도 관련 없다. Sort는 그냥 _타입_을 뜻하는 은어다.
둘째는 상수(constants). 일반인이 생각하는 상수와 다르다. 솔버가 문제를 풀 때 돌리는 손잡이(노브) 같은 것들이다. 상수에는 두 가지가 있는데: free 상수는 보통 우리가 말하는 변수에 해당한다. interpreted 상수는 정수 리터럴을 타이핑하면 타입 마법으로 솔버의 상수로 해석되는 경우다.
또한 솔버는 프로그래밍 언어의 일반적인 타입 시스템 안에서 동작하지 않는다. 자체 타입(미안, sort)과 연산을 가지고 있으며, 이게 언어의 타입과 연산에 곱게 매핑될 수도 있고 아닐 수도 있다. 실제로 우리가 쓰는 코드의 상당 부분은 목표 솔버의 언어로 표현하는 일이다. z3는 “SMT-LIB2”(이하 smt2)라는 언어를 쓴다. 제약을 이 언어로 직접 적어서 라이브러리에 넣을 수도 있다. 바인딩이 하는 일의 상당 부분은 당신의 코드를 이 언어로 내부 변환해서 솔버에 먹이는 것이다.2
가장 단순하고 멍청한 방정식부터 시작해 보자. x를 구하라:
x + 4 = 7
그래, 아이(정말로)도 풀 수 있다. 그래도 예쁘지 않나. 이걸 푸는 러스트 프로그램은 다음과 같다.
use z3::{Solver, ast::Int};
fn main() {
let solver = Solver::new();
// 변수를 정의한다.
let x = Int::new_const("x");
// 식을 정의한다
solver.assert((&x + 4).eq(7));
// 솔버 실행
_ = solver.check();
let model = solver.get_model().unwrap();
println!("{model:?}");
}
해를 출력한다. x는 3이다. 누가 예상이나 했겠나?
x -> 3
러스트 바인딩은 이런 부분의 인체공학이 꽤 좋다. 그냥 &x + 4라고 쓰면, 내부적으로 알아서 4(그리고 7)를 해석된 상수로 바꾸고 내부 모델에 넣는다.
new_const에 문자열을 넘기는 이유는, 그게 smt2에서 변수 이름으로 쓰이기 때문이다. 꼭 "x"일 필요는 없고 아무거나 가능하다. 바인딩이 왜 자동으로 이름을 만들어주지 않는지는 모르겠다.
솔버 자체를 출력하면(예: println!("{solver:?}");) 다음과 같은 smt2 출력이 나온다.
(declare-fun x () Int)
(assert (= (+ x 4) 7))
선언한 변수가 _함수_로 선언되었다는 점에 주목하자. free 상수는 본질적으로 입력이 없고 출력만 있는 함수다(여기서는 타입 sort가 Int). 솔버는 이 함수의 어떤 값이 주어진 assert들을 만족하는지 찾는다. 그래서 아까 x -> 3에서 화살표가 나온다. x가 3으로 평가된다.
학교에서 1개의 미지수에서 2개의 미지수로 넘어가면 체감 난이도가 훅 올라간다. 모든 게 두 배가 된 느낌! 다음의 연립방정식을 풀어보자.
x + y = 17
y = 2 * x
프로그램은 다음과 같다. solver.check()의 결과를 먼저 출력해 보겠다. 숫자는 그냥 내가 아무렇게나 정했다!
use z3::{Solver, ast::Int};
fn main() {
let solver = Solver::new();
// 변수를 정의한다.
let x = Int::new_const("x");
let y = Int::new_const("y");
// 식을 정의한다
solver.assert((&x + &y).eq(17));
solver.assert((&x * 2).eq(&y));
println!("{solver:?}");
let c = solver.check();
println!("; {c:?}");
}
출력은 다음과 같다.
(declare-fun y () Int)
(declare-fun x () Int)
(assert (= (+ x y) 17))
(assert (= (* x 2) y))
; Unsat
오, Unsat다. 만족 불가능. 망했다. 즉, 정의한 대로는 풀 수 없다는 뜻.
Real3 타입으로 바꿔보자. Real은 Int처럼 예쁜 문법 설탕이 없는 것 같아서 코드가 약간 못생겨진다. 바꾼 코드는 이렇다.
use z3::{Solver, ast::Real};
fn main() {
let solver = Solver::new();
// 변수를 정의한다.
let x = Real::new_const("x");
let y = Real::new_const("y");
let seventeen = Real::from_rational(17, 1);
let two = Real::from_rational(2, 1);
// 식을 정의한다
solver.assert((&x + &y).eq(&seventeen));
solver.assert((&x * &two).eq(&y));
println!("{solver:?}");
let c = solver.check();
println!("; {c:?}");
}
출력은 다음과 같다.
(declare-fun y () Real)
(declare-fun x () Real)
(assert (= (+ x y) 17.0))
(assert (= (* x 2.0) y))
; Sat
아주 좋다! 이전처럼 get_model()로 모델을 찍으면, 보기 좋은 유리수 형태의 답을 준다.
y -> (/ 34.0 3.0)
x -> (/ 17.0 3.0)
디버그 출력 대신 실제 값을 코드에서 뽑아내려면 API와 약간의 댄스가 필요하지만, 사실 간단하다. 대략 이렇게 쓴다.
// 만족 불가능 시 패닉 피하기 위해
if let z3::SatResult::Sat = solver.check() {
let model = solver.get_model().unwrap();
// `true`가 뭔지는 묻지 말자. 나도 모른다.
let x = model.eval(&x, true).unwrap().approx_f64();
let y = model.eval(&y, true).unwrap().approx_f64();
println!("x: {x:.3}\ty: {y:.3}");
}
출력은 다음과 같다.
x: 5.667 y: 11.333
좋다. 멋지지 않은가?
고등학교 수학에서 알다시피, 어떤 방정식은 해가 여러 개다. 아주 쉬운 예를 보자.
x * x = 4
러스트 바인딩에는 솔버에서 여러 해를 뽑아내는 간편한 메서드 solutions가 있다. 위의 model.eval()처럼 동작하며 같은 파라미터/출력을 가진다. 전체 코드는 다음과 같다. (나는 Real 숫자를 다룰 깜냥이 못 되니 다시 Int로 돌아간다.)
use z3::{Solver, ast::Int};
fn main() {
let solver = Solver::new();
let x = Int::new_const("x");
solver.assert((&x * &x).eq(4));
println!("{solver:?}");
// `check`가 `Sat`가 아니게 되면 순회 종료
for (idx, s) in solver.solutions(x, true).enumerate() {
let s = s.as_i64().unwrap();
println!(";{}:\t{s}", idx + 1);
}
}
출력은 다음과 같다.
(declare-fun x () Int)
(assert (= (* x x) 4))
;1: -2
;2: 2
일반적인 check 다음에 get_model을 써서 여러 해를 얻는 방법은 사실 잘 모르겠다. 그래도 solutions가 충분히 쓰기 쉽다. 또한 어떤 문제는 해가 무한히 많을 수 있으니, solutions 이터레이터에는 take를 붙여 쓰는 게 좋다. 예시로 원 방정식을 써보자.
x * x + y * y = 25
아래는 단순한 스크립트와 그 출력이다. fresh_const API는 호출할 때마다 유니크한 이름을 만들어 준다.
use z3::{Solver, ast::Int};
fn main() {
let solver = Solver::new();
let x = Int::fresh_const("x");
let y = Int::fresh_const("x");
let area = &x * &x + &y * &y;
solver.assert(area.eq(25));
println!("{solver:?}");
for (idx, (x,y)) in solver.solutions((x,y), true).enumerate() {
let x = x.as_i64().unwrap();
let y = y.as_i64().unwrap();
println!("; {}:\t{x:>2},{y:?2} ", idx + 1);
}
}
(declare-fun x!1 () Int)
(declare-fun x!0 () Int)
(assert (= (+ (* x!0 x!0) (* x!1 x!1)) 25))
; 1: 0, 5
; 2: -5, 0
; 3: -3,-4
; 4: -4,-3
; 5: 0,-5
; 6: 3,-4
; 7: 4,-3
; 8: 5, 0
; 9: 3, 4
; 10: 4, 3
; 11: -3, 4
; 12: -4, 3
말할 필요도 없지만, 여기서 Real 타입을 썼다면 해가 무한히 나오게 될 것이다.
동전 거스름돈 문제는 단순하다. 주어진 액면가 목록과 총액이 있을 때, 그 총액을 만드는 동전 개수의 _최솟값_을 구하라. 이전 문제들과 달리 이건 최적화 문제다. 특정 조건을 만족하는 어떤 해가 아니라, 그중 최적인 해를 찾는다. 마침 z3에는 최적화를 위한 Optimize 객체가 있다.
문제를 평범한 말로 설정해 보자. 액면가는 1, 5, 10. 총 37을 가장 적은 동전으로 만들어야 한다. 이건 사람이 봐도 바로 답이 보인다: 10 세 개, 5 하나, 1 두 개. 같은 결과를 얻을 수 있을까? 늘 그렇듯 코드와 출력부터 보자.
use z3::{Optimize, ast::Int};
fn main() {
let opt = Optimize::new();
let c1 = Int::new_const("c1");
let c5 = Int::new_const("c5");
let c10 = Int::new_const("c10");
let total = (&c1 * 1) + (&c5 * 5) + (&c10 * 10);
let count = &c1 + &c5 + &c10;
opt.assert(&total.eq(37));
opt.minimize(&count);
println!("{opt:?}");
if let z3::SatResult::Sat = opt.check(&[]) {
let model = opt.get_model().unwrap();
let c1 = model.eval(&c1, true).unwrap();
let c5 = model.eval(&c5, true).unwrap();
let c10 = model.eval(&c10, true).unwrap();
println!("; c1: {c1:?}, c5: {c5:?}, c10: {c10:?}");
} else {
println!("; woe for us");
}
}
(declare-fun c10 () Int)
(declare-fun c5 () Int)
(declare-fun c1 () Int)
(assert (= (+ (* c1 1) (* c5 5) (* c10 10)) 37))
(minimize (+ c1 c5 c10))
(check-sat)
; c1: 37, c5: 0, c10: 0
어라. 이건 아니다.
왜 답이 이런 식으로 엉망이 되는지 사실 잘 모르겠다. 문제는 Int가 정수 전 범위를 포함해서, 동전 개수가 음수가 될 수도 있다고 여기는 데 있다. 그래도 최적해가 왜 37개인지(즉 1원짜리만 37개인지)는 설명이 되지 않는다. (설명 가능하신 분, 제보 부탁드립니다.)
이 문제의 해결책은 동전 개수를 음이 아닌 값으로 제한하는 것이다. 그러자. check 전에 아래 assert들을 추가하면 된다.
opt.assert(&c1.ge(0));
opt.assert(&c5.ge(0));
opt.assert(&c10.ge(0));
(declare-fun c1 () Int)
(declare-fun c5 () Int)
(declare-fun c10 () Int)
(assert (>= c1 0))
(assert (>= c5 0))
(assert (>= c10 0))
(assert (= (+ (* c1 1) (* c5 5) (* c10 10)) 37))
(minimize (+ c1 c5 c10))
(check-sat)
; c1: 2, c5: 1, c10: 3
이제서야 제대로다. 다른 액면가로도 해보자. 10, 9, 1 같은 조합. 37의 최적해는: 10 하나, 9 세 개, 1 없음. 탐욕적 해법은 이걸 놓친다. 최적화기와 결과를 출력해 보자.
(declare-fun c1 () Int)
(declare-fun c9 () Int)
(declare-fun c10 () Int)
(assert (>= c1 0))
(assert (>= c9 0))
(assert (>= c10 0))
(assert (= (+ (* c1 1) (* c9 9) (* c10 10)) 37))
(minimize (+ c1 c9 c10))
(check-sat)
; c1: 0, c9: 3, c10: 1
성공!
push와 pop지금은 총액 37을 하드코딩했다. 여러 총액에 대한 답을 한 번에 얻고 싶다면? 다행히 매번 최적화기를 처음부터 만들 필요는 없다. 대신 push와 pop이라는 마법 같은 함수를 쓰면 된다. 전자는 assert 스택에 책갈피를 하나 만든다. 후자는 그 책갈피 위의 모든 assert와 책갈피 자체를 지운다. 간단하다. 그럼 30에서 39까지 해를 구해보자. 왜냐고? 그냥.
전체 main은 아래와 같다. 출력은 생략한다.
let opt = Optimize::new();
let c1 = Int::new_const("c1");
let c9 = Int::new_const("c9");
let c10 = Int::new_const("c10");
opt.assert(&c1.ge(0));
opt.assert(&c9.ge(0));
opt.assert(&c10.ge(0));
let total = (&c1 * 1) + (&c9 * 9) + (&c10 * 10);
let count = &c1 + &c9 + &c10;
opt.minimize(&count);
println!("; total\tcount\tc1\tc9\tc10");
for t in (30u32..).take(10) {
print!("; {t}\t");
opt.push();
opt.assert(&total.eq(t));
if let SatResult::Sat = opt.check(&[]) {
let model = opt.get_model().unwrap();
let c1 = model.eval(&c1, true).unwrap().as_u64().unwrap();
let c9 = model.eval(&c9, true).unwrap().as_u64().unwrap();
let c10 = model.eval(&c10, true).unwrap().as_u64().unwrap();
let count = c1 + c9 + c10;
println!("{count}\t{c1:?}\t{c9:?}\t{c10:?}");
} else {
println!("; woe for us");
}
opt.pop(); // RAII 따윈 없다
}
push/pop API는 Solver에도 있다. 아무튼 계속하자.
이번엔 복잡도가 크게 뛴다. 잠깐만 참아 달라. 스도쿠를 풀어보자.5 z3.Int들을 Rust의 배열이나 Vec으로 조직해서 제약을 걸면 된다. 먼저 풀 퍼즐은 다음과 같다.
....94.3.
...51...7
.89....4.
......2.8
.6.2.1.5.
1.2......
.7....52.
9...65...
.4.97....
이걸 [[Option<u8>;9];9]로 바꾸는 과정은 생략한다. 아래 코드는 get_puzzle() 함수가 그 정보를 돌려주는 것으로 가정한다.
let solver = Solver::new();
// 주의: 이건 Rust 배열이다. 솔버는 배열을 모른다.
let grid: [[_; 9]; 9] =
array::from_fn(|i| array::from_fn(|j| Int::new_const(format!("x{i}{j}"))));
// 각 칸은 1<=x<=9
grid.iter().flatten().for_each(|i| {
solver.assert(i.ge(1) & i.le(9));
});
// 각 행은 중복 없이 1~9를 포함
for row in &grid {
solver.assert(Ast::distinct(row));
}
// 각 열은 중복 없이 1~9를 포함
for idx in 0..9 {
let mut col = Vec::with_capacity(9);
grid.iter().for_each(|r| col.push(r[idx].clone()));
solver.assert(Ast::distinct(&col))
}
// 각 3x3은 중복 없이 1~9를 포함
for x_s in (0..9).step_by(3) {
for y_s in (0..9).step_by(3) {
let mut square = Vec::with_capacity(9);
for x in (x_s..).take(3) {
for y in (y_s..).take(3) {
// 매우 중첩된 루프
square.push(grid[x][y].clone());
}
}
solver.assert(Ast::distinct(&square))
}
}
// 마지막으로, 퍼즐에 주어진 단서와 같은 칸에는 그 값을 강제한다
get_puzzle().iter().flatten().zip(grid.iter().flatten()).for_each(|(clue, variable)| {
if let Some(clue) = clue {
solver.assert(variable.eq(*clue));
}
});
eprintln!("{solver:?}");
각 단계에서 솔버를 출력해 보면 제약을 제대로 걸었는지 디버깅할 수 있다. 출력은 200줄이 넘으니 생략. 이제 grid의 각 칸 값을 확인하면 된다.
if let SatResult::Sat = solver.check() {
let model = solver.get_model().unwrap();
for row in grid {
for int in row {
let result = model.eval(&int, true).unwrap();
print!("{result:?}");
}
println!();
}
} else {
println!("Unsolvable")
}
출력은 다음과 같다. 맞는지 직접 검증해 보시라. 다른 퍼즐로도 해보고, 제약을 더 추가해도 좋다. Miracle Sudoku도 시도해 보라.
715894632
234516897
689723145
493657218
867231954
152489763
376148529
928365471
541972386
여기서 한 가지 흥미로운 점: 솔버가 얼마나 _멍청한지_다. 솔버 출력을 보면, 행·열·작은 정사각형 같은 개념이 전혀 없다. X-wing 같은 스도쿠 기법도 없다. 데이터 조직은 전부 러스트 쪽에서 하고, 솔버에 전달되는 건 “이 변수와 저 변수는 같으면 안 됨” 같은 제약을 수없이 반복하는 것뿐이다. 그러면 솔버가 … 나머지를 채워 준다.
또 하나는, 유일해를 보장하지 않는다는 것이다. 퍼즐이 엉성하게 만들어져 해가 여럿일 수도 있는데, 그러면 솔버는 기꺼이 하나, 둘, 원하면 더 많이도 준다. 다만 풀 수 없는 경우(모순)는 잘 잡아낸다!
실전에서 솔버를 쓰는 유명한 예 중 하나가 … 레이아웃이다. 여러 요소를 페이지나 브라우저 창 등에 배치해야 한다. 간단한 버전으로 해보자.6
우리가 레이아웃할 페이지는 가로 190mm, 세로 270mm. 크기가 서로 다른 박스 3개를 올릴 것이다. 대충 정하자: 첫 박스 105x140, 둘째 85x135, 셋째 120x110. 서로 겹치면 안 된다. … 그게 다인가?
let page_width = 190;
let page_height = 270;
let solver = Solver::new();
let box_dims = [(105, 140), (85, 135), (120, 110)];
let box_locs = box_dims.map(|b| {
let left = Int::fresh_const("x");
let top = Int::fresh_const("y");
let right = &left + b.0;
let bottom = &top + b.1;
// 박스가 페이지 안에 들어오도록 강제
solver.assert(&left.ge(0));
solver.assert(&top.ge(0));
solver.assert(&right.le(page_width));
solver.assert(&bottom.le(page_height));
// 각 박스는 라인에 맞춰 정렬. 라인 높이는 10mm
solver.assert(&bottom.rem(10).eq(0));
(left, top, right, bottom)
});
// 박스들은 서로 겹치면 안 된다
for i in 0..box_locs.len() {
for j in i + 1..box_locs.len() {
let fst_box = &box_locs[i];
let snd_box = &box_locs[j];
// 튜플 구조: (left, top, right, bottom)
let cond_1 = fst_box.0.ge(&snd_box.2); // fst left >= snd right
let cond_2 = fst_box.1.ge(&snd_box.3); // fst top >= snd bottom
let cond_3 = fst_box.2.le(&snd_box.0); // fst right <= snd left
let cond_4 = fst_box.3.le(&snd_box.1); // fst bottom <= snd top
solver.assert(Bool::or(&[cond_1, cond_2, cond_3, cond_4]));
}
}
// println!("{solver:?}");
if let SatResult::Sat = solver.check() {
let model = solver.get_model().unwrap();
for (idx, b) in box_locs.into_iter().enumerate() {
print!("box {}\t", idx + 1);
let left = model.eval(&b.0, true).unwrap();
let top = model.eval(&b.1, true).unwrap();
let right = model.eval(&b.2, true).unwrap();
let bottom = model.eval(&b.3, true).unwrap();
println!("{left}, {top}, {right}, {bottom}");
}
} else {
println!("Unsolvable");
}
출력은 다음과 같다. 제법 근사한 해다.
box 1 85, 0, 190, 140
box 2 0, 5, 85, 140
box 3 0, 140, 120, 250
생각보다 쉽네. 핫.
물론, 여기 나온 예제들은 대체로 간단하다. 문제를 불리언 규칙과 제약의 형태로 모델링하는 법을 찾아내는 게 사실상 거의 전부다. 한계도 있다. z3는 2^x == 3 같은 형태는 풀지 못한다. 외부 함수를 호출해 값을 얻을 수도 없다(우회하는 방법은 있다).
아직 보여주지 않은 것도 많다. Array(프로그래밍 언어의 배열과 달리, 한 도메인에서 다른 도메인으로의 매핑에 가깝다), BV(비트벡터. and/or/비트 시프트 같은 비트 연산을 지원한다. Hanging Gardens 문제의 핵심), Set, Seq, String, 정규식 등등. 웹의 자료 대부분은 이론 비중이 높고, 나 같은 멍청한 코더를 겨냥하지는 않은 게 아쉽다.
다음에 또 보자.