VLSI CAD: Logic to Layout Lecture 014 Sat For Logic

[음악] 그래서, 강의 4

3에서 우리는 전산 부울 대수학에 대한 탐험을 완료하십시오 Boolean SAT에 대한 토론 그리고 지금까지 우리가 본 것은 높은 수준, CNF 형식으로 SAT 문제를 표현하는 방법 및 부울 제약 조건 전파는 만족성에 대한 질문에 대답하는 데 도움이 될 수 있습니다 또는 불만족 하지만 당신이 아직 모르는 부분은 사실 논리 게이트의 현실적인 네트워크를 가져 와서 이것을 조금만 바꾸면됩니다

이상한 찾고 CNF 양식 그리고 실제로 내가 어떻게 포즈를 취할 것인가? 엔지니어링 관련 질문,이 두 가지 구현은 큰, 논리 게이트와 같은 복잡한 부울 기능,이 두 가지가 동일하거나, 안 그래? 무슨 일이야? 실제 상황에서 벗어나기위한 놀랍도록 간단한 기계 절차가 있음을 알 수 있습니다 게이트와 와이어가있는 논리를 CNF 형식으로 만듭니다 그래서 우리는 그것을 살펴보고 부울에 대한 토론을 완료 할 것입니다 이 강의에서 만족할만한 성질을 보여줍니다

나는 실제로 그것이 실제로 처음에는 좋다고 생각한다 조금 뒤로 물러서 라 이번 주에 우리가 실제로 한 일 때문에 물론, 이번 주 전반기에 우리는 이진 결정을했습니다 다이어그램을 작성하고, 주 후반기에는 부울 만족 성을 수행했습니다 그것들이 동일하지 않다는 것을 아는 것이 중요합니다

그들은 무료입니다 그래서 이것은 일종의 슬라이드입니다 당신도 알다시피, 그들은 정말로 평등하지 않습니다 알다시피, 그들은 아니에요 정확히 같은

그리고 두 가지를 아는 것이 중요합니다 그래서 우리는이 한 주 전체를이 중요한 두 가지 주제에 보냈습니다 그러니 Bdd는 종종 많은 문제에 대해 잘 작동하지만, SAT는 종종 많은 문제에서 잘 작동합니다 그러나 둘 다 항상 효과가 있다는 보장은 없습니다

죄송합니다 그것은 바로 사물을 해결하는 본질에 있습니다 기하 급수적으로 힘들어서 때로는 당신의 경험적 기법이 작동하지 BDD의 경우 기본적으로 우리가 할 수있는 일은 우리는 기능을 표현할 BDD를 구축 할 수 있을지도 모릅니다 그리고 SAT 측면에서 우리는 예 또는 아니오로 만족감을 해결할 수 있습니다

그 기능 그리고 그 것들은 정말로 다릅니다 소지품 괜찮아 이제는 BDD를 구축 할 수없는 경우가 있습니다

합리적인 컴퓨터 자원 그리고 일반적으로 발생하는 것은 당신이 부족합니다 메모리의 당신은 단지 기가 바이트가 충분하지 않습니다 BDD를 작성하십시오

그리고 SAT 측면에서, 때때로 당신은 할 수 없습니다 SAT 솔루션을 찾으십시오 만족스러운 과제를 찾을 수 없거나 합리적인 컴퓨터 자원으로 존재하지 않는다는 것을 증명하십시오 일반적으로 시간이 없습니다 너 알다시피, 너 그냥 방금 검색하는거야

검색 및 검색 및 검색 및 당신은 그냥 완료하지 마십시오 따라서 기억해야 할 사항 중 하나는 BDD가 실제로 빌드하는 것입니다 함수의 완전한 표현 그것은 모든 것을 나타냅니다 사실, 함수의 표준 표현입니다

이것은 실제로 BDD에 관한 멋진 것들 그러나 SAT 해결사는 전체 기능 말하자면, 그들은 그것을 대표하지 않는다 크고 풍부하고 아름다운 조작을 지원하는 방식으로 불리언에 일종의 임의의 종류의 계산적인 일을하고 싶습니다 기능

BDD로 시작하는 것이 좋습니다 당신이이 풍부한 팔레트를 가지고 있기 때문입니다 하지만, 그냥 부울 함수를 풀고 싶다면 말하자면, 할 수 있을까요? 0? 예 또는 아니오, 사용하고자 할 때입니다 SAT 예를 들어, 실존 적 및 보편적 인 양을 나타내는 함수

