VLSI CAD: Logic to Layout Lecture 013 Sat Part 2

[음악] 그래서 여기 우리는 강의 42에 있습니다

우리는 계속 작업 할 것입니다 전산 부울 대수 (boolean algebra)에 대한 논의를 계속할 것입니다 부울 적합성 또는 SAT 마지막 강의에서는 Conjunctive Normal Form, CNF로 표현 체계 그리고 이제 우리는 어떻게 실제로 하나의 조항으로 시작할 것인가를 보여줄 것입니다

CNF 양식을 작성하고 만족 스러운지 여부에 대한 질문에 대답하십시오 그리고 우리는 놀라지 않을 것입니다 그것은 재귀적인 계산의 또 다른 종류입니다 그러나 더 중요한 것은, 매우 강력하고 중요한 반복적 인 좀 더 많거나 적다면, 특정 변수가 가지고 있다고 가정 해 봅시다 가치, 그리고 무슨 일이 일어나는 지 보자

부울 수식이있는 경우 많은 변수와 많은 변수, 많은 변수, 많은 변수가 있습니다 이 간단한 절차로 수행 된 작업 그리고 이것을 부울 제약이라고합니다 전파 또는 BCP 그리고 우리가 다음에 이야기 할 내용은 BCP가 어떻게 작동하는지

그래서 마지막 강연에서 우리는 부울 satisfiability 두 가지 큰 부분을했다 결정을 내 렸습니다 변수에 어떤 값을 임의로 설정하기는 어렵습니다 그리고 우리는 CNF 양식을 간소화하고 어떤 일이 일어나는지 봅니다 우리는 그것을 만족시킬 수 있습니까? 아니면 우리가 갈등합니까? 문제는 그것이 지금까지만 갈 것이라는 것입니다

일부 변수는 값을 가지므로 그 값을 추론 할 수 있습니다 다른 변수에는 값이 있어야합니다 그리고 그것은 정말로, 정말로 정말 큰 부울 함수에 대한 CNF의 큰 인스턴스, 거대한 가능한이 공제액 사실, 이것은 실제로 모든 부울의 만족성에 깊은 일이 일어납니다 그리고 이것은 물건이 이름을 가지고 있다는 것을 의미합니다

부울 제약이라고 불립니다 번식 그래서 주어진 고정 변수 집합 과제, 다른 과제에 대해 당신이 추론 할 수있는 다른 것 변수? 글쎄, 당신은 전파함으로써 그것을 할 수있다 제약 조건 이제는 매우 유명한 전략이 있습니다

이것은 Unit Clause Rule이라고 부르며, 이것은 50 세와 같습니다 하나의 할당되지 않은 리터럴이 정확히 있다면 절이 단위라고합니다 그래서 단위 절은 여러분이 그것을 만족시킬 수있는 한 가지 방법을 가지고 있습니다 즉, 1 절의 극성을 선택해야합니다 당신은 선택의 여지가 없습니다, 당신은 임의로 그 극성을 선택하지 않아도됩니다

문자 그대로 그 선택을 암시라고합니다 그래서 여기에 약간의 부울 함수 phi, a plus c, b plus c, a plus a not b plus 우리가 이러한 선택을하기로 결정했다고 가정합시다 그래서 a는 1이고 b는 1입니다 그래서 우리는 무엇을 압니까? 첫 번째 절에서 a는 1이므로 해당 절이 충족됩니다 나는 그것에 대해 걱정하지 않을 수 있습니다

그리고 두 번째 절에서 b는 1입니다 그 조항은 만족스럽고, 그것에 대해 걱정하지 않을 수 있습니다 그러나 세 번째 절에서 a는 0이됩니다 b 항은 0이됩니다 무슨 일이 일어난? 이 조항은 단위가되었습니다

정확히 하나의 할당되지 않은 리터럴이 있기 때문에 단위입니다이 경우에는 C 바 그래서 내가 아는 것은, 나는 c가 반드시 있어야한다는 것을 안다 0이어야합니다 왜냐하면 유일한 방법은 이 절을 만족시킬 수있는 것은 c가 0 인 경우입니다

그리고 그 절은 1이됩니다 만약 내가 정말로이 불리언을 만족 시키길 원한다면 나는 a와 b에 대한 결정 때문에, 나는 추론했다 그 의미에 의해, c는 0이되어야합니다 그것은 거대한 CNF에서 실제 산업 회로라면 이러한 단위 절을 엄청나게 추론 할 수 있습니다 당신은 수천 개의 변수 값을 추론 할 수 있습니다

