이진 결정 다이어그램
컴퓨터 과학에서 이진 결정 다이어그램(binary decision diagram, BDD) 또는 분기 프로그램은 불 함수를 나타내는 데 사용되는 자료 구조이다. 더 추상적인 수준에서 BDD는 집합 또는 관계의 압축된 표현으로 간주될 수 있다. 다른 압축된 표현과 달리 압축 해제 없이 압축된 표현에서 직접 작업을 수행한다.
유사한 자료 구조에는 부정 정규형(NNF), 제갈킨 다항식 및 명제 유향 비순환 그래프(PDAG)가 있다.
정의
[편집]불 함수는 여러 (결정) 노드와 두 개의 터미널 노드로 구성된 루트, 유향, 비순환 그래프로 표현될 수 있다. 두 터미널 노드에는 0(FALSE)과 1(TRUE)이 레이블로 지정된다. 각 (결정) 노드 는 불변수 로 레이블이 지정되며 로우 자식과 하이 자식이라는 두 개의 자식 노드를 갖는다. 노드 에서 로우 (또는 하이) 자식으로 가는 에지는 변수 에 값 FALSE (또는 TRUE)를 할당하는 것을 나타낸다. 이러한 BDD는 루트의 모든 경로에서 다른 변수가 동일한 순서로 나타나면 '정렬됨'이라고 한다. BDD는 다음 두 규칙이 그래프에 적용된 경우 '축소됨'이라고 한다.
- 동형 서브그래프를 병합한다.
- 두 자식이 동형인 노드를 제거한다.
일반적으로 BDD라는 용어는 거의 항상 환원 정렬 이진 결정 다이어그램(문헌에서는 정렬 및 축소 측면을 강조해야 할 때 사용되는 ROBDD)을 의미한다. ROBDD의 장점은 특정 함수 및 변수 순서에 대해 정식(동형에 대해 고유)이라는 것이다.[1] 이 속성은 기능 등가성 확인 및 기능 기술 매핑과 같은 다른 작업에 유용하게 만든다.
루트 노드에서 1-터미널로 가는 경로는 표현된 불 함수가 참인 (부분적일 수도 있는) 변수 할당을 나타낸다. 경로가 노드에서 로우(또는 하이) 자식으로 내려갈 때 해당 노드의 변수는 0(각각 1)으로 할당된다.
예시
[편집]아래 왼쪽 그림은 이진 결정 트리(축소 규칙이 적용되지 않음)와 진리표를 보여주며, 각각 함수 를 나타낸다. 왼쪽 트리의 경우, 주어진 변수 할당에 대한 함수의 값은 그래프를 따라 터미널로 내려가는 경로를 따라 결정할 수 있다. 아래 그림에서 점선은 로우 자식으로 가는 에지를 나타내고, 실선은 하이 자식으로 가는 에지를 나타낸다. 따라서 을 찾으려면 x1에서 시작하여 점선을 따라 x2로 이동한 다음 (x1이 0으로 할당되었으므로) 두 개의 실선을 따라 이동한다 (x2와 x3가 각각 1로 할당되었으므로). 이것은 터미널 1로 이어지며, 이는 의 값이다.
왼쪽 그림의 이진 결정 트리는 두 가지 축소 규칙에 따라 최대로 축소하여 이진 결정 다이어그램으로 변환할 수 있다. 결과 BDD는 오른쪽 그림에 나와 있다.
이 불 함수를 쓰는 또 다른 표기법은 이다.
보완된 에지
[편집]
ROBDD는 보완 링크라고도 알려진 보완된 에지를 사용하여 더욱 간결하게 표현할 수 있다.[2][3] 결과 BDD는 때때로 유형화된 BDD[4] 또는 부호 있는 BDD로 알려져 있다. 보완된 에지는 로우 에지에 보완되었는지 여부를 주석으로 달아서 형성된다. 에지가 보완된 경우, 해당 에지가 가리키는 노드에 해당하는 불 함수의 부정(해당 노드를 루트로 하는 BDD가 나타내는 불 함수)을 나타낸다. 하이 에지는 결과 BDD 표현이 정식 형태임을 보장하기 위해 보완되지 않는다. 이 표현에서 BDD는 아래에 설명된 이유로 단일 리프 노드를 갖는다.
BDD를 표현할 때 보완된 에지를 사용하는 두 가지 장점은 다음과 같다.
- BDD의 부정을 계산하는 데 상수 시간이 걸린다.
- 공간 사용량(즉, 필요한 메모리)이 (최대 2배까지) 감소한다.
- 모든 주요 BDD 패키지에서 이러한 링크를 사용하지만, 컴퓨터 프로그램이 훨씬 더 복잡해지기 때문에 권장하기 어렵다. 메모리 절약은 일반적으로 미미하며, 2배를 넘지 않는다. 또한 저자의 실험에 따르면 실행 시간 측면에서도 거의 이득이 없었다.
이 표현에서 BDD에 대한 참조는 BDD의 루트를 가리키는 (가능하면 보완된) "에지"이다. 이는 보완된 에지를 사용하지 않는 표현에서 BDD의 루트 노드인 BDD에 대한 참조와는 대조적이다. 이 표현에서 참조가 에지여야 하는 이유는 각 불 함수에 대해 함수와 그 부정이 BDD 루트에 대한 에지와 동일한 BDD 루트에 대한 보완된 에지로 표현되기 때문이다. 이것이 부정이 상수 시간을 필요로 하는 이유이다. 또한 단일 리프 노드로 충분한 이유도 설명한다. FALSE는 리프 노드를 가리키는 보완된 에지로 표현되고, TRUE는 리프 노드를 가리키는 일반 에지(즉, 보완되지 않음)로 표현된다.
예를 들어, 불 함수가 보완된 에지를 사용하여 표현된 BDD로 표현된다고 가정하자. 변수에 (불) 값이 할당된 경우 불 함수의 값을 찾으려면 BDD의 루트를 가리키는 참조 에지에서 시작하여 주어진 변수 값으로 정의된 경로를 따라가다가(노드를 레이블하는 변수가 FALSE이면 로우 에지를 따라가고, 노드를 레이블하는 변수가 TRUE이면 하이 에지를 따라감) 리프 노드에 도달할 때까지 계속한다. 이 경로를 따르는 동안 우리가 통과한 보완된 에지의 수를 센다. 리프 노드에 도달했을 때 홀수 개의 보완된 에지를 교차했다면, 주어진 변수 할당에 대한 불 함수의 값은 FALSE이고, 그렇지 않으면(짝수 개의 보완된 에지를 교차했다면) 주어진 변수 할당에 대한 불 함수의 값은 TRUE이다.
이 표현에서 BDD의 예시 다이어그램은 오른쪽에 나와 있으며, 위에 있는 다이어그램과 동일한 불 표현, 즉 를 나타낸다. 로우 에지는 점선으로, 하이 에지는 실선으로 표시되며, 보완된 에지는 원본에 원으로 표시된다. @ 기호가 있는 노드는 BDD에 대한 참조를 나타낸다. 즉, 참조 에지는 이 노드에서 시작하는 에지이다.
역사
[편집]자료 구조가 만들어진 기본적인 아이디어는 섀넌 확장에서 비롯되었다. 스위칭 함수는 하나의 변수를 할당함으로써 두 개의 서브 함수(공인수)로 분할된다 (if-then-else 정규형 참고). 이러한 서브 함수가 서브 트리로 간주되면 이진 결정 트리로 표현될 수 있다. 이진 결정 다이어그램(BDD)은 C. Y. Lee[6]에 의해 도입되었고, Sheldon B. Akers[7]와 Raymond T. Boute[8]에 의해 추가로 연구되고 알려지게 되었다. 이들 저자들과는 독립적으로, "정식 괄호 형식"이라는 이름의 BDD는 Yu. V. Mamrukov가 속도 독립 회로 분석을 위한 CAD에서 구현했다.[9] 자료 구조에 기반한 효율적인 알고리즘의 잠재력은 카네기 멜런 대학교의 랜달 브라이언트가 조사했다. 그의 주요 확장은 고정 변수 순서(정식 표현을 위해)와 공유 서브그래프(압축을 위해)를 사용하는 것이었다. 이 두 가지 개념을 적용하면 집합과 관계의 표현을 위한 효율적인 자료 구조와 알고리즘이 탄생했다.[10][11] 여러 BDD에 걸쳐 공유를 확장하여, 즉 하나의 서브그래프가 여러 BDD에서 사용될 때, 공유 축소 정렬 이진 결정 다이어그램 자료 구조가 정의된다.[2] BDD라는 개념은 이제 일반적으로 그 특정 자료 구조를 지칭하는 데 사용된다.
도널드 커누스는 그의 비디오 강의 "이진 결정 다이어그램(BDD)의 재미"[12]에서 BDD를 "지난 25년간 나온 유일하고 정말 근본적인 자료 구조 중 하나"라고 부르며, 브라이언트의 1986년 논문이 한동안 컴퓨터 과학에서 가장 많이 인용된 논문 중 하나였다고 언급했다.
아드난 다르위시와 그의 협력자들은 BDD가 요구 사항의 다양한 조합에 의해 유도된 여러 불 함수의 정규형 중 하나임을 보여주었다. 다르위시에 의해 식별된 또 다른 중요한 정규형은 분해 가능한 부정 정규형 또는 DNNF이다.
응용
[편집]BDD는 CAD 소프트웨어에서 회로를 합성(논리 합성)하고 형식 검증에 광범위하게 사용된다. 결함 트리 분석, 베이즈 추론, 제품 구성 및 사적 정보 검색을 포함하여 덜 알려진 BDD의 여러 응용 프로그램이 있다.[13][14]
모든 임의의 BDD(축소되거나 정렬되지 않았더라도)는 각 노드를 2대1 멀티플렉서로 대체함으로써 하드웨어에 직접 구현할 수 있다. 각 멀티플렉서는 FPGA의 4-LUT로 직접 구현할 수 있다. 임의의 논리 게이트 네트워크를 BDD로 변환하는 것은 그렇게 간단하지 않다(AND-인버터 그래프와 달리).
BDD는 효율적인 데이터로그 인터프리터에 적용되었다.[15]
변수 순서
[편집]BDD의 크기는 표현되는 함수와 선택된 변수 순서에 따라 결정된다. 변수 순서에 따라 노드 수가 최적의 경우 선형(n에 비례)이고 최악의 경우 지수적으로 늘어나는 불 함수 가 존재한다(예: 리플 캐리 가산기). 불 함수 를 고려해 보자. 변수 순서 를 사용하면 함수를 표현하는 데 개의 노드가 필요하다. 순서 를 사용하면 BDD는 개의 노드로 구성된다.
이 자료 구조를 실제로 적용할 때 변수 순서에 신경 쓰는 것은 매우 중요하다. 최적의 변수 순서를 찾는 문제는 NP-난해이다.[16] 어떤 상수 c > 1에 대해서는 최적의 것보다 크기가 최대 c배 더 큰 OBDD를 생성하는 변수 순서를 계산하는 것도 NP-난해이다.[17] 그러나 이 문제를 해결하기 위한 효율적인 휴리스틱이 존재한다.[18]
그래프 크기가 항상 변수 순서와 무관하게 지수적인 함수도 있다. 이는 예를 들어 곱셈 함수에 해당한다.[1] 실제로, 두 비트 숫자의 곱셈의 중간 비트를 계산하는 함수는 개 정점보다 작은 OBDD를 갖지 않는다.[19] (곱셈 함수가 다항식 크기 OBDD를 갖는다면, 이는 소인수분해가 P/poly에 속함을 보여줄 것이며, 이는 사실로 알려져 있지 않다.[20]) 또 다른 악명 높은 예시는 지수 크기 BDD를 갖는 가장 간단한 함수로 간주되는 숨겨진 가중치 비트 함수이다.[21]
연구자들은 BDD 자료 구조의 개선을 제안하여 BMD(이진 모멘트 다이어그램), ZDD(제로 억제 결정 다이어그램), FBDD(자유 이진 결정 다이어그램), FDD(함수 결정 다이어그램), PDD(패리티 결정 다이어그램), MTBDD(다중 터미널 BDD)와 같은 여러 관련 그래프를 탄생시켰다.
BDD에서의 논리 연산
[편집]BDD에 대한 많은 논리 연산은 다항 시간 그래프 조작 알고리즘으로 구현될 수 있다.[22]:20
그러나 이러한 연산을 여러 번 반복하면, 예를 들어 BDD 집합의 논리곱 또는 논리합을 형성하면 최악의 경우 기하급수적으로 큰 BDD가 발생할 수 있다. 이는 두 BDD에 대한 이전 연산 중 하나가 BDD 크기의 곱에 비례하는 BDD를 초래할 수 있고, 결과적으로 여러 BDD의 경우 연산 수에 따라 크기가 기하급수적으로 커질 수 있기 때문이다. 변수 순서는 새로 고려해야 한다. BDD 집합(일부)에 좋은 순서가 연산 결과에 좋은 순서가 아닐 수도 있다. 또한 불 함수의 BDD를 구성하는 것은 NP-완전 충족 가능성 문제와 co-NP-완전 항진식 문제를 해결하므로, 결과 BDD가 작더라도 BDD를 구성하는 데 불 수식 크기에 비례하여 기하급수적인 시간이 걸릴 수 있다.
축소된 BDD의 여러 변수에 대한 존재 추상화를 계산하는 것은 NP-완전이다.[23]
모델-카운팅, 즉 불 함수의 만족 할당 수를 세는 것은 BDD의 경우 다항 시간에 수행될 수 있다. 일반적인 명제 수식의 경우 문제는 ♯P-완전이며 알려진 최상의 알고리즘은 최악의 경우 지수 시간을 필요로 한다.
같이 보기
[편집]- 충족 가능성 문제, 정식 NP-완전 계산 문제
- L/poly, 다항식 크기의 BDD를 가진 문제 집합을 엄격하게 포함하는 복잡도 종류
- 모델 검사
- 기수 트리
- 배링턴 정리
- 하드웨어 가속
- 카노 맵, 불 대수 표현식을 단순화하는 방법
- 제로 억제 결정 다이어그램
- 대수 결정 다이어그램, 2원소에서 임의의 유한 집합으로의 BDD 일반화
- 문장 결정 다이어그램, OBDD의 일반화
- 영향 다이어그램
각주
[편집]- ↑ 가 나 Bryant, Randal E. (August 1986). 《Graph-Based Algorithms for Boolean Function Manipulation》 (PDF). 《IEEE Transactions on Computers》 C–35. 677–691쪽. CiteSeerX 10.1.1.476.2952. doi:10.1109/TC.1986.1676819. S2CID 10385726.
- ↑ 가 나 Brace, Karl S.; Rudell, Richard L.; Bryant, Randal E. (1990). 〈Efficient Implementation of a BDD Package〉. 《Proceedings of the 27th ACM/IEEE Design Automation Conference (DAC 1990)》. IEEE Computer Society Press. 40–45쪽. doi:10.1145/123186.123222. ISBN 978-0-89791-363-8.
- ↑ Somenzi, Fabio (1999). 〈Binary decision diagrams〉 (PDF). 《Calculational system design》. NATO Science Series F: Computer and systems sciences 173. IOS Press. 303–366쪽. ISBN 978-90-5199-459-9.
- ↑ Jean-Christophe Madre; Jean-Paul Billon (1988). 〈Proving Circuit Correctness Using Formal Comparison Between Expected and Extracted Behaviour〉. 《Proceedings of the 25th ACM/IEEE Conference on Design Automation, DAC '88, Anaheim, CA, USA, June 12-15, 1988》. 205–210쪽. doi:10.1109/DAC.1988.14759. ISBN 0-8186-0864-1.
- ↑ Knuth, D.E. (2009). 《Fascicle 1: Bitwise tricks & techniques; Binary Decision Diagrams》. 컴퓨터 프로그래밍의 예술 4. Addison–Wesley. ISBN 978-0-321-58050-4. Fascicle 1b 초안 보관됨 2016-03-12 - 웨이백 머신 다운로드 가능
- ↑ Lee, C.Y. (1959). 《Representation of Switching Circuits by Binary-Decision Programs》. 《Bell System Technical Journal》 38. 985–999쪽. doi:10.1002/j.1538-7305.1959.tb01585.x.
- ↑ Akers, Jr., Sheldon B (June 1978). 《Binary Decision Diagrams》. 《IEEE Transactions on Computers》 C–27. 509–516쪽. doi:10.1109/TC.1978.1675141. S2CID 21028055.
- ↑ Boute, Raymond T. (January 1976). 《The Binary Decision Machine as a programmable controller》. 《EUROMICRO Newsletter》 1. 16–22쪽. doi:10.1016/0303-1268(76)90033-X.
- ↑ Mamrukov, Yu. V. (1984). 《Analysis of aperiodic circuits and asynchronous processes》 (PhD). Leningrad Electrotechnical Institute.
- ↑ Bryant., Randal E. (1986). 《Graph-Based Algorithms for Boolean Function Manipulation》 (PDF). 《IEEE Transactions on Computers》 C–35. 677–691쪽. doi:10.1109/TC.1986.1676819. S2CID 10385726.
- ↑ Bryant, Randal E. (September 1992). 《Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams》. 《ACM Computing Surveys》 24. 293–318쪽. doi:10.1145/136035.136043. S2CID 1933530.
- ↑ “Stanford Center for Professional Development”. 《scpd.stanford.edu》. 2014년 6월 4일에 원본 문서에서 보존된 문서. 2018년 4월 23일에 확인함.
- ↑ Jensen, R.M. (2004). 〈CLab: A C++ library for fast backtrack-free interactive product configuration〉. 《Proceedings of the Tenth International Conference on Principles and Practice of Constraint Programming》. Lecture Notes in Computer Science 3258. Springer. 816쪽. doi:10.1007/978-3-540-30201-8_94. ISBN 978-3-540-30201-8.
- ↑ Lipmaa, H.L. (2009). 〈First CPIR Protocol with Data-Dependent Computation〉 (PDF). 《International Conference on Information Security and Cryptology》. Lecture Notes in Computer Science 5984. Springer. 193–210쪽. doi:10.1007/978-3-642-14423-3_14. ISBN 978-3-642-14423-3.
- ↑ Whaley, John; Avots, Dzintars; Carbin, Michael; Lam, Monica S. (2005). 〈Using Datalog with Binary Decision Diagrams for Program Analysis〉 (영어). Yi, Kwangkeun (편집). 《Programming Languages and Systems》. Lecture Notes in Computer Science 3780. Berlin, Heidelberg: Springer. 97–118쪽. doi:10.1007/11575467_8. ISBN 978-3-540-32247-4. S2CID 5223577.
- ↑ Bollig, Beate; Wegener, Ingo (September 1996). 《Improving the Variable Ordering of OBDDs Is NP-Complete》. 《IEEE Transactions on Computers》 45. 993–1002쪽. doi:10.1109/12.537122.
- ↑ Sieling, Detlef (2002). 《The nonapproximability of OBDD minimization》. 《Information and Computation》 172. 103–138쪽. doi:10.1006/inco.2001.3076.
- ↑ Rice, Michael. “A Survey of Static Variable Ordering Heuristics for Efficient BDD/MDD Construction” (PDF).
- ↑ Woelfel, Philipp (2005). 《Bounds on the OBDD-size of integer multiplication via universal hashing》. 《Journal of Computer and System Sciences》 71. 520–534쪽. CiteSeerX 10.1.1.138.6771. doi:10.1016/j.jcss.2005.05.004.
- ↑ 리처드 J. 립튼. "BDD's and Factoring". 괴델의 잃어버린 편지와 P=NP, 2009.
- ↑ Méaux, Pierrick; Seuré, Tim; Deng, Tang (2024). 《The Revisited Hidden Weight Bit Function》 (PDF). 《IACR Cryptology ePrint Archive》. 24쪽. 2025년 6월 19일에 확인함.
- ↑ Andersen, H. R. (1999). “An Introduction to Binary Decision Diagrams” (PDF). 《Lecture Notes》. IT University of Copenhagen.
- ↑ Huth, Michael; Ryan, Mark (2004). 《Logic in computer science: modelling and reasoning about systems》 2판. Cambridge University Press. 380–쪽. ISBN 978-0-52154310-1. OCLC 54960031.
더 읽어보기
[편집]- Ubar, R. (1976). 《Test Generation for Digital Circuits Using Alternative Graphs》 (러시아어). 《Proc. Tallinn Technical University》 (Tallinn, Estonia). 75–81쪽.
- Meinel, C.; Theobald, T. (2012) [1998]. 《Algorithms and Data Structures in VLSI-Design: OBDD – Foundations and Applications》 (PDF). Springer. ISBN 978-3-642-58940-9. 전체 교과서 다운로드 가능.
- Ebendt, Rüdiger; Fey, Görschwin; Drechsler, Rolf (2005). 《Advanced BDD optimization》. Springer. ISBN 978-0-387-25453-1.
- Becker, Bernd; Drechsler, Rolf (1998). 《Binary Decision Diagrams: Theory and Implementation》. Springer. ISBN 978-1-4419-5047-5.