그것은 BDD에서 할 수있는 조작 방법 중 하나입니다 우주 SAT 우주에서, 그것은 SAT 솔버의 버전은 실제로 다릅니다 모든 SAT 솔버가 아니지만 SAT 솔버 버전이 있습니다 그들은 정량화 된 SAT 솔버라고 불리며, 여러분이 말할 수 있습니다

기능을 사용하면 CNF 형식으로 그에게 줄 수 있습니다 그리고 나서 여러분은 말합니다 그리고 여기에 계량화하고자하는 변수들이 있습니다 부디 그리고 SAT 해결사는 흥미로운 일을합니다

내부 마법을 사용하고 정량화 된 기능에 대한 만족 성을 해결합니다 그것은 SAT 솔버의 완전히 다른 범주입니다 그러나 SAT 솔버를 사용하여 임의의 부울 연산을 수행 할 수는 없습니다 SAT를 풀 수 있습니다 그것이 그들이하는 일입니다

부울 함수에서 임의의 작업을 수행하려는 경우 BDD가 필요할 수 있습니다 BDD로 SAT를 할 수 있습니다 아마 그럴 것입니다 효율적인 방법 괜찮아? 그렇게 중요한가? 어쩌면 약간의 미묘한 세트 구별하지만, 알다시피, 만약 당신이 이것을 내면화 시키면

당신은있을 겁니다 당신은 존재를 향한 진전을 이루게 될 것입니다 심각한 [알 수없는] 사람입니다 알다시피, 전형적인 실용적인 것은 무엇입니까? 토 문제가 있습니까? 두 가지 논리 네트워크가 있습니다 그리고 그것들은 똑같은 입력의 로직 네트워크입니다

같은 부울 함수인지 확인합니다 나는 F가 G와 정확히 똑같은 일을하는지 알고 싶습니다 그래서 저는 단지 G가 F라는 질문을하고 있습니다 어떻게 그걸합니까? 글쎄, 당신은 일반적으로 수행원 출력 쌍마다, 그냥합시다

F1이 G1이라고 가정한다 그들은 같은 일을하기로되어있다 맡은 일 그리고 F2는 G2로되어 있습니다 그들은 똑같은 일을하기로되어 있습니다

출력 쌍마다 Exclusive OR Gate를 넣습니다 그래서 당신은 거기에 F1과 G1을 넣습니다 그리고 여기에 또 다른 Exclusive OR Gate와 거기에 F2를 놓고 거기에 G2를 놓습니다 자, 잠깐 생각 해보자 Exclusive OR Gates를 만드는 것은 무엇입니까? 1

F와 G 입력이 일치하지 않으면 대답이됩니다 괜찮아 그래서 이걸로 1을 만드는 유일한 방법은 XOR 게이트는 F와 G가 같은 기능을 갖지 않도록하는 것입니다 승인 그래서, 우리가 여기서 무엇을 찾고 있습니까? 우리는 하나의 OR 게이트를 찾고 있습니다

승인 그걸 Z라고 부르 자 그리고 진실은 무엇인가? 자, 사실은 Z가 1이 될 것입니다 그것은 만족할만한 것입니다, 맞죠? 우리는 X의 패턴을 찾을 수있을 것이다 그것은 F가 G와 같지 않은 경우에만 Z를 1로 만듭니다

권리? 그 말이 맞죠? 그리고 우리가 Z를 만족스럽게 찾을 수 있다면 권리? 그러면 우리는 속성을 가진 X를 찾을 것입니다 권리? 그건, 알다시피, F X는 G가 X를 사용하는 것과 동일하지 않습니다 적어도, 알다시피, 그 중 하나, 그 중 하나 인 것입니다 입력이 다를 것입니다

그렇게 멋진 데, 맞죠? 나는 두 개의 큰 복잡성을 가지고 있습니다, 당신도 알다시피, 실제 공학 논리의 조각들입니다 그리고 나는이 두 가지가 똑같은 일을하고 있다고 말하고 싶습니다 독점적으로 또는 관련 출력, 또는 모든 독점적 OR을 함께 사용하면 부울 satisfiability 그것을 해결하는 질문 이봐, Z를 1로 할 수 있을까? Z를 1과 같게 만들면 네트워크가 동일하지 않습니다 이 입력 패턴은 출력을 다르게 만듭니다