모든 실제 SAT 엔진에서 진행됩니다 일종의 방법을 살펴 보겠습니다 일할 수도 있습니다 그래서 여기에 약간의 예가 있습니다 이것은 내 친구들 John이 체크 아웃 할만한 가치가있는이 논문의 한 예입니다

마르케스 실바와 카렌 사 칼라 둘 다 대학에 있었을 때 완료 미시간 Marques는 현재 Dublin에 있습니다 그래서, phi, 내 작은 부울 함수는 9 개의 절이 있습니다 오메가 1, 오메가 2, 3, 4, 5, 6, 7, 8, 9

9 절 그리고 오메가 1, 아니 x1 플러스 x2 오메가 2, 아니 x1 플러스 x3 플러스 x9 오메가 3, x2 플러스 x3 플러스 x4, 오메가 4, x4 플러스 x5 플러스 x10, 오메가 5 아니 x4 플러스 x6 플러스 x11, 오메가 6, x5 플러스 x6, 오메가 7, x1 플러스 x7 플러스 x12, 오메가 8, x1 + x8 오메가 9 x7 플러스 x8 플러스 x13 아니

이런 이러한 것들이 만족 스러운가? 그리고 그것이 힘든 일이라면 상상해보십시오 13 개의 변수가있는 함수에 대해 13 개의 변수가 무엇인지 상상해보십시오 이것이 우리가 알고리즘과 질문에 대한 전산 접근법을 필요로하는 이유입니다 이러한 문제를 해결합니다

그럼 어떻게 시작하니? 우선, 다소 임의적으로 부분 할당 x9, 10, 11을 수행해 봅시다 x12 및 13은 여기에 표시된 부호있는 값이고 x9, 10, 11은 0, x12 및 1은 13입니다 우리는 함수의 절을 살펴볼 것입니다 이러한 값을 삽입하여 단순화하십시오 그래서 여기에 우리가 간다

9, 10, 11, 12, 13 값을 삽입했습니다 그래, 무슨 일이 일어나고 대답은 그다지 발생하지 않는다 나는이 조항들 중 어느 것도 만족시킬 수 없으며,이 조항들에 분쟁이있다 기본적으로 여기에 단위 절이 없습니다 이 운동의 흥미로운 부분

나는 거의 아무것도 할 수 없다 나는 지금 무엇을 말할 수 있으며 대답은 내가 결정해야 할 것 같아 흥미로운 것이 없으므로 임의로 변수 값을 설정해야합니다 여기에서 일어났습니다 나는 당신이 정말로 모르고 있었고, 나는 그렇지 않았습니다

아무 것도 결론 지을 수 없었다 좋아, 그럼 우리가 다음에 무엇을 할거야? 변수에 값을 할당하도록 선택할 것이므로 x1을 1로 지정하십시오 그래서, 저는 다시 부울로갑니다 여기 방정식과 나는 지난 라운드의 모든 이전 과제를 가졌어 회색으로 표시되고이 값을 할당 할 것입니다 그리고, 오메가 1과 오메가 2 절에서 x1 항이 0이됩니다

그리고 오메가 7과 오메가 8 절에서 x1 항은 1이됩니다 오, 이거 좋은데 이것은 도움이됩니다 두 절, 그리고 여기에이 동그라미를 긋겠다 처음 두 절에서 절의 오메가 1에 속한 유닛 x2는 홀로 존재합니다

값없이 나는 그것이 무엇이되어야 하는지를 안다 그것은 1이되어야한다 그리고 x3에서는 오메가 2에서 유감입니다 x3은 값이없는 유일한 변수입니다

그렇지 않으면 0이고 그래서 x3은 1이되어야한다는 것을 알게됩니다 그래서, 내 단위 조항 규칙은 나에게 뭔가를 알아 낸 것 같아 X2는 1이되어야하고 x3은 1이되어야합니다 그렇지 않으면 더 이상 진전을 이루지 못합니다 마찬가지로 오메가 7에서는 x1을, 오메가 8에서는 x1을 사용해야합니다

이 두 절은 만족 스럽습니다 나는 그들에 대해 걱정하지 않을 수있다 훌륭합니다 그래서 이봐, 내가 실제로 만든 것 같은 느낌이야 진행

