VLSI Korea[VLSI CAD] MiniSAT?
SAT(Satisfiability) 문제는 다음 질문으로 요약된다. 주어진 Boolean 수식이 True가 되도록 변수들을 True / False로 정할 수 있는가? 예를 들어, f(x,y,z)=(x || y) && (!x || z) 라는 수식이 있을 때, 이건 단순해...
![[VLSI CAD] MiniSAT?](https://images.unsplash.com/photo-1509228468518-180dd4864904?crop=entropy&cs=tinysrgb&fit=max&fm=webp&ixid=M3wxMTc3M3wwfDF8c2VhcmNofDN8fG1hdGh8ZW58MHx8fHwxNzcyOTUwMDY2fDA&ixlib=rb-4.1.0&q=80&w=2000)
🆓 무료 글 · 누구나 무료로 읽을 수 있는 글입니다
SAT(Satisfiability) 문제는 다음 질문으로 요약된다.
주어진 Boolean 수식이 True가 되도록
변수들을 True / False로 정할 수 있는가?
예를 들어, f(x,y,z)=(x || y) && (!x || z) 라는 수식이 있을 때,
- x, y, z에 True/False를 어떻게 할당하면 전체 수식이 True가 되는지를 찾는 것이 SAT 문제다.
이건 단순해 보이지만,
- 변수 수가 수천~수만 개
- 제약이 수십만 개가 되면 완전 탐색은 불가능해진다.
이걸 효율적으로 푸는 것이 SAT solver의 역할이다.
2. MiniSat은 어떤 SAT solver인가
MiniSat은 고성능 CDCL 기반 SAT solver다.
특징을 요약하면:
- CDCL (Conflict-Driven Clause Learning)
- 매우 작은 코드베이스
- 빠르고 안정적
- 다른 툴에 라이브러리처럼 embedding하기 쉬움
그래서 MiniSat은 단독으로 쓰이기도 하지만,
실제로는 다음과 같은 용도로 더 많이 쓰인다.
- Formal Verification tool 내부 엔진
- EDA tool의 decision engine
- Research prototype의 baseline solver
- SMT / PB solver의 backend SAT engine
즉,
MiniSat은 “SAT solver계의 표준 엔진”에 가깝다
3. 그런데 현실 문제는 SAT만으로 안 끝난다
문제는 현실의 제약이 항상 Boolean만은 아니라는 점이다.
예를 들어 이런 제약은 SAT가 아니다.
3a + 2b + c ≥ 4
여기서 a, b, c는 Boolean 변수지만,
식 자체는 정수 가중치를 가진 제약이다.
이런 제약을 Pseudo-Boolean (PB) constraint라고 부른다.
PB 문제의 특징:
- 변수는 Boolean
- 제약은 선형 정수 부등식
- 최적화 문제(min/max)가 붙는 경우도 많음
4. MiniSat+의 핵심 아이디어
MiniSat+는 새로운 solver가 아니다.
핵심 아이디어는 단 하나다.
PB 제약을 SAT로 “번역”한 뒤,
MiniSat으로 푼다
즉 구조는 이렇다.
PB 문제
↓ (translation)
SAT 문제
↓
MiniSat
MiniSat+는 이 translation layer를 담당한다.
5. PB → SAT는 어떻게 바꾸는가
MiniSat+는 PB 제약을 SAT로 바꾸기 위해
다음과 같은 논리 회로 기반 기법을 사용한다.
- BDD (Binary Decision Diagram)
- Adder network
- Sorting network
핵심은:
- PB 제약을 만족하는지 판단하는 논리 회로를 만든 뒤
- 그 회로를 Tseitin transformation으로 CNF로 변환
- 결과를 MiniSat에 입력
즉,
“제약을 검사하는 회로를 만들고,
그 회로가 항상 True가 되도록 강제한다”
6. 왜 굳이 SAT로 바꾸는가
직접 PB solver를 쓰면 되지 않냐는 질문이 나온다.
논문과 실무에서의 답은 명확하다.
- SAT solver는 수십 년간 최적화됨
- Clause learning, heuristics, propagation이 매우 강력
- “거의 SAT에 가까운 문제”에서는
- PB native solver보다
- SAT 변환 + MiniSat이 더 빠른 경우가 많음
특히 EDA/Verification 쪽 문제는:
- 대부분 Boolean 구조
- 일부만 가중치/카운트 제약
이 구조에서 MiniSat+ 접근이 잘 먹힌다.
7. EDA 관점에서 보면 어디에 쓰이나
엔지니어 관점에서 보면 MiniSat 계열은 다음 문제에 자연스럽게 대응한다.
- Formal equivalence checking
- ECO에서 최소 수정 집합 선택
- Constraint-based synthesis
- Resource / option selection 문제
- 일부 STA/CDC/DFT 내부 decision logic
공통점은 모두 이렇다.
선택 변수 + 제약 조건 + 조합 폭발
이걸 사람이 로직으로 직접 다루는 순간 유지보수 지옥이 된다.
SAT solver는 이걸 엔진 레벨에서 해결해준다.
8. 한 문단 요약
- MiniSat
→ 고성능 Boolean SAT solver
→ 선택 문제를 빠르게 푸는 엔진 - MiniSat+
→ 정수 가중치 제약(PB)을 SAT로 변환
→ MiniSat의 성능을 그대로 활용 - 왜 쓰이나
→ SAT solver는 여전히 가장 강력한 조합 탐색 엔진
→ EDA/Verification에서 구조적으로 잘 맞음
자주 묻는 질문
SAT 문제란 무엇인가?
주어진 Boolean 수식이 True가 되도록 변수들을 True·False로 정할 수 있는지를 묻는 문제다. 변수 수천~수만 개, 제약 수십만 개가 되면 완전 탐색이 불가능해지며, 이를 효율적으로 푸는 것이 SAT solver의 역할이다.
MiniSat은 어떤 SAT solver인가?
고성능 CDCL(Conflict-Driven Clause Learning) 기반 SAT solver다. 코드베이스가 매우 작고 빠르고 안정적이며, 다른 툴에 라이브러리처럼 embedding하기 쉬워 formal verification 툴의 내부 엔진이나 EDA decision engine으로 많이 쓰인다.
MiniSat+의 핵심 아이디어는 무엇인가?
새 solver가 아니라, Pseudo-Boolean 제약을 SAT로 번역한 뒤 MiniSat으로 푸는 translation layer다. BDD, adder network, sorting network로 제약을 검사하는 논리 회로를 만들고, Tseitin transformation으로 CNF로 변환해 MiniSat에 입력한다.
Pseudo-Boolean(PB) 제약이란 무엇인가?
변수는 Boolean이지만 식 자체는 정수 가중치를 가진 선형 부등식인 제약이다. 예를 들어 3a + 2b + c ≥ 4 같은 형태이며, 최적화 문제가 붙는 경우도 많다.
관련 글