그리고 이것이 사실 일뿐만 아니라 입력 X를 얻을 것입니다 실제로 F와 G가 다르게 만들어서 디버깅 도구로 유용 할 것입니다 그리고 그것이 만족스럽지 않다면, Z가 항상 0이면, 그렇습니다 그들은 사실 동일한 논리입니다 그들은 똑같은 일을하고 있습니다

그래서 아주 멋집니다 그러나 그것은 많은 질문을 제기합니다 그리고 첫 번째 질문은 게이트 레벨 설명으로 시작하여 CNF? 이게 어렵지 않니? 권리 부울 대수가 필요하지 않습니다 BDD 또는 뭔가 복잡한가? CNF 양식은 조금 이상합니다

아시다시피, 조금 어색함을 느꼈습니다 그리고 내가 50,000 게이트가있는 거대한 논리 네트워크를 가지고 있다면, 그렇지 않습니다 그게 끔찍한가? 대답은 '아니오'입니다 사실, 정말 쉽습니다 그것은 놀랍게도 쉽습니다

그러나 우리는 약간의 기술을 구축해야합니다 약간의 수학이 필요합니다 우리를 거기에 데려와 이제 살펴 보도록하겠습니다 여기에 약간의 논리 네트워크가 있습니다

NAND 게이트에는 1과 2가 두 개 있습니다 입력 및 NOR 게이트 번호 2를 포함한다이 회로의 3 개의 입력 중, 그 중 하나는 게이트 1과 게이트 2간에 공유됩니다 게이트 1은 인버터 3 번 게이트로 가고, OR 게이트 4 번 게이트의 한 입력으로 간다 또한, 게이트 (2)는 게이트 (4)의 다른 입력이다

그리고 게이트 5는 인버터 3과 OR 게이트 4의 출력을 취하는 AND 게이트이고, 그게 다야 그래서, 어떻게이 CNF 일을합니까? 큰 멋진 간단한 아이디어는 당신이 CNF 하나의 게이트를 시각 그래서 개념을 소개해야합니다 개념은 우리가 호출 할 게이트 일관성 기능입니다 전체가 함수라고하면, phi라고하는 것입니다

게이트 일관성 기능은 출력의 하위 이름입니다 자,이 NAND 게이트가 여기 있다고 가정합시다 입력 a와 b가 있습니다 d라는 출력이 있습니다 그래서 게이트 일관성 기능은 다음과 같습니다

phi d라고합니다 그리고 이것은 실제로 d 값과 같습니다 게이트의 기능에 자 여기 기억하십시오 이 문이 정말로하고있는 것

이 게이트는 NAND 게이트입니다 그래서 그것은 바입니다 그것이 바로이 문이하는 일입니다 그래서 이것은 실제로 우리가 출력물에 사용하는 상징 이상의 것입니다 gate,이 게이트가 가정 한 부울 수식이있는 Exclusive NORd ab 바입니다

그리고 당신이 조금이라도 부울을한다면 이것을 단순화하면 더하기 d, b + d, 바 + b 바, d bar이고 이것은 phi sub d와 같습니다 자, 알았어 내가 왜 이러는거야? 있잖아,이게 무슨 소용 이니? 이것은 정말로, 정말로, 당신도 알다시피, 마법의 작은, 조금 도움이되는 것으로 밝혀졌습니다 실제로 우리가 전체 네트워크에 대해 CNF를 얻을 수있게 해주는 도우미 기능 얼마나 복잡한 지, 한 번에 하나의 문 그래서 처음에는 약간의 리뷰를했습니다

여러분 모두 알고 있습니다 독점적 인 OR, XOR 아시다시피, 우리는 더하기 기호 B로 동그라미로 작성합니다 a와 b가 다른 경우에만 출력이 1입니다 괜찮아? 권리 그래서 그것이 일반적으로이 게이트입니다

그것의 또 다른 술집과 OR 게이트의 종류입니다 A와 B는 입력 값입니다 Y가 출력이라고합니다 이것은 Y가 막대 b와 AB 막대를 더한 것과 같습니다 그래서 이것은 1을 만드는 문입니다