내 조항 중 두 개가 내 목록에서 제외되었습니다 내가 걱정해야 할 것들 오메가 7과 오메가 8 내 절 중 두 개가 단위 였기 때문에 두 개 더 내 목록에서 제외되었습니다 나는 그들에게 무슨 일이 일어나는 지 압니다

X2와 x1은 또는 x2와 x3입니다 죄송합니다 1 앞으로 나아가고 무슨 일이 일어나는 지 봅시다 그래서 여기 있습니다

나는 다시 모든 것을 회색으로 표시했다 우리가이 시점까지 얻었던 과제, 그리고 실제로 x2를 1로 설정하려고합니다 x3에서 1로 그래서, 어떻게되는지 봅시다 그리고 이것은 여러분이 알다시피, 1 절과 2 절에서 x2와 x3 각각 1이되고, 당신도 알다시피 만족 스럽습니다

그러나 오메가 3 절에서 x2와 x3은 이제 값 0을 취하고 x4는 단위 리터럴 이 절에서는 유닛에 선택 나는 무엇이 일어나야하는지 정확히 알고있다 x4, x4는 1이어야합니다 사실 변수에 몇 가지 값을 할당했다는 사실은 전체적으로 많은 것을 의미합니다

우리가 만족할만한 방향으로 나아가려면 다른 변수들도 값을 가져야한다 해결책 그리고이 거대한 산업 규모의 SAT 문제가 생기면 BCP는 계속해서 계속 켜져 있습니다 이러한 알고리즘 알고리즘의 핵심은 이러한 기술입니다 그래서 x4는 오메가 3가 단위라는 것을 발견했습니다

훌륭합니다 그것은 우리에게 뭔가를 말해줍니다 우리는 앞으로 나아갈 수 있고 우리는 단순화 할 수 있습니다 그래서, 어떻게되는지 봅시다 그래서 우리는 x4를 1과 같게하려고합니다

그리고 다시 나는 모든 것을 회색으로 표시했습니다 이전 과제 그래서 들어가서 x4를 1로 설정하면 잘됩니다 절 오메가 3가 만족되면 깜짝 조항 오메가 4는 이제 단위가 아니므로 x4는 0 X5는 노출되어 있어야합니다

가치 그리고 오메가 5 절에서 x4도 0입니다 리터럴 x6은 내가 아는 가치로 드러납니다 그래서 저는 x5와 x6을 발견했습니다 암시, 가치있다

그것들은 각각 1과 1이어야합니다 X5는 1이어야하고 x6는 1이어야합니다 좋아요, 전 진전을 이루고있는 것 같아요 나는 하나의 단위 인 조항을 밝히고있다 나는 그 조항을 만족하게하는 과제를하고 나는 다른 것을 밝힌다

단위 인 조항은 계속 유지됩니다 그것은, 와우,이 일은 그 자체를 단순화하는 것과 같습니다 그럼 그 과제를 만들어 보겠습니다 오메가 4와 오메가 5는 이제 단위 절입니다 우리는 x5와 x6이 무엇인지 알아야합니다

가자 따라서 앞으로 x5와 x6을 각각 값 1에 할당하려고합니다 그리고 어떻게되는지 봅시다 오메가 4 절에서 x5는 1입니다 오메가 4가 만족됩니다

오메가 5 절에서 x5는 1입니다 만족합니다 그리고 뭔가 나쁜 일이 일어났습니다 오메가 6 조항에서 무슨 일이 일어 났는지보십시오 x5는 0입니다

x6은 0이 아닙니다 그것은 행복하지 않다 괜찮아? 오메가 6 조항은 이제 만족스럽지 않게되었습니다 권리? 오메가 6 절은 갈등이 있습니다 특정 변수의 값을 순서대로 가지도록 한 다른 절의 포인트 그들을 만족시키기 위해서는 절의 오메가 6이 반드시 충돌해야합니다

죄송합니다 죄송합니다 이것은 이것이 작동하는 방식입니다 이것이 바로 이런 종류의 문제입니다 재귀 적

너도 행복 할 때까지 갈거야 당신이 그것을 만족시키는 과제를 찾거나 당신이 무언가가 될 때까지 불행한 일이 생겨서, 갈등이 생겼어 나는 어떤 결정을 내리기 위해 일찍 결정을 취소해야 할 것 같아 앞으로 진행 그래서 꽤 많이, 당신도 알다시피

