Лекция 11. Bounded Model Checking. Выполнимость булевых формул SAT, страница 2

Åñëè π ýòî (`, k) -ïóòü, òî π |=k ϕ ⇔ πb |= ϕ.2. Åñëè π ýòî k -ïóòü, òî π |=k ϕ ⇔ πb |=0k ϕ,ãäå äëÿ ëþáîé ïàðû 0 ≤ i ≤ kIπ |=ik p ⇐⇒ p ∈ L(si ), π |=ik ¬p ⇐⇒ p ∈/ L(si ),Iπ |=ik f ∧ g ⇐⇒ π |=ik f è π |=ik f ,Iπ |=ik f ∨ g ⇐⇒ π |=ik f èëè π |=ik f ,Iπ |=ikXf⇐⇒ π |=i+1f è i < k,kIπ |=ikFf⇐⇒ π |=jk f äëÿ íåêîòîðîãî j : i ≤ j ≤ k ,Iπ 6|=ikGfäëÿ ëþáûõ i, k ,IπfUg ⇐⇒ àíàëîãè÷íî, ñàìîñòîÿòåëüíî ,Iπ|=ik|=ikfRg ⇐⇒ àíàëîãè÷íî, ñàìîñòîÿòåëüíî ,Çàäà÷à îãðàíè÷åííîé âåðèôèêàöèè ìîäåëåéïðîãðàìì (BMC)Îáðàòèòå âíèìàíèå, ÷òî π |=k ¬ G f 6⇐⇒ π |=kF ¬fÇàäà÷à 1.À êàêèå åùå ðàâíîñèëüíîñòè, âûïîëíÿþøèåñÿ â PLTL,íàðóøàþòñÿ ïðè ïåðåõîäå ê îòíîøåíèþ îãðàíè÷åííîéâûïîëíèìîñòè?Äåéñòâóþò ëè äëÿ îòíîøåíèÿ îãðàíè÷åííîé âûïîëíèìîñòèçàêîíû íåïîäâèæíîé òî÷êè?Çàäà÷à îãðàíè÷åííîé âåðèôèêàöèè ìîäåëåéïðîãðàìì (BMC)Îáðàòèòå âíèìàíèå, ÷òî π |=k ¬ G f 6⇐⇒ π |=kF ¬fÇàäà÷à 1.À êàêèå åùå ðàâíîñèëüíîñòè, âûïîëíÿþøèåñÿ â PLTL,íàðóøàþòñÿ ïðè ïåðåõîäå ê îòíîøåíèþ îãðàíè÷åííîéâûïîëíèìîñòè?Äåéñòâóþò ëè äëÿ îòíîøåíèÿ îãðàíè÷åííîé âûïîëíèìîñòèçàêîíû íåïîäâèæíîé òî÷êè?Ïóñòü ϕ ïðîèçâîëüíàÿ ôîðìóëà ïóòè.

Óñëîâèìñÿèñïîëüçîâàòü çàïèñü M |=k E ϕ äëÿ îáîçíà÷åíèÿ çàÿâëåíèÿ îòîì, ÷òî â ìîäåëè M ñóùåñòâóåò íà÷àëüíûé k -ïóòü èëè(`, k)-ïóòü π , äëÿ êîòîðîãî âåðíî ñîîòíîøåíèå π |=k ϕ .Çàäà÷à îãðàíè÷åííîé âåðèôèêàöèè ìîäåëåéïðîãðàìì (BMC)Óòâåðæäåíèå 1.Äëÿ ëþáîé ôîðìóëû ïóòè â ïîçèòèâíîé ôîðìå ϕ , äëÿ ëþáîãîk, k ≥ 1 , è äëÿ ëþáîãî (áåñêîíå÷íîãî) ïóòè π∞ = ππ 0 , ãäå π k -ïóòü, âåðíî ñîîòíîøåíèå π |=k ϕ ⇒ π∞ |= ϕ .Çàäà÷à îãðàíè÷åííîé âåðèôèêàöèè ìîäåëåéïðîãðàìì (BMC)Óòâåðæäåíèå 1.Äëÿ ëþáîé ôîðìóëû ïóòè â ïîçèòèâíîé ôîðìå ϕ , äëÿ ëþáîãîk, k ≥ 1 , è äëÿ ëþáîãî (áåñêîíå÷íîãî) ïóòè π∞ = ππ 0 , ãäå π k -ïóòü, âåðíî ñîîòíîøåíèå π |=k ϕ ⇒ π∞ |= ϕ .Óòâåðæäåíèå 2.Ïóñòü ϕ ôîðìóëà ïóòè â ïîçèòèâíîé ôîðìå, è M ìîäåëüÊðèïêå.