그것의 입력은 다르다 독점적 인 노어 나는이 방법으로 그것을 쓰고 싶다 나는 그것 위에 막대기와 함께 독점적 인 OR 문으로 그것을 쓰고 싶다 다른 사람들은 주위에 원과 함께 AND 함수처럼 그것을 쓰고 싶습니다 나는 아니에요, 그게 아니에요

그것은 개인적인 취향입니다 다시 NOR 게이트이지만, 거품이 그려져 있습니다 독점 노어 그것은 두 개의 입력 A와 B를 가지고 있으며, 다시 한 출력 Y 그리고 A는 미안 해요 Y, 출력 1, 입력이 같아도됩니다

권리? 그리고 이것은 Y 플러스 AB 플러스 바, B 바입니다 그리고 당신은 부울에서 볼 수 있습니다 수식은 그들이 독점적 인 OR은 단지 그들이 다르다면 1입니다 배타적 NOR는 동일하다면 1입니다 그래서 일종의 알림입니다 권리

그리고 게이트 일관성 기능은 심볼의 배타적 NOR입니다 게이트 출력 부울 수식을 사용한 독점 NOR'D 게이트가하는 것의 자, 그게 뭐지? 실제로 다소 좋은 것입니다 게이트 일관성 함수는 1을 만듭니다 입력과 출력의 조합에만 해당됩니다

게이트가 실제로하는 것과 일치합니다 그리고 그것이 의미하는 것은 게이트 일관성 기능이 흥미 롭습니다 당신이 a에 넣을 수있는 작은 물건과 ab에 넣을 수 있습니다 광고 및 게이트 일관성 기능은 1을 말합니다 예, 게이트가 수행하는 것 또는 0, 아니, 그건 문이하는 게 아니야

예를 들어, 내가 a를 0, b를 a 0과 d는 1? 음, 이것은 NAND 게이트입니다 그래서 저는 여기에 0을 넣었습니다 나는 여기에 0을 넣었다 0과 0은 0입니다 반전 된 0은 1입니다

네, 사실 저는 1을 만들어야합니다 이것은 일관성이 있습니다 그리고 계속하십시오 시도 해봐 당신이 발견 할 수있는 것은 당신이 이것을한다면, 피는 1입니다

Phi d는 예라고 말하고 a는 0, b는 0, d는 1입니다 네 확실합니다 그것이이 게이트의 역할입니다 그러나 만약 당신이 대신했다면, 이것 2 대 1을 넣으면 어떨까요? 1 및 1은 1입니다

반전 된 1은 0입니다 불행히도, 나는 방금 내가 생각한다고 말했다 이것은 일치하지 않습니다 실제로 여기서 일어날 일은 바로 그것입니다 φd는 0이 될 것이다

권리? 피디가하는 일입니다 피는 이봐 요, 이거라고 말하는 기능입니다 문은 무엇을합니까? 당신이 정말로 필요로하는 모든 것이 전체 게이트 네트워크에 대한 적합성 공식을 만들려면 어떻게해야합니까? 함께 그리고 함께 모든 게이트 일관성 기능을 게이트 일관성 기능 중 하나는 기본적으로 입력을 출력에 연결합니다 대부분의 게이트에서 출력은 다음 게이트의 입력입니다 권리? 그리고 이것은 이것이 절이 서로 붙어서 값이 모두 겹치게됩니다 따라서 전체 함수를 1로 만드는 유일한 방법은 일관되게 끝까지

그 흥미있는 믿어지지 않는 정도로 실제적인 개념 따라서 논리 네트워크의 경우 각 와이어에 라벨을 붙이십시오 모든 것, 맞죠? 여기에이 네트워크의 입력이 있습니다 여기에이 네트워크의 출력이 있습니다 그리고 이것은 이전의 동일한 논리 네트워크입니다

게이츠 1, 2, 3, 4, 5 1은 NAND이며, ab 출력을 입력합니다 d 2는 NOR, 입력 bc 출력 e입니다 3은 입력되지 않습니다 d 출력 f

4는 OR, 입력 출력 g입니다 5는 AND, 입력 fg 출력 h입니다 모든 단일 내부 라벨에 라벨을 지정해야합니다 변수 이름을 가진 철사 권리? 그 이유는 모든 단일 항목에 대해 부울 수식을 작성하게 될 것이기 때문입니다

문 따라서 모든 입력과 모든 출력에는 이름을 그래서, 우리가하고 싶다고 가정합시다 g 용 좋아, 그럼 내가 원하는 건 내가 나야