SAT 엔진의 핵심 인 BCP가 통과를 완료하면 SAT 해결자가 있습니다 일어날 수있는 정말로 세 가지 전 SAT 시험을 모두 볼 수 있었어 내가 돌아갈 수있을 정도로 내가 일하고 있었던 조항 이 조항 중 많은 부분이 만족 스러웠습니다

또는 상황이 해결되지 않을 수 있습니다 우리는 사실 미해결 조항을 가지고있었습니다 여기서 오메가 9 조항은 해결되지 않았습니다 나는 그것이 만족 스럽거나 만족스럽지 않을지 충분히 알지 못한다 하지만 실제로 가장 큰 문제는 omega라는 것이 었습니다

6은 만족하지 못했습니다 그것은 갈등이었습니다 우리는 갈등을 발견했습니다 하나 이상의 절이 0으로 평가됩니다 너는 무엇을해야만 하는가? 결정한 사람 중 하나를 실행 취소해야합니다

변수 할당 너는 다시 길을 가야 해 임의로 변수 값을 결정한이 프로세스의 시작과 당신은 그것을 취소하고 다른 것을 시도해야합니다 이것은 정말 유명한 이름입니다 이것은 DPLL입니다

그래서 데이비스 퍼트 남 -로만 만 – 러블랜드입니다 그래서 Davis와 Putnam은 기본을 발표했다 1960 년 부울 만족을 해결하기위한 재귀 적 프레임 워크 와우, 오래 전 이었어 그리고 나서 Davis, Logemann 및 Loveland는이 똑똑한 부울 제약 전파를 발견했으며, 기본적으로 그들은 1962 년에 단위 조항 규칙 방식을 제안 했으므로 50을 약간 넘었습니다 여러 해 전에

놀랍게도, 그것은 50 년입니다 오래되었지만 여전히 현대의 모든 SAT 엔진의 마음과 정신입니다 첫 번째 논문을 기리는 의미에서 종종 데이비스 – 퍼트 남 (DP)으로 불리우거나 부정확하게, 데이비스 – 퍼트 남 -로만 만 – 러블랜드 그들 중 네 명이 실제로 한 적이 없었습니다 이 모든 것을 함께 게시하십시오

그리고 큰 아이디어는 완전한 것입니다 변수 할당에 대한 체계적인 검색, CNF 형식은 효율성을 높이기위한 유용한 형식입니다 그 중 하나가 0이기 때문에 즉시 이러한 것들을 만족시킬 수 없습니다 그리고 검색을 더 일찍 멈추게하는 단위 절이있는 BCP 더 많은 것을 반복하지 않고 배정 그래서 이것은 정말로 정말로 유명합니다

물건 그것은 매우 유명합니다 자체 Wikipedia를 가지고 있습니다 페이지, 헤이, 헤이 그래서 그것은 확실히 가치있는 체크 아웃입니다

당신이 있다면, 당신은 역사에 대해 조금 알고 싶습니다 사실 많은 이 사람들은, 그들이 60 년대 초에 그 물건을 출판하고 있다는 사실에도 불구하고, 아직 살아있다 그들은 저기에 올라가고 있지만 그들은 여전히 ​​주위에있어,에 대한 개인적인 전기를 볼 수 있습니다 재미있는 Wikipedia 이제 SAC는 엄청난 거대한 엄청난 규모를 가지고 있습니다

지난 20 년 동안 진보 그래서 DPLL은 물건이 시작되는 곳입니다 그러나 SAT는 강렬한 연구의 주제였습니다 불행히도 압축 된 시간 제약 조건을 Armook 나는 진짜로 2 주 그것을 보내지 않는다

계속되는 모든 재미있는 것들에 대해 이야기하려고합니다 하지만 정말로 네 가지 일이 있습니다 효율적인 데이터 구조가 있습니다 그 (것)들을 빨리 찾을 수있다 그래야 괜찮아

효율적인 변수 선택이 있습니다 추론을 사용하면 가능성이있는 변수를 선택할 수 있습니다 boolean 제약 조건 전달 동작을 많이 제공합니다 단편화되고 단순화되는 많은 절을 만들려고합니다 그리고 그것은 멋진 아이디어입니다

