SAT·SMT·정수 차분 제약

참인 문장들이 실제로 함께 가능할까?

AI가 일정을 만들면서 세 작업의 시간 조건이 모두 맞는다고 말한다고 생각해 봅시다. 각각을 참이라고 표시하는 것과 실제 시작 시간을 정할 수 있는 것은 별개의 문제입니다. SAT는 명제식이 참이 되는 Boolean 배정이 있는지 묻습니다. SMT는 그 명제들이 정수 산술 같은 배경 이론 안에서도 실현되는지 묻습니다. 제약 충족 문제인 CSP는 변수, 각 변수의 정의역, 허용되는 조합을 지정합니다. Boolean SAT는 그 중요한 특수 사례이며, 일반 CSP나 SMT는 정의역과 제약 언어에 따라 풀이 방법이 달라집니다.

이 실습은 범위 제한 없는 정수 변수 x,y,z와 다음 세 원자를 사용합니다.

$$P:(x-y\le a),\qquad Q:(y-z\le b),\qquad R:(z-x\le c).$$

경계 a,b,c는 −2부터 2까지의 정수입니다. 세 입력 절을 AND로 연결하고, 각 절 안에서는 P,Q,R과 그 부정을 OR로 연결합니다. Boolean 배정은 여덟 개지만 정수 변수의 정의역은 유한한 화면이나 여덟 개 값으로 제한하지 않습니다. 일반 SMT 전체를 푸는 도구가 아니라 정수 차분 논리의 작은 문제를 정확히 분석하는 실험입니다.

절 mask와 배정 mask를 구분하기

절 mask의 비트 가중치는 P=1, Q=2, R=4, ¬P=8, ¬Q=16, ¬R=32입니다. 예를 들어 9는 P∨¬P이므로 항상 참입니다. 0은 literal이 없는 빈 OR이므로 거짓입니다. 반면 배정 mask는 1,2,4만 사용하며 비트가 켜지면 해당 원자를 참으로 놓습니다. 배정 7은 P,Q,R 모두 참입니다.

절 행렬의 점은 해당 literal이 없다는 뜻이고 숫자는 있는 literal의 참과 거짓입니다. 행 내부는 OR, 세 행 사이는 AND입니다. 파란 그림은 Boolean CNF를 만족하는 배정, 주황 그림은 정수 이론까지 만족하는 배정입니다. SMT 수치는 정수 witness를 허용하는 Boolean 배정의 수입니다. 무한히 많을 수도 있는 정수 모델 전체의 개수를 세는 것이 아닙니다. 세로축의 0과 1은 이산 판정이지 확률이나 학습 손실이 아닙니다.

정수에서는 부정의 경계가 한 칸 이동한다

정수 변수에 대해서는 다음 동치가 성립합니다.

$$\neg(u-v\le k)\iff u-v\ge k+1\iff v-u\le-k-1.$$

a=0에서 P가 거짓이면 y−x≤−1이어야 합니다. 단순히 방향만 바꾸어 y−x≤0으로 쓰면 등호가 양쪽에 포함되어 P와 ¬P가 동시에 참이 되는 잘못된 해석을 만듭니다. 실수에서는 0과 1 사이에도 값이 있으므로 같은 +1 변환을 사용할 수 없습니다. 정의역을 바꾸면 이론 검사도 바뀌어야 합니다.

부등식을 화살표로 바꾸기

v−u≤w는 u에서 v로 향하는 가중치 w의 간선입니다. 모든 간선에서 d_v≤d_u+w를 만족하는 정수 potential d를 찾으면 그 값이 실제 변수의 해입니다. Bellman–Ford는 모든 potential을 0으로 시작합니다. 이는 별도의 시작점에서 모든 변수로 가중치 0의 간선을 추가하는 것과 같습니다. 세 변수 그래프에서 세 차례 완화하고 마지막 차례에도 값이 내려가면 음수 사이클이 있습니다. 그렇지 않으면 계산한 potential이 모든 제약을 만족합니다.

음수 사이클이 왜 모순일까요? 사이클에 있는 부등식을 모두 더하면 변수 항이 서로 사라집니다.

$$0\le\sum_{e\in\mathrm{cycle}}w_e<0.$$

0이 음수 이하일 수 없으므로 해당 원자 배정에는 정수 해가 없습니다. 이는 계산 시간이 부족하다는 표시가 아니라 모순의 인증서입니다. 해가 있으면 모든 potential에서 d_x를 빼서 x=0으로 보여줍니다. 차이는 보존되므로 가능한 해 전체를 대표하는 평행이동 정규화입니다. x를 검색 범위에 가둔 것이 아니며 해가 유일하다는 뜻도 아닙니다.

세 안내 실험을 손으로 풀기