그 문을 봐야 해 좋구나 그래서 그것들은 이름을 필요로하는 내부 노드입니다 그리고 그것은 이름을 필요로하는 내부 노드입니다 그래서 이것은 OR 게이트 인 게이트입니다

그 안에 d와 e가 들어갑니다 그리고 그것에서 나가고있어 우리가 실제로이 일을한다면, 게이트 일관성 함수, phi g는 g의 출력 이름이 될 것입니다 그리고 이것은 Exclusive NOR'd가 될 것입니다 것은하고, 그것은 d + e입니다

우리가 실제로 그것을 연마한다면, 우리는 그것을 발견 할 것입니다, 그것은 d bar plus g ANDed e bar plus g, ANDed d plus e 플러스 g 바 그리고 거기에 우리가 가지고 있습니다 그리고, 당신도 알다시피, 다른 이들 중 일부는이 작업을 수행할만한 가치가 있습니다 당신의 손을 시험해보고 여기에서 무슨 일이 벌어지고 있는지 스스로 깨닫게하십시오 그럼, 우리는 다음에 무엇을해야합니까? 전체 CNF를 얻으려면 net list, 당신이하는 일은 다음과 같습니다

이 CNF를 작성하십시오 좋아, 파이 그리고 두 부분으로되어 있습니다 실제로 출력 변수를 절의 하나에 넣어야합니다 그리고 실제로, 출력 변수가 있습니다

그리고 실제로 거기에 넣어야합니다 바로 거기에 있습니다 그리고 아이디어는 우리가 모든 것을 만족시킬 수 있는지를 해결한다는 것입니다 그 중 하나는 h가 하나라는 것이 진실이어야한다는 것입니다 그리고이 절 데이터베이스에서 h가 1인지 확인하는 방법은 h가 1 인 경우에만 만족할 수있는 h가있는 절

권리? 그리고 나서 그것은 제품을 가지고 있습니다 제품이란 네트워크의 모든 게이트를 통해 큰 AND를 의미합니다 그런 다음 게이트를 일관성 기능 그것은 phi k가있는 것입니다 그리고, 게이트 1에 대해서는 게이트 일관성 기능이 있고, 게이트 1에 대해서는 게이트 일관성 기능이 있습니다

게이트 2에 대한 일관성 기능, 게이트 3에 대한 게이트 일관성 기능 게이트 (4)에 대한 게이트 일관성 기능, 게이트에 대한 게이트 일관성 기능 5 맞아 그래서 같은 논리 네트워크, NAND 게이트 1, NOR 게이트 2, NOT 게이트 3, OR 게이트 4 AND 게이트 5, 똑같은 그리고 나는이 멋진 큰 절 CNF를 얻었다 형식으로 문자 그대로 읽을 수 있습니다

게이트 1은 게이트 일관성 기능을 만듭니다 빵, 내려 놔 게이트 2는 게이트 일관성을 만듭니다 기능 빵, 내려 놔

게이트 3은 게이트 일관성 기능을 만듭니다 내려 놔 4 개를 내려 놓으십시오 그 중 하나를 내려 놓으십시오 하나의 절을 넣으십시오

출력 변수입니다 당신은 그것을 가지고 있습니다 이것은 귀하의 로직 네트워크를위한 CNF입니다 게이트와 전선에서 할 수 있습니다 네트워크를 걷는 것

그래, 꽤 커질거야 죄송합니다 그것이 작동하는 방식입니다 SAT 해결사에게 건네주십시오 당신이하고 싶은 질문을하십시오

따라서, 각각에 대해서가 아닌 실제 부울 대수 단순화를 읽지 마십시오 개별 게이트 레벨 기능 그리고 네트워크 수준에서 당신과 그들 모두 함께 이제이 결과로 영리한 사람들 수식을 작성했습니다 계속해서 진행해야하기 때문에 지루합니다

이것들을 파생시킨다 그리고 이것은 아주 복잡한 슬라이드입니다 그래서 나는 Fadi Aloul, Igor에서부터 꽤 유명한 논문에서이 공식들을 얻었습니다 마르코프, 카렘 사 칼라 미시건 대학의 모든 곳 그들은 SAT로 흥미로운 것들을 해보기 만했습니다