Òîãäà åñëè M 6|= A ¬ϕ , òî ñóùåñòâóåò òàêîéíà÷àëüíûé k -ïóòü èëè (`, k)-ïóòü π , äëÿ êîòîðîãî âåðíîñîîòíîøåíèå π |=k ϕ .Çàäà÷à îãðàíè÷åííîé âåðèôèêàöèè ìîäåëåéïðîãðàìì (BMC)Óòâåðæäåíèå 1.Äëÿ ëþáîé ôîðìóëû ïóòè â ïîçèòèâíîé ôîðìå ϕ , äëÿ ëþáîãîk, k ≥ 1 , è äëÿ ëþáîãî (áåñêîíå÷íîãî) ïóòè π∞ = ππ 0 , ãäå π k -ïóòü, âåðíî ñîîòíîøåíèå π |=k ϕ ⇒ π∞ |= ϕ .Óòâåðæäåíèå 2.Ïóñòü ϕ ôîðìóëà ïóòè â ïîçèòèâíîé ôîðìå, è M ìîäåëüÊðèïêå. Òîãäà åñëè M 6|= A ¬ϕ , òî ñóùåñòâóåò òàêîéíà÷àëüíûé k -ïóòü èëè (`, k)-ïóòü π , äëÿ êîòîðîãî âåðíîñîîòíîøåíèå π |=k ϕ .Òåîðåìà 1.Ïóñòü ϕ ôîðìóëà ïóòè â ïîçèòèâíîé ôîðìå, è M ìîäåëüÊðèïêå. Òîãäà M 6|= A ¬ϕ â òîì è òîëüêî òîì ñëó÷àå, êîãäà äëÿíåêîòîðîãî k âåðíî ñîîòíîøåíèå M |=k E ϕ .Çàäà÷à îãðàíè÷åííîé âåðèôèêàöèè ìîäåëåéïðîãðàìì (BMC)Òàêèì îáðàçîì, ìû ïðèõîäèì ê çàäà÷å BMC:äëÿ çàäàííûõ ôîðìóëû ïóòè â ïîçèòèâíîé ôîðìåìîäåëè ÊðèïêåM |=kMè öåëîãîkϕ,ïðîâåðèòü ñîîòíîøåíèåEϕ .Ïîêàæåì, êàê ìîæíî ñâåñòè çàäà÷ó BMC ê çàäà÷å SAT.Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÄëÿ ýòîãî îïèøåì àëãîðèòì (òðàíñëÿòîð), êîòîðûé äëÿïðîèçâîëüíîé ôîðìóëû ïóòè ϕ , ìîäåëè Êðèïêå M è öåëîãî kñòðîèò òàêóþ áóëåâó ôîðìóëó Trans[ϕ, M, k] , êîòîðàÿâûïîëíèìà â òîì è òîëüêî òîì ñëó÷àå, êîãäà M |=k E ϕ .Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÄëÿ ýòîãî îïèøåì àëãîðèòì (òðàíñëÿòîð), êîòîðûé äëÿïðîèçâîëüíîé ôîðìóëû ïóòè ϕ , ìîäåëè Êðèïêå M è öåëîãî kñòðîèò òàêóþ áóëåâó ôîðìóëó Trans[ϕ, M, k] , êîòîðàÿâûïîëíèìà â òîì è òîëüêî òîì ñëó÷àå, êîãäà M |=k E ϕ .Òðàíñëÿöèÿ ïðîâîäèòñÿ â òðè ýòàïà.1).