첫 예제는 a=0,b=0,c=−1이며 입력 절은 P,Q,R입니다. Boolean에서는 배정 7 하나가 모델입니다. 하지만 x−y≤0, y−z≤0, z−x≤−1을 더하면 0≤−1이 되어 정수 해가 없습니다. SMT 해를 허용하는 Boolean 배정 수는 0이고 선택 사이클 합은 −1입니다. 이 고정된 경계에서는 ¬P∨¬Q∨¬R이라는 충돌 학습 절을 얻습니다. 절 mask로는 56입니다.

둘째 예제는 c만 0으로 바꿉니다. 이제 (0,0,0)이 세 원자와 모든 절을 만족하므로 두 검사를 통과하는 Boolean 배정 수가 각각 1입니다. 정수 해가 하나라는 뜻은 아닙니다. 임의의 정수 t에 대해 (t,t,t)가 모두 해이므로 실제 정수 모델은 무한히 많습니다. 음수 사이클과 UNSAT core는 없습니다. 없는 인증서는 0으로 꾸미지 않고 사용 불가로 표시합니다.

셋째 예제는 a=b=c=0, 입력 절 P,¬P,P∨¬P, 선택 배정 1입니다. P와 ¬P를 동시에 요구하므로 전체 식은 Boolean에서도 SMT에서도 UNSAT입니다. 그런데 선택한 원자 배정 자체에는 (0,2,1)이라는 이론 해가 있습니다. x−y=−2이므로 P는 참, y−z=1과 z−x=1이므로 Q,R은 거짓입니다. 이 해는 입력 절 ¬P를 만족하지 않으므로 전체 식의 해로 사용할 수 없습니다.

음수 사이클·학습 절·입력 core는 다른 설명이다

음수 사이클은 선택한 이론 literal들의 연립이 왜 불가능한지 설명합니다. 학습 절은 그 모순을 만드는 literal들의 동시 선택을 금지하며, 현재 고정된 경계와 원자 해석 아래 유효합니다. 선택 하나의 실패로 모든 Boolean 배정이 불가능하다고 결론 내리면 안 됩니다. 경계 (0,0,−1)에서 세 입력 절이 모두 항진식이면 선택 7은 모순이어도 다른 여섯 Boolean 배정은 SMT witness를 허용합니다.

입력 UNSAT core는 입력한 세 절 중 모순을 유지하는 부분집합입니다. 실습은 여덟 부분집합을 검사하여 절 개수가 최소인 것을 선택하며 동률이면 작은 mask를 택합니다. 첫 예제는 Boolean core가 없지만 SMT에서는 세 절 모두 필요합니다. 셋째 예제는 두 검사 모두 C1,C2가 최소 core입니다. 고정된 원자의 산술 의미는 배경 가정이며 입력 core의 절 목록에는 들어가지 않습니다. 실제 solver가 반환하는 core가 언제나 최소 개수라는 보장은 없습니다.

연습 문제와 해설

문제: 경계를 (−1,−1,−1), 입력 절을 ¬P,¬Q,¬R, 선택 배정을 0으로 놓으세요. 정수 부정을 적용하면 모순인가요?

해설: 제약은 y−x≤0, z−y≤0, x−z≤0이 됩니다. 사이클 합은 0이고 (0,0,0)이 해입니다. 원래 세 차이는 모두 0이므로 −1 이하라는 원자는 모두 거짓입니다. 음수 사이클과 가중치 합 0인 사이클을 구분해야 합니다. 이어서 C1을 빈 절로 바꾸면 전체 식은 즉시 거짓입니다. 선택 이론에는 여전히 해가 있어도 전체 해는 없으며 최소 입력 core는 C1 하나입니다.

AI 연구와 더 큰 solver로 연결하기

생성 모델의 계획을 검증하려면 필요한 조건을 먼저 정확히 부호화해야 합니다. 부호화한 식에 해가 있다는 사실은 현실의 누락된 조건까지 검증했다는 뜻이 아닙니다. witness, 충돌 인증서, 입력 core를 따로 기록하면 오류가 식 자체인지 선택한 후보인지 파악하기 쉽습니다. 이 실습은 이해를 위해 여덟 배정을 전수 열거합니다. 실제 대규모 solver는 SAT 탐색, 전파, 이론 추론을 결합하며, 여기서 CDCL이나 DPLL(T)의 전체 동작과 성능을 재현하지는 않습니다.

SMT-LIB 논리 정의에서 정수 차분 논리의 범위를 확인하고, cvc5 이론 안내서에서 해석되는 이론과 논리 선택을 살펴볼 수 있습니다. 여기의 세 변수 그래프와 예제는 교재를 위해 직접 구성했습니다.

차분 제약의 해와 음수 사이클의 관계는 MIT 6.046J 11강 5–6쪽에서 증명합니다.