다음은 수식입니다 흥미롭게도 공식이 있습니다 충분하고, 철사 때때로 너는 전선이있어 당신은 한 게이트의 출력을 가지는데, x와 입력을합시다 다음 게이트의 이름이 z라고하자

그리고 당신은 부울 함수, z는 x와 같습니다 당신은 그것에 대한 부울 CNF 수식이 필요합니다 X 바 플러스 z, x 플러스 z 바 그런 다음 NOR 게이트 용 수식이 필요합니다 OR 게이트들, NAND 게이트들, AND 게이트들, 및 인버터들을 포함한다

인버터는 간단합니다 X 플러스 z, x 바 플러스 z 바 나머지는 모두 복잡합니다 그리고 그들은 일종의 복잡하지만 그것도 일종의 단순합니다 그들은 모두 정확히 세 부분을 가지고 있습니다

그럼 예를 들어 보겠습니다 문 첫 번째 부분은 제품입니다 그리고 그것은 모든 입력에 대한 제품입니다 n 개의 입력이 있습니다

그리고이 제품은 xi bar plus z bar입니다 4 개의 입력 NOR 게이트가 있다면 4 개의 제품을 얻을 수 있습니다 모두 xi bar plus z bar처럼 보입니다 그리고 나서, 그것은 합계 항과 ANDed됩니다 그 안에는 두 가지가 있습니다

권리 그래서 이것은 합계입니다, 이것은 당신이 알고있는 OR입니다 이것은 모든 입력의 OR입니다 그래서 4 개의 입력이 있다면, x1, x2, x3, x4 이것은 x1 + x2 + x3 + x4입니다

그리고 나서이 합계에 하나의 용어가 있습니다이 경우에는 z 기간 그리고 각각의 방정식을 보면 NOR 또는 NAND의 경우, 어디에서 발견 되는가에 따라 달라질 수 있습니다 보완 바, 바가 어디 있는지, 당신은 알고 있습니다 그리고 그것은 당신이 독점적 인 기능을 수행하고 기능의 대수를 갈아 치워 라

이것은 단지 패턴입니다 그래서, 기억할 가치가 있습니다 또는 아시다시피 손등에 적어 두십시오 나는 그것이 더 좋은 대답일지도 모른다라고 생각한다 이제, 내가 할 다른 한 가지, 내가 할 것이다

인정해라 그리고 이것은 불행한 일이다 그러나 당신은 알고있다, 나는 EXOR 게이츠가 어떻게 당신에게 말해야한다 EXNOR 게이트는 게이트 일관성 기능도 가지고 있기 때문에 작동합니다 그리고 문제는 EXOR 게이트이며 EXNOR 게이트는 SAT에 대해 다소 불쾌합니다

해결사 이 기본 구조는 어떤 거친 SAT 수색을 위해 그들은 오히려 큰 게이트 일관성 기능을 가지고 있습니다 너무 따라서 작은 두 입력 게이트 만 생성됩니다 많은 용어들

그래서 여기에 무슨 일이 일어나는가가 있습니다 z가 Exclusive OR와 동일한 경우 a와 b의 게이트 레벨 일관성 기능은 z XNOR ax 또는 b입니다 b 조금 불쾌한 부울입니다 대수학

나는 단지 너를 위해 그것을 쓰고있다 XNOR에 대한 정보를 알아내는 것이 좋습니다 우리는 그렇게 할 필요가 없습니다 원한다면 더 많은 공식을 도출 할 수 있습니다 입력

그것은 단지 불쾌한 일입니다 그것은 단지 크고 추한 것입니다 하지만 이제 알다시피, 당신은 게이트 레벨을 가지고 있습니다 알고 있어야 할 모든 게이트에 대한 일관성 기능 그리고 부울 표현식, 부울 논리 네트워크를 걸을 수 있습니다 게이트 레벨 일관성 기능을 구축 할 수 있습니다

그리고 그것은 단지 가치있는 것입니다 알다시피, 여기에서 하나를하는 것입니다 단지 설득력있는 것입니다 우리는 우리 자신을 압니다 여기에 일반적인 공식이 있습니다

n 입력 NAND 게이트 제품 용어가 있고 그것은 총계 기간과 ANDed이고, 하나의 추가 기여 기간이 있습니다 관련 출력합니다 n이 2 일 경우 어떻게됩니까? 권리? 당신은 무엇을 얻습니까? 여기에 제품 용어가 있습니다 권리? 이 제품은 AND를 의미하기 때문입니다

