이항 결정도

컴퓨터 과학에서 BDD(binary decision diagram) 또는 분기 프로그램은 부울 함수를 나타내기 위해 사용되는 데이터 구조입니다.보다 추상적인 수준에서 BDD는 집합 또는 관계를 압축한 표현으로 간주할 수 있습니다.다른 압축 표현과 달리, 연산은 압축 표현에 대해 직접, 즉 압축 해제 없이 수행됩니다.

유사한 데이터 구조로는 부정 정규형(NNF), 제갈킨 다항식 및 명제 지향 비순환 그래프(PDAG)가 있다.

정의.

부울 함수는 루트의 유도 비순환 그래프로 나타낼 수 있습니다.이 그래프는 여러 개의 (결정) 노드와 두 개의 터미널 노드로 구성됩니다.2개의 터미널 노드에는 0(FALSE)과 1(TRUE)의 라벨이 붙어 있습니다.각 ($결정$) $노드$u {displaystyle$$u}에는$$$$ 부울 $변수{\displaystyle {}_{}}$ ${\displaystyle x_{}}$i {\$displaystyle x_{i$} 로 라벨이 부착되어 있으며 하위 노드와 상위 노드라는2개의 하위 노드가 있습니다.$노드{\displaystyle }$u {\$displaystyle$u}에서$$ 하위(또는 높음) 자에 대한 엣지는 값 FALSE(또는 TRUE)를 ${\displaystyle {변수}_{}}$ xi$${\$style x_{i$에 할당한 것을 나타냅니다.루트로부터의 모든 경로에 다른 변수가 같은 순서로 표시되는 경우는, 이러한 BDD를 「순서」라고 부릅니다.BDD의 그래프에 다음의 2개의 룰이 적용되고 있는 경우, BDD는 「축소」라고 불립니다.

• 모든 동형 서브그래프를 병합합니다.
• 두 자녀가 동형인 노드를 모두 제거합니다.

일반적인 용법에서 BDD라는 용어는 거의 항상 순서부여된 이진 의사결정도(문헌에서 순서부여 및 감소 측면을 강조해야 할 때 사용되는 ROBDD)를 나타냅니다.ROBDD의 장점은 특정 함수 및 가변 ^[1]순서에 대해 표준(고유)이라는 것입니다.이 속성은 기능적 동등성 검사 및 기능적 기술 매핑과 같은 기타 작업에 유용합니다.

루트 노드에서1 터미널까지의 경로는 표현된 부울 함수가 참인 (일부적인) 변수 할당을 나타냅니다.경로가 노드에서 하위(또는 상위) 하위(또는 하위)로 내려가면 해당 노드의 변수가 0(각각 1)에 할당됩니다.

예

아래 왼쪽 그림은 함수 $f{\displaystyle (x}$1, ${\displaystyle x}$2, x${\displaystyle 3}$)$${$displaystyle$ f$(x1, x2, x3$를 나타내는 이진수 결정 트리(축소 규칙은 적용되지 않음)와 진실 테이블을 보여 줍니다.왼쪽 트리에서 함수의 값은 단말기로의 경로를 따라 특정 변수 할당에 대해 확인할 수 있습니다.아래 그림에서 점선은 낮은 아이의 가장자리를 나타내며 실선은 높은 아이의 가장자리를 나타냅니다.따라서 f${\displaystyle }$( ${\displaystyle 0}$,${\displaystyle 1}$ , $){$ $displaystyle$f ($0$ ,$1$)$$}를 찾으려면 x1부터 시작하여 점선을 따라 x2까지 이동한 다음 (x1에 0이 할당되어 있으므로)2개의 실선으로 이동합니다(x2와 x3에 각각1이 할당되어 있기 때문에).이것에 의해, 단자 1에 연결됩니다.${\displaystyle \mathrm{이것}}$은${\displaystyle }$f (${\displaystyle 0}$ ,${\displaystyle 1}$ $){$ $displaystyle$f ($0$ ,$1$) $\}$의 값입니다.

왼쪽 그림의 2진수 결정 트리는 2개의 축소 규칙에 따라 최대 축소함으로써 2진수 결정 다이어그램으로 변환할 수 있습니다.결과 BDD는 오른쪽 그림에 나타나 있습니다.

${\displaystyle {}_{}}$f ( ${\displaystyle {}_{}}$ ${\displaystyle {1\mathrm{}}_{}}$,${\displaystyle {}_{}{}_{}{}_{}}$2, x${\displaystyle {}_{}{3\mathrm{}}_{}}$) ${\displaystyle =}$ (${\displaystyle \mathrm{}{}_{}}$ x ${\displaystyle {1\mathrm{}}_{}}$ ${\displaystyle {}_{}}$ ${\displaystyle {x\mathrm{}}_{}}$ 2 ${\displaystyle \mathrm{\wedge }}$ ${\displaystyle {x\mathrm{}}_{}}$3) ${\displaystyle \vee }$ ( ${\displaystyle {}_{}}$ 2${\displaystyle {}_{}{}_{}}$ x 2)${\displaystyle \vee }$ ( ${\displaystyle {x\mathrm{}}_{}}$ ${\displaystyle {2\mathrm{}}_{}}$ )$$ ( x 3${\displaystyle {}_{}}$) { $display style$ f$(x_{1$},$x_{$3}) = (\$neg x_{1}\neg)$의 이진법 결정 트리 및 진실 표 오퍼레이터.

함수 f의 BDD

이 부울 함수를 쓰기 위한 다른 표기법은 $x{\displaystyle {\stackrel{}{}}_{}}$ $1$1 x${\displaystyle {\stackrel{}{}}_{}{2}_{\mathrm{}}}$ ${\displaystyle {}_{}{\stackrel{}{}}_{}}$ x ${\displaystyle 3_{\mathrm{}}}$3 + ${\displaystyle {}_{}}$ ${\displaystyle {}_{}{}_{}}$ x${\displaystyle {}_{}{2\mathrm{}}_{}}$ + ${\displaystyle {}_{}}$ ${\displaystyle {2\mathrm{}}_{}}$ ${\displaystyle {}_{}{}_{}}$ ${\displaystyle {2\mathrm{}}_{}}$ {$$\ $displaystyle${ \ $overline { x$} _ {$}$ _ {$}$ { \ $overline { x$} + $x _$ { 1 } 입니다.$}x_{2}+x_{2$$}x_{$3$\}\}:$

보완된 가장자리

보완된 모서리를 사용하여 ^[2][3]ROBDD를 더욱 콤팩트하게 표현할 수 있습니다.보완된 모서리는 낮은 모서리에 보완된 것인지 여부에 대한 주석을 달아 형성됩니다.에지가 보완되어 있는 경우는, 에지가 가리키는 노드(루트를 가지는 BDD에 의해서 나타나는 부울 함수)에 대응하는 부울 함수의 부정을 참조합니다.결과적인 BDD 표현이 정규 형식이 되도록 하기 위해 높은 에지는 보완되지 않습니다.이 그림에서 BDD에는 리프 노드가 1개 있습니다.이러한 이유는 다음과 같습니다.

BDD를 나타낼 때 보완 에지를 사용하는 두 가지 장점은 다음과 같습니다.

• BDD의 부정 계산에는 일정한 시간이 걸린다
• 공간 사용량(즉, 필요한 메모리) 감소

이 표현에서 BDD는 BDD의 루트를 가리키는 (보완될 가능성이 있는) 엣지입니다.이는 BDD의 루트 노드인 보완 에지를 사용하지 않고 표현에서 BDD를 참조하는 것과는 대조적입니다.이 표현에서 참조가 엣지여야 하는 이유는 각 부울 함수에 대해 함수와 부정이 BDD의 루트에 대한 엣지와 동일한 BDD의 루트에 대한 보완 엣지로 표현되기 때문입니다.이것이 부정하는 데 일정한 시간이 걸리는 이유이다.또한 단일 리프 노드가 충분한 이유에 대해서도 설명합니다.FALSE는 리프 노드를 가리키는 보완된 에지로 표현되며 TRUE는 리프 노드를 가리키는 일반 에지(즉, 보완되지 않음)로 표현됩니다.

예를 들어, 부울 함수가 보완된 에지를 사용하여 표현되는 BDD로 표현된다고 가정합니다.변수에 대한 (부울) 값의 특정 할당에 대한 부울 함수의 값을 찾으려면 BDD의 루트를 가리키는 참조 에지에서 시작하여 주어진 변수 값에 의해 정의된 경로를 따릅니다(노드에 FALSE라는 레이블이 있는 변수가 있으면 낮은 에지를 따르고 변수 th에 해당하는 경우 높은 에지를 따릅니다).라벨이 TRUE인 경우)로 설정합니다.이 경로를 따라 이동하는 동안 횡단한 보완 에지 수를 계산합니다.리프 노드에 도달했을 때 보완된 홀수의 에지를 넘었을 경우 지정된 변수 할당에 대한 부울 함수의 값은 FALSE이고, 그렇지 않을 경우(짝수의 보완된 에지를 넘었을 경우), 지정된 변수 할당에 대한 부울 함수의 값은 TRUE입니다.

이 표현에서의 BDD의 예시는 오른쪽에 나타나 있으며, 위의 그림과 같은 부울식을 나타내고 있습니다.${\displaystyle {즉\mathrm{}}_{}}$, (${\displaystyle \mathrm{}{1\mathrm{}}_{}}$ x 1${\displaystyle \mathrm{}{}_{}}$ x 2${\displaystyle {}_{}{x\mathrm{}}_{}}$ ${\displaystyle {x\mathrm{}}_{}}$3 ) ${\displaystyle \vee }$ ( ${\displaystyle {x\mathrm{}}_{}}$ 2${\displaystyle {}_{}{}_{}}$ ${\displaystyle {x\mathrm{}}_{}}$ 3${\displaystyle {}_{}}$)$style$ （ $neg x$_ $1$\ \ $wed$）$。$$\}\}.$ 낮은 가장자리는 점선 처리되고 높은 가장자리는 솔리드 처리되며 보완된 가장자리는 "-1" 라벨로 표시됩니다.라벨이 @ 기호로 시작하는 노드는 BDD에 대한 참조를 나타냅니다. 즉, 기준 에지는 이 노드에서 시작하는 에지입니다.

역사

데이터 구조가 생성된 기본 개념은 Shannon 확장입니다.스위칭 함수는 하나의 변수(if-then-else 정규형식 참조)를 할당함으로써 2개의 서브함수(코팩터)로 분할된다.이러한 하위 함수가 하위 트리로 간주될 경우, 이진수 결정 트리로 나타낼 수 있습니다.이진 결정 다이어그램(BDD)은 C. Y.^[4] Lee에 의해 도입되었고 쉘든 B에 의해 추가로 연구되고 알려졌다.에이커스와^[5] 레이먼드 T.Boute.^[6] 이들 저자와는 별도로 속도 독립 ^[7]회로 분석을 위한 CAD에서 "캐노니컬 브래킷 형태"라는 이름의 BDD가 실현되었습니다.데이터 구조를 기반으로 한 효율적인 알고리즘의 모든 가능성을 Carnegie Mellon 대학의 Randal Bryant가 조사했습니다. 그의 주요 확장 기능은 고정 변수 순서(표준 표현용)와 공유 하위 그래프(압축용)를 사용하는 것이었습니다.이 두 가지 개념을 적용하면 집합과 ^[8][9]관계를 표현하기 위한 효율적인 데이터 구조와 알고리즘이 생성됩니다.공유를 여러 BDD로 확장함으로써, 즉 하나의 서브 그래프가 여러 BDD에 의해 사용됨으로써, 데이터 구조의 공유 감소 순서 바이너리 결정도를 ^[2]정의한다.현재 BDD의 개념은 일반적으로 특정 데이터 구조를 지칭하는 데 사용됩니다.

Donald Knuth는 비디오 강의인 Fun With Binary Decision Diagram(BDDs)^[10]에서 BDD를 "지난 25년간 나온 가장 기본적인 데이터 구조 중 하나"라고 칭하며 Bryant의 1986년 논문은 한동안 컴퓨터 과학에서 가장 주목받는 논문 중 하나였다고 언급했습니다.

Adnan Darwiche와 그의 협력자들은 BDD가 각각 다른 요구사항 조합에 의해 유도되는 부울 함수의 몇 가지 정상적인 형태 중 하나라는 것을 보여주었다.Darwiche에 의해 식별된 또 다른 중요한 정상 형태는 분해 가능한 부정 정상형 또는 DNNF이다.

적용들

BDD는 CAD 소프트웨어에서 회로 합성(로직 합성) 및 형식 검증에 광범위하게 사용됩니다.BDD에는 폴트 트리 분석, 베이지안 추론, 제품 구성, 개인 정보 ^{[11][12][citation needed]}검색 등 잘 알려지지 않은 응용 프로그램이 몇 가지 있습니다.

각 노드를 2 대 1의 멀티플렉서로 대체함으로써 임의의 BDD를 하드웨어에 직접 구현할 수 있습니다.각 멀티플렉서는 FPGA의 4-LUT에 의해 직접 구현할 수 있습니다.논리 게이트의 임의의 네트워크에서 BDD로^{[citation needed]} 변환하는 것은 그리 간단하지 않습니다(and-inverter 그래프와는 다릅니다).

가변 순서 지정

BDD의 크기는 표시되는 함수와 변수의 선택된 순서에 따라 결정됩니다.부울 함수 f (${\displaystyle {}_{}}$ 1 , ... ,${\displaystyle {}_{}}$n$$) { $displaystyle$f ( x$_$ {$1}$ , \$ldots$, x$_$ { $n$} )이 $있습니다{\displaystyle }$.변수의 순서에 따라 노드 수가 최대로 선형(n 단위), 최악의 경우 지수(예: 리플 캐리 가산기)인 그래프를 얻을 수 있습니다.부울 $함수{\displaystyle }$f ( ${\displaystyle {}_{}{1\mathrm{}}_{}}$,${\displaystyle \dots ,}$ ${\displaystyle {}_{}}$ ${\displaystyle {2\mathrm{}}_{}{n}_{}}$ ) ${\displaystyle =}$ ${\displaystyle {x\mathrm{}}_{}}$ ${\displaystyle {}_{}{}_{}}$ x${\displaystyle {}_{}{2\mathrm{}}_{}}$ + ${\displaystyle {}_{}}$ ${\displaystyle {}_{}{}_{}}$ x${\displaystyle {}_{}{4\mathrm{}}_{}}$ +${\displaystyle \cdots }$ + ${\displaystyle {}_{}}$ ${\displaystyle 2_{}}$n - ${\displaystyle {}_{}{}_{}}$ ${\displaystyle {x\mathrm{}}_{}}$ 2${\displaystyle {}_{}{n}_{}}$. { $display$ f ( x$_$ {$1$ , \$ldots$, $x$_ 2 n } = x $_${ 1$x$ _ { 2 $n$} + x$_ 3$ n .$}x_{4}+\cdots +x_{2n-1}x_{2n}.$} 1 < 3 < - 1 < > < 4 > < 2 $n <$ x _ { x $3$} <\$cdots$ < x _ { 2 n - 1 } <x _ { $4$ } <\$cdots$ <x$_$ { 2 n} } 를 사용하면, BDD $display$ 2${\displaystyle {\mathrm{n}}^{}}$ + 1$$이 ${\displaystyle {필요}^{}}$합니다$.$ 1< < < 4 n - < n - 1 < x 2 $n }$ < $x$_ { x _ { 3 } < x$_$ { $4 }$ <\ $cdots$ < $x$_ { $2n$ - 1 } <$x_{$ $2n}$ } <x_{ 4$}$ >를$$ 사용하면, BDD는${\displaystyle 2}$ +$2$ n노드로 $구성$됩니다.

함수 δ(x1, ..., x8)의12 BDD = xx3456 + xx78 + xx + xx + xx 의 잘못된 변수 순서를 사용합니다.

양호한 변수 순서 지정

실제로 이 데이터 구조를 적용할 때는 변수 순서에 주의를 기울이는 것이 매우 중요합니다.최적의 변수 순서를 찾는 문제는 NP-hard입니다.^[13]상수 c > 1에 대해 변수 순서를 계산하는 것은 NP조차 어렵습니다.그 결과,^[14] OBDD의 사이즈는 최적보다 최대 c배 커집니다.그러나 이 ^[15]문제를 해결하기 위한 효율적인 휴리스틱스가 존재한다.

그래프 크기가 변수 순서와 관계없이 항상 지수 함수인 함수가 있습니다.이것은 예를 들어 곱셈 ^[1]함수의 경우 유지된다.실제로 $2개$의$n개의 n비트$ 곱의 중간비트를 계산하는 함수에는 ${\displaystyle {\mathrm{2\mu n}/2\mu \mathrm{}}^{}61}$- 4$(\displaystyle 2^{\lfloor n$/2$\rfloor }/$61-4$}$^[16]개의 정점보다$$ $작은{\displaystyle {\mathrm{}}^{}}$ OBDD가 없습니다.(곱셈 함수에 다항식 크기의 OBDD가 있는 경우 정수 인수분해는 P/poly로 나타나며 이는 사실이 아닙니다.)^[17]

연구자들은 BMD(이진 모멘트 다이어그램), ZDD(제로 억제 결정 다이어그램), FDD(자유 이진 결정 다이어그램), PDD(패리티 결정 다이어그램), MTBDD(복수 터미널 BDD)와 같은 많은 관련 그래프에 자리를 내주는 BDD 데이터 구조에 대한 개선을 제안했다.

BDD에서의 논리 연산

BDD의 많은 논리 연산은 다항식 시간 그래프 조작 ^{[18]: 20} 알고리즘에 의해 구현될 수 있습니다.

• 접속사
• 분리
• 부정

단, 예를 들어 일련의 BDD의 결합 또는 분리를 형성하는 등 이러한 조작을 여러 번 반복하면 최악의 경우 BDD가 기하급수적으로 커질 수 있습니다.이것은, 2개의 BDD에 대해서 상기의 조작 중 어느 것이든, BDD의 사이즈의 곱에 비례하는 사이즈의 BDD가 되는 경우가 있기 때문에, 복수의 BDD에 대해서, 그 사이즈는 조작의 수에 있어서 기하급수적인 경우가 있습니다.변수 순서를 다시 검토할 필요가 있습니다.일부 BDD 세트에 대해 적절한 순서가 될 수 있는 것은 조작 결과에 대한 적절한 순서가 아닐 수 있습니다.또, 부울 함수의 BDD를 구축하면, NP완전 부울 만족도 문제와 co-NP완전 타우톨로지 문제가 해결되기 때문에, BDD의 구축은, BDD가 작은 경우에도 부울식의 사이즈의 기하급수적인 시간이 걸릴 수 있다.

감소된 BDD의 여러 변수에 대한 실존적 추상화 계산은 ^[19]NP-완료입니다.

BDD의 경우 Boolean 공식의 만족스러운 할당 수를 카운트하는 모델 카운팅을 다항식 시간으로 수행할 수 있습니다.일반적인 명제 공식의 경우 문제는 p-complete이며 가장 잘 알려진 알고리즘은 최악의 경우 지수 시간이 필요합니다.

「 」를 참조해 주세요.

• 부울 만족도 문제, 표준 NP 완전 계산 문제
• L/poly, 다항식 크기의^{[citation needed]} BDD에 대한 일련의 문제를 포함하는 복잡도 클래스
• 모델 체크
• 기수목
• 배링턴 정리
• 하드웨어 액셀러레이션
• 부울 대수식을 단순화하는 방법인 카르노 맵

레퍼런스

추가 정보

• R. Ubar, Proc의 "대안 그래프를 사용한 디지털 회로 생성 테스트(러시아어)"탈린 기술 대학교, 1976년, 제409호, 에스토니아 탈린, 탈린 기술 대학교, 75-81페이지.
• D. E. Knuth, "The Art of Computer Programming Volume 4, Faccle 1: Bitwise Tricks & Technologies; Binary Decision Diagram" (애디슨-Wesley Professional, 2009년 3월 27일) vi+260pp, ISBN 0-321-58050-8.패시클 1b의 초안을 다운로드 할 수 있습니다.
• Ch. Meinel, T.Theobald, "VLSI-Design: OBDD – Foundations and Applications", Springer-Verlag, 베를린, 하이델베르크, 뉴욕, 1998.전체 교재를 다운로드할 수 있습니다.
• 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.

외부 링크

• 이진 의사결정 다이어그램(BDD), Donald Knuth 강의
• 여러 프로그래밍 언어의 BDD 소프트웨어 라이브러리 목록입니다.