어떻게 할 수 있습니까? 음, 그렇게 할 수있는 흥미로운 발견법이 있습니다 그래서 당신은 많은 함의를 발견 할 수 있습니다 놀랍고 효율적인 BCP가 있습니다 메커니즘 그 이유는 SAT가 거의 모든 시간은 BCP 안에 있습니다

당신이 당신의 모든 시간을 찾기 때문에 단위가되는 절, 단위 인 변수를 찾는 것, 그들에게 내포 된 값을 할당 한 다음 절 데이터베이스로 돌아가서 당신이 그것을 다음에 할당해야하는 것을 알아내는 것 그리고 당신은 매우 가벼운 터치가 필요합니다 단위가 될 수없는 절을 보지 않도록해야합니다 그리고 당신은 다음과 같은 조항에 대해 가능한 한 최소한의 계산 작업을 수행해야합니다 단위로 무엇을해야할지 파악합니다

정말 멋진 데이터 구조가 있습니다 당신이 그렇게하게 만들었습니다 실제로 몇 가지가 있습니다 소위 학습 메커니즘 그들은 갈등 학습이라고 불립니다

재귀 적 탐색을 진행하면서 패턴을 찾을 수 있습니다 만족감을 유발할 수없는 변수 당신은 그것들을 배울 수 있고 그것들을 배우는 것은 당신이 실제로 그것을 창조 할 수 있다는 것입니다 이러한 변수의 구조를 캡처하는 데이터베이스의 새로운 절 그것을 데이터베이스에 다시 추가 할 수 있습니다

그래서 당신은 결코 그것을 찾으려고 노력하지 않을 것입니다 패턴을 다시 사용하면 주기적으로 반복되는 비효율을 피할 수 있습니다 1과 0 중 특정 패턴을 피해야하는 변수들의 부분 집합 매우 흥미로운 알고리즘 세트 결과는 좋은 SAT 코드이며, 그들은 거대한 문제를 일으킬 수 있습니다

거대한 문제가 뭐니? 커다란 문제는 5 만 개의 변수를 가지고 있습니다 커다란 문제는 2,500 만 개의 리터럴이 있습니다 거대한 문제에는 5 천만 개의 조항이 있습니다 왜 헤이, 내가 왜 못 만들지 궁금해 각 절에 대한 BDD가 0인지 또는 1인지 여부를 확인합니다

그렇기 때문에 아무도 5 천만 BDD를 만들고 싶어하지 않습니다 괜찮아 그것은 단지 일어나지 않는 것입니다 따라서 지난 20 년 동안 이러한 매우 차가운 효율 메커니즘의 결과 몇 년 동안 놀라운 SAT 코드가있었습니다 당신은 실제로 나가서 이런 것들을 발견 할 수 있습니다

그들 중 많은 수가 있습니다 유용한 SAT 해결사가 많이 있습니다 온라인 오픈 소스 스웨덴의 두 Niklas 출신의 많은 SAT 아주 작은 작은 최소의 솔버 코드 갖고 계신다면 개인 기계에 붙잡기가 매우 쉽습니다

우리는 MOOC에서 이것을 사용하지 않을 것입니다 우리는 당신과 함께 놀 수있는 Coursera 서버에 이것을 설치합니다 샤프 말릭 (Sharad Malik)과 프린스턴 대학교 (Princeton University)의 학생 인 채프 (Chaff) 미시간 대 (University of Michigan)의 Marques-Silva와 Sakallah에서 파악하십시오 당신이 약간의 인터넷 검색을하면, 실제로 갈 수 있습니다, 당신은 실제로 모든 것을 찾을 수 있습니다

이러한 것들 중 그리고 너도 알다시피, 이것은 아마도 당신이 그렇게하기에 흥미 롭습니다 소년, 제비 뽑기와 제비 뽑기가있다 웹상에 SAT에 대한 정보가 있습니다 나는 당신이 주변을 둘러 보도록 권합니다

읽을만한 흥미로운 정보가 많이 있습니다 그러나 이것은 SAT 내부에서 일어나는 일들에 대한 우리의 논의 일 것입니다 우리가 다음에해야 할 일은 질문을합니다 음, 엔지니어링이 있습니다 VLSI 사람들이 디자인하려고했던 우주의 모습

게이트 블록들 이제 우리는 무엇을합니까? 실제 로직 디자인처럼 보이게하려면 어떻게해야합니까? 우리에게 유용한 것을하십시오 그럼 다음에 대해 이야기하겠습니다