Âíà÷àëå ïîñòðîèì áóëåâó ôîðìóëó PH[M, k] , êîòîðàÿâûïîëíÿåòñÿ òîëüêî íà òåõ íàáîðàõ çíà÷åíèé ïåðåìåííûõ,êîòîðûå ïðåäñòàâëÿþò âñåâîçìîæíûå íà÷àëüíûå ïóòè π äëèíûk â ìîäåëè M .2) Çàòåì ïîñòðîèì áóëåâû ôîðìóëû LP[k, `] è NL[k] ,âûïîëíèìîñòü êîòîðûõ ñëóæèò èíäèêàòîðîìñóùåñòâîâàíèÿ/îòñóòñòâèÿ öèêëà â (`, k)-ïóòè π .3)  çàêëþ÷åíèå ïîñòðîèì áóëåâó ôîðìóëó CH[i, k, ϕ] ,âûïîëíèìîñòü êîòîðîé ÿâëÿåòñÿ ïðèçíàêîì òîãî, ÷òî π |=ik ϕ .Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÇàìåòèì, ÷òî ìîäåëü M = (S, S0 , R, L) ìîæåò áûòüïðåäñòàâëåíà òàê:Iìíîæåñòâî ñîñòîÿíèé S ýòî ìíîæåñòâî äâîè÷íûõíàáîðîâ íåêîòîðîé äëèíû n ;Iìíîæåñòâî íà÷àëüíûõ ñîñòîÿíèé S0 îïèñûâàåòñÿ áóëåâîéôîðìóëîé I : I (s) = 1 òîãäà è òîëüêî òîãäà, êîãäà s ∈ S0 ;Iîòíîøåíèå ïåðåõîäîâ R îïèñûâàåòñÿ áóëåâîé ôîðìóëîé T: T (s 0 , s 00 ) = 1 òîãäà è òîëüêî òîãäà, êîãäà (s 0 , s 00 ) ∈ R ;Iäëÿ êàæäîãî àòîìàðíîãî âûñêàçûâàíèÿ p åñòü áóëåâàôîðìóëà P : P(s) = 1 òîãäà è òîëüêî òîãäà, êîãäà p ∈ L(s)Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÇàìåòèì, ÷òî ìîäåëü M = (S, S0 , R, L) ìîæåò áûòüïðåäñòàâëåíà òàê:Iìíîæåñòâî ñîñòîÿíèé S ýòî ìíîæåñòâî äâîè÷íûõíàáîðîâ íåêîòîðîé äëèíû n ;Iìíîæåñòâî íà÷àëüíûõ ñîñòîÿíèé S0 îïèñûâàåòñÿ áóëåâîéôîðìóëîé I : I (s) = 1 òîãäà è òîëüêî òîãäà, êîãäà s ∈ S0 ;Iîòíîøåíèå ïåðåõîäîâ R îïèñûâàåòñÿ áóëåâîé ôîðìóëîé T: T (s 0 , s 00 ) = 1 òîãäà è òîëüêî òîãäà, êîãäà (s 0 , s 00 ) ∈ R ;äëÿ êàæäîãî àòîìàðíîãî âûñêàçûâàíèÿ p åñòü áóëåâàôîðìóëà P : P(s) = 1 òîãäà è òîëüêî òîãäà, êîãäà p ∈ L(s)kVÒîãäà PH[M, k](x0 , x1 , .

. . , xk ) = I (x0 ) ∧T (xi−1 , xi )Ii=1LP[k, `] = T (xk , x` ) ,kVNL[k] =LP[k, `] .i=0Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÓòâåðæäåíèå 3.Äëÿ ëþáîé ïîñëåäîâàòåëüíîñòè ñîñòîÿíèé s0 , s1 , . . . , sk âìîäåëè M ýòà ïîñëåäîâàòåëüíîñòü îáðàçóåò k -ïóòüs0 → s1 → · · · → sk â òîì è òîëüêî òîì ñëó÷àå, êîãäàPH[M, k](s0 , s1 , . . . , sk ) = 1 .Óòâåðæäåíèå 4.Äëÿ ëþáîé ïîñëåäîâàòåëüíîñòè ñîñòîÿíèé s0 , s1 , . . . , sk âìîäåëè M ýòà ïîñëåäîâàòåëüíîñòü îáðàçóåò (`,k )-ïóòüs0 → s1 → · · · → sk → s` â òîì è òîëüêî òîì ñëó÷àå, êîãäàPH[M, k, `](s0 , s1 , . . . , sk ) ∧ LP[k, `](s0 , s1 , . .

. , sk ) = 1 .Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÄëÿ ïàðàìåòðîâ k, ` è öåëîãî i, 0 ≤ i ≤ k áóäåì ïîëàãàòü(i + 1 åñëè i < k,succ(i, `, k) =` åñëè i = k.Òîãäà äëÿ ñëó÷àÿ (`, k)-ïóòè π òðàíñëÿöèÿ óñëîâèÿâûïîëíèìîñòè π |=ik ϕ òàêîâà:I CH[i, `, k, p] = P(xi ) äëÿ àòîìàðíîé ôîðìóëû p ;I CH[i, `, k, ¬p] = P(xi ) ;I CH[i, `, k, f ∧ g ] = CH[i, `, k, f ] ∧ CH[i, `, k, g ] ;I CH[i, `, k, f ∨ g ] = CH[i, `, k, f ] ∨ CH[i, `, k, g ] ;I CH[i, `, k, X f ] = CH[succ(i, `, k), `, k, f ] ;kWI CH[i, `, k, F f ] =CH[j, `, k, f ] ;j=min(i,`)ICH[i, `, k, G f ] =kVj=min(i,`)CH[i, `, k, f ] ;Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÇàìå÷àíèå 3.Îáðàòèòå âíèìàíèå, ÷òî ïðàâèëà òðàíñëÿöèè ïðåäóñìàòðèâàþòââåäåíèå âñïîìîãàòåëüíûõ áóëåâûõ ïåðåìåííûõ.Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÇàìå÷àíèå 3.Îáðàòèòå âíèìàíèå, ÷òî ïðàâèëà òðàíñëÿöèè ïðåäóñìàòðèâàþòââåäåíèå âñïîìîãàòåëüíûõ áóëåâûõ ïåðåìåííûõ.Íàïðèìåð, äëÿ ñëó÷àÿ CH[0, 0, 2, G F p] ïîëó÷àåìCH[0, 0, 2, G F p] = (y0 ∧ y1 ∧ y2 ) ∧∧ (y0 ≡ (P(s0 ) ∨ P(s1 ) ∨ P(s2 ))) ∧∧ (y1 ≡ (P(s0 ) ∨ P(s1 ) ∨ P(s2 ))) ∧∧ (y2 ≡ (P(s0 ) ∨ P(s1 ) ∨ P(s2 ))) ∧Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÇàìå÷àíèå 3.Îáðàòèòå âíèìàíèå, ÷òî ïðàâèëà òðàíñëÿöèè ïðåäóñìàòðèâàþòââåäåíèå âñïîìîãàòåëüíûõ áóëåâûõ ïåðåìåííûõ.Íàïðèìåð, äëÿ ñëó÷àÿ CH[0, 0, 2, G F p] ïîëó÷àåìCH[0, 0, 2, G F p] = (y0 ∧ y1 ∧ y2 ) ∧∧ (y0 ≡ (P(s0 ) ∨ P(s1 ) ∨ P(s2 ))) ∧∧ (y1 ≡ (P(s0 ) ∨ P(s1 ) ∨ P(s2 ))) ∧∧ (y2 ≡ (P(s0 ) ∨ P(s1 ) ∨ P(s2 ))) ∧Çàäà÷à 2.Ýòî íå ñëèøêîì ýêîíîìíàÿ òðàíñëÿöèÿ.

À íåëüçÿ ëè ñäåëàòü ååáîëåå ýôôåêòèâíî?Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÇàìå÷àíèå 3.Îáðàòèòå âíèìàíèå, ÷òî ïðàâèëà òðàíñëÿöèè ïðåäóñìàòðèâàþòââåäåíèå âñïîìîãàòåëüíûõ áóëåâûõ ïåðåìåííûõ.Íàïðèìåð, äëÿ ñëó÷àÿ CH[0, 0, 2, G F p] ïîëó÷àåìCH[0, 0, 2, G F p] = (y0 ∧ y1 ∧ y2 ) ∧∧ (y0 ≡ (P(s0 ) ∨ P(s1 ) ∨ P(s2 ))) ∧∧ (y1 ≡ (P(s0 ) ∨ P(s1 ) ∨ P(s2 ))) ∧∧ (y2 ≡ (P(s0 ) ∨ P(s1 ) ∨ P(s2 ))) ∧Çàäà÷à 2.Ýòî íå ñëèøêîì ýêîíîìíàÿ òðàíñëÿöèÿ. À íåëüçÿ ëè ñäåëàòü ååáîëåå ýôôåêòèâíî?Çàäà÷à 3.À êàê óñòðîåíà òðàíñëÿöèÿ ôîðìóëû CH[i, `, k, fUg] ?Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÄëÿ ñëó÷àÿ k -ïóòè π òðàíñëÿöèÿ óñëîâèÿ âûïîëíèìîñòèπ |=ik ϕ òàêîâà:ICH[i, k, p] = P(xi ) äëÿ àòîìàðíîé ôîðìóëû p ;ICH[i, k, ¬p] = P(xi ) ;ICH[i, k, f ∧ g ] = CH[i, k, f ] ∧ CH[i, k, g ] ;ICH[i, k, f ∨ g ] = CH[i, k, f ] ∨ CH[i, k, g ] ;ICH[i, k, X f ] = CH[i + 1, k, k, f ] ;ICH[i, k, F f ] = CH[i, k, f ] ∨ CH[i + 1, k, F f ] ;ICH[i, k, G f ] = CH[i, k, f ] ∧ CH[i + 1, k, G f ] ;ICH[k + 1, k, f ] = 0 .Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÄëÿ ñëó÷àÿ k -ïóòè π òðàíñëÿöèÿ óñëîâèÿ âûïîëíèìîñòèπ |=ik ϕ òàêîâà:ICH[i, k, p] = P(xi ) äëÿ àòîìàðíîé ôîðìóëû p ;ICH[i, k, ¬p] = P(xi ) ;ICH[i, k, f ∧ g ] = CH[i, k, f ] ∧ CH[i, k, g ] ;ICH[i, k, f ∨ g ] = CH[i, k, f ] ∨ CH[i, k, g ] ;ICH[i, k, X f ] = CH[i + 1, k, k, f ] ;ICH[i, k, F f ] = CH[i, k, f ] ∨ CH[i + 1, k, F f ] ;ICH[i, k, G f ] = CH[i, k, f ] ∧ CH[i + 1, k, G f ] ;ICH[k + 1, k, f ] = 0 .Çàäà÷à 4.À êàê óñòðîåíà òðàíñëÿöèÿ ôîðìóëû CH[i, k, fUg] ?Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÎêîí÷àòåëüíî èìååìk_Tr [ϕ,M,k] = Path[M,k] ∧ (NL[k] ∧ CH[0,k,ϕ]) ∨ (LP[`,k] ∧ CH[0,`,k,ϕ]){z}|`=0k−ïóòè|{z}(`,k)−ïóòèÒðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÎêîí÷àòåëüíî èìååìk_Tr [ϕ,M,k] = Path[M,k] ∧ (NL[k] ∧ CH[0,k,ϕ]) ∨ (LP[`,k] ∧ CH[0,`,k,ϕ]){z}|`=0k−ïóòè|{z}(`,k)−ïóòèÒåîðåìà 2.Äëÿ ëþáîé ôîðìóëû ïóòè â ïîçèòèâíîé ôîðìå ϕ , äëÿ ëþáîãîk , è äëÿ ëþáîé ìîäåëè Êðèïêå M âåðíîM |=kEϕ⇐⇒ Tr [ϕ,M,k] − âûïîëíèìàÿ áóëåâà ôîðìóëà.Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÀ êàêîâ ðàçìåð áóëåâîé ôîðìóëû, êîòîðûé ïîëó÷àåòñÿ âðåçóëüòàòå òàêîé òðàíñëÿöèè BMC-to-SAT?Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÀ êàêîâ ðàçìåð áóëåâîé ôîðìóëû, êîòîðûé ïîëó÷àåòñÿ âðåçóëüòàòå òàêîé òðàíñëÿöèè BMC-to-SAT? òîì âèäå, â êîòîðîì òðàíñëÿöèÿ áûëà îïèñàíà çäåñü, áóëåâàôîðìóëà Tr [ϕ,M,k] èìååò ðàçìåðO(k|M| + k 2 |ϕ|).Åñëè âîñïîëüçîâàòüñÿ áîëåå ýêîíîìíîé òðàíñëÿöèåé, òî ðàçìåðóäàåòñÿ ñîêðàòèòü äîO(k(|M| + |ϕ|)).Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÈòàê, ðàçìåð ïðîâåðÿåìîé áóëåâîé ôîðìóëû O(k(|M| + |ϕ|)).Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÈòàê, ðàçìåð ïðîâåðÿåìîé áóëåâîé ôîðìóëû O(k(|M| + |ϕ|)).Îäíàêî äëÿ ãàðàíòèðîâàííîé ïðîâåðêè M |= E ϕ íóæíîèñïîëüçîâàòü çíà÷åíèå k ðàâíîå äèàìåòðó d(M) ìîäåëè M . îáùåì ñëó÷àå, d(M) = 2O(|M|) .Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÈòàê, ðàçìåð ïðîâåðÿåìîé áóëåâîé ôîðìóëû O(k(|M| + |ϕ|)).Îäíàêî äëÿ ãàðàíòèðîâàííîé ïðîâåðêè M |= E ϕ íóæíîèñïîëüçîâàòü çíà÷åíèå k ðàâíîå äèàìåòðó d(M) ìîäåëè M . îáùåì ñëó÷àå, d(M) = 2O(|M|) .Êðîìå òîãî, ïðîâåðêà âûïîëíèìîñòè áóëåâîé ôîðìóëûïðîâîäèòñÿ â õóäøåì ñëó÷àå çà âðåìÿ, ýêñïîíåíöèàëüíîçàâèñÿùåå îò ðàçìåðà ýòîé ôîðìóëû.Òàêèì îáðàçîì, â õóäøåì ñëó÷àå ïðîâåðêà M |= E ϕïîñðåäñòâîì òðàíñëÿöèè BMC-to-SAT ïðîâîäèòñÿ çà âðåìÿ22O(|M|).Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÈòàê, ðàçìåð ïðîâåðÿåìîé áóëåâîé ôîðìóëû O(k(|M| + |ϕ|)).Îäíàêî äëÿ ãàðàíòèðîâàííîé ïðîâåðêè M |= E ϕ íóæíîèñïîëüçîâàòü çíà÷åíèå k ðàâíîå äèàìåòðó d(M) ìîäåëè M . îáùåì ñëó÷àå, d(M) = 2O(|M|) .Êðîìå òîãî, ïðîâåðêà âûïîëíèìîñòè áóëåâîé ôîðìóëûïðîâîäèòñÿ â õóäøåì ñëó÷àå çà âðåìÿ, ýêñïîíåíöèàëüíîçàâèñÿùåå îò ðàçìåðà ýòîé ôîðìóëû.Òàêèì îáðàçîì, â õóäøåì ñëó÷àå ïðîâåðêà M |= E ϕïîñðåäñòâîì òðàíñëÿöèè BMC-to-SAT ïðîâîäèòñÿ çà âðåìÿ22O(|M|).Äëÿ ñïðàâêè: òàáëè÷íûé àëãîðèòì âåðèôèêàöèè M |= E ϕèìååò ñëîæíîñòü 2O(|M|+|ϕ|) . ÷åì æå ãåøåôò?Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÏðåèìóùåñòâà BMC òàêîâû:1.

BMC ðàáîòàåò ñ íåÿâíûì ïðåäñòàâëåíèåì ìîäåëè;2. ïîäàâëÿþùåå áîëüøèíñòâî îøèáîê ðàñïîëàãàþòñÿ¾íåãëóáîêî¿;3. ó ìíîãèõ ïðàêòè÷åñêè âàæíûõ ìîäåëåé äèàìåòð d(M)íåâåëèê;Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÏðåèìóùåñòâà BMC òàêîâû:1. BMC ðàáîòàåò ñ íåÿâíûì ïðåäñòàâëåíèåì ìîäåëè;2. ïîäàâëÿþùåå áîëüøèíñòâî îøèáîê ðàñïîëàãàþòñÿ¾íåãëóáîêî¿;3. ó ìíîãèõ ïðàêòè÷åñêè âàæíûõ ìîäåëåé äèàìåòð d(M)íåâåëèê;4.ñîâðåìåííûå SAT-ðåøàòåëè íåïðàâäîïîäîáíîïðîèçâîäèòåëüíû íà ïðàêòèêå!Òðàíñëÿöèÿ çàäà÷è BMC â çàäà÷ó SATÏðàêòè÷åñêèå ïðåèìóùåñòâà BMC ïî ñðàâíåíèþ ñâåðèôèêàöèåé ROBDD:ModelCircuitCircuitCircuitCircuitCircuitCircuitCircuitCircuitCircuitCircuit12345678910k57711112028103712BDD1142106618941962795*5524**BMC2.50.82210236463781951070Ðèñ.: Ðåçóëüòàòû âåðèôèêàöèè (ñåê) ðàçëè÷íûõ ïðîåêòîâ ýëåòðîííûõñõåì Intel ïðè ïîìîùè ñðåäñòâà âåðèôèêàöèè ñ èñïîëüçîâàíèåìROBDD (Forcast) è BMC (SAT-ðåøàòåëü Thunder)ÊÎÍÅÖ ËÅÊÖÈÈ 11..