제약 솔버로 NAND 게이트 9개짜리 전가산기 회로를 찾고 최소 조건을 확인하다

제약 솔버를 이용해 NAND 게이트만으로 1비트 전가산기 회로를 설계하는 과정을 소개한다. CPMpy와 OR-Tools의 CP-SAT 솔버로 회로 연결과 출력을 모델링한 결과, 게이트 9개와 깊이 6이 필요했고 게이트 8개로는 해가 없었다.

제약 만족 문제(CSP)는 변수와 가능한 값, 변수 간 제약으로 문제를 표현한다. 목적에 게이트 수나 깊이의 최소화를 더하면 제약 최적화 문제가 된다. 글은 게이트 수를 고정한 뒤 깊이를 최소화하는 방식으로 두 목표를 다룬다.

전가산기는 입력 비트 A, B와 입력 올림 비트 Ci를 받아 합 비트 S와 출력 올림 비트 Co를 만든다. 글에서는 2 Co + S = A + B + Ci를 만족하도록 NAND 게이트의 연결을 찾는다. 각 게이트에는 입력·출력 값과 깊이를 나타내는 변수를 두고, 게이트 사이의 연결과 전가산기의 입출력 대응을 제약으로 표현한다.

처음에는 전가산기의 산술 관계만 모델링해 잘못된 회로가 나왔다. 이 관계는 입력과 출력이 한 번만 맞으면 만족할 수 있어, 모든 입력 조합에서 올바르게 동작한다는 조건을 보장하지 않기 때문이다. 이를 해결하기 위해 가능한 8가지 입력 조합을 각각 변수 배열에 담고, 진리표를 제약으로 추가했다.

글에 따르면 CP-SAT는 이 모델에서 9개 게이트로 동작하는 회로를 찾았다. 게이트 수를 8개로 줄이면 약 99밀리초 만에 해가 없다고 판정했고, 깊이를 최소화하면 최적 깊이 6을 찾았다. 이는 글에 소개된 모델과 솔버 실행 결과이며, 더 큰 가산기에서는 탐색이 어려워지기 시작한다고 설명한다. 2비트 가산기는 여전히 풀 수 있지만, 더 큰 회로는 전가산기를 불투명한 블록으로 조합해 다루는 방법을 제안한다.

활용과 참고 자료

글은 제약 풀이가 분산 프로그램의 경쟁 상태·교착 상태 검증, 메카트로닉스 시스템 설계, 매개변수 최적화 등에 쓰인다고 설명한다. 관련 분야로 SAT, SMT, 제약 프로그래밍을 들며, 게임의 절차적 타일맵 생성 기법인 Wave Function Collapse와 Lean 증명 보조기의 Grind 전술도 언급한다.

CPMpy로 작성한 전체 코드는 gist에서 확인할 수 있다. 글에서 안내하는 자료로는 CPMpy 문서, OR-Tools, CP-SAT가 있다.