[VLSI CAD] MiniSAT?

SAT(Satisfiability) 문제는 다음 질문으로 요약된다.

주어진 Boolean 수식이 True가 되도록
변수들을 True / False로 정할 수 있는가?

예를 들어, f(x,y,z)=(x || y) && (!x || z) 라는 수식이 있을 때,

• x, y, z에 True/False를 어떻게 할당하면 전체 수식이 True가 되는지를 찾는 것이 SAT 문제다.

이건 단순해 보이지만,

• 변수 수가 수천~수만 개
• 제약이 수십만 개가 되면 완전 탐색은 불가능해진다.
  이걸 효율적으로 푸는 것이 SAT solver의 역할이다.

MiniSat Page

by Niklas Eén, Niklas Sörensson

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에서 구조적으로 잘 맞음