그리고 n은 2이기 때문에 권리 i의 제품은 xi의 1 – 2와 같습니다 더하기 z는 x1 + z와 x2 + z입니다 그게 전부입니다

그리고 나서 총항 (sum term)이 있습니다 그리고 다시, n은 2와 같습니다 그리고 이것은 i가 1에서 n까지의 합계입니다 그리고 합계는 OR을 의미합니다 권리? 여기에 한 가지 추가 용어가 있습니다

그래서 i의 합은 xi의 1과 2가 같습니다 bar는 x1 + x2가 아닙니다 그리고 나서 우리는 여전히 같은 액수 안에 있습니다 그리고 거기에는 언제나 하나의 용어가 있습니다이 경우 z 바입니다

그래서 이것이 여러분이이 공식을 읽는 방법이며, 여러분이 그것을하는 방법입니다 그것은 전부 기계적입니다 실제로 아무도 이것을 손으로하지 않습니다 당신은 프로그램을 쓴다 우리는 실제로 당신에게 글쓰기를 요청할 것입니다

네가 알기 때문에 네 인생에서 한 번 해보니 좋다 너도 알다시피, 3 ~ 4 개, 5 개의 게이트가있다 생성되는 것, 아시다시피, 10 개 또는 15 개의 조항 당신이 그것을 기계적으로 할 때, 당신도 알다시피, 종이와 연필 형태 저를 믿으십시오, 당신은 그것이 어떻게 작동하는지 알 것입니다

그렇기 때문에 부울 만족을 위해서입니다 그것은 매우 중요한 기술이며 BDD와 함께 꽤 많이 사용됩니다 표현의 종류와 큰 종류의 우주의 종류를 나타냅니다 불리언 방정식을위한 전산 도구 저는 SAT가 실제로 이진 결정 다이어그램을 많이 옮겼습니다

그저 놀라 울 정도로 큰 응용 프로그램 집합 만 해결하면됩니다 그것 나는 말할 필요가있다 이 큰 불리언 함수에 대한 할당을 만족시키고 있습니까? 네, 저 하나주세요 아니, 알았어

알 필요가있어 그래서 SAT를 만드는 형식으로 변형 된 많은 것들이 있습니다 선호되는 기술이지만 BDD는 여전히 중요합니다 장소 SAT의 가장 큰 이유는 확장 성

거대한 문제를 일으킬 수 있습니다, 50,000 변수, 2,500 만 조항, 5 천만 조항, 5 천만 조항 권리? 죄송합니다 당신이 알고있는 5 천만 개의 리터럴, 조항에 변수가 나타납니다 그러나 여러분도 알다시피 말 그대로, 수 만개의 변수, 수천만 절 그것들은 거대한 문제입니다 당신은 실제로 그러한 것들을 현저하게 빨리 해결할 수 있습니다

BDD와 같은 여전히 ​​SAT는 아닙니다 적당한 시간 또는 공간 아이디어는 40 ~ 50 년 전의 것입니다 당신이보고있는 종이에 따라 그러나 여전히 큰 아이디어입니다

Davisputnamlogemannloveland는 재귀의 계산적 내장의 일종 그러나 그것을 가능하게하는 몇 가지 놀라운 엔지니어링 진보가있었습니다 엄청나게 빠르다 그리고 우리는 실제로 경기에 나설 것입니다 이것으로 일부 숙제를합니다

내가 끝내기 전에,이 강의 리프, 나는 내 친구 중 일부에게 약간의 인정을하고 싶었습니다 Karem Sakallah는 미시건 대학교의 제 친구입니다 나는 미시간 대학 명반 대학이라고 인정할 것이다 나처럼 클로드 섀넌과 카렘은 너와 함께 매우 관대했고 시간과 이 강의 자료의 아주 초기 버전에 입력합니다 그리고 그의 이전 PHDA 학생 인 Joao Marques-Silva는 충돌 학습에 대한 가장 초기의 연구는 내가 이것을 사용하고있는 서류들

그리고 그는 현재 University College에 있습니다 더블린 두 사람 모두에게 큰 감사를드립니다 이 강의를 도와주었습니다 그리고 이제 우리는 사물을 종합하는 것에 사물을 나타냅니다

이것이 바로 우리의 다음 큰 주제입니다 [음악]