擺渡者難題課件

擺渡者難題

你可記得擺渡者難題：一個船夫、山羊、卷心菜和狼都在河的一邊。船夫至多可搭載一位乘客過河。如果船夫離開，山羊會吃掉卷心菜，狼也會吃掉山羊。船夫能否將它們（包括狼、山羊、卷心菜）安全送到河對岸？

其實(shí)這只是一道很簡單的智力題，我們幾乎馬上可以得到其中一種答案：

而今天我們要做的就是讓計(jì)算機(jī)來給出我們這樣一個答案。

分析過河過程：從問題的描述可以看出,在過河的過程中船夫是具有選擇權(quán)的（這個選擇交由計(jì)算機(jī)執(zhí)行），他可以選擇搭載或者不搭載物品（即狼，羊，菜）。而且，船夫只有和某物品處在同一側(cè)岸邊，他才有可能搭載這個物品，并且最多只能搭載一個。這就意味著，若船夫同狼、羊、菜分別位于河的兩岸時，就沒有辦法搭載它們了。根據(jù)以上過河過程的分析，我們可以建立這樣一個遷移狀態(tài)：

船夫：在此岸或者彼岸山羊：在此岸或者彼岸狼：在此岸或者彼岸卷心菜：在此岸或者彼岸初始時船夫：此岸山羊：此岸狼：此岸卷心菜：在此岸下個狀態(tài)船夫：在此岸或彼岸

（搭載物品？由計(jì)算機(jī)在滿足條件的物品中隨機(jī)選擇）狼：若此時和船夫同處一岸又被選中，則下個狀態(tài)在對岸，否則還在此地。山羊：若此時和船夫同處一岸又被選中，則下個狀態(tài)在對岸，否則還在此地。卷心菜：若此時和船夫同處一岸又被選中，則下個狀態(tài)在對岸，否則還在此地。

上述遷移狀態(tài)用NuSMV語言表達(dá)則為：MODULEmainVARferryman:boolean;goat:boolean;cabbage:boolean;wolf:boolean;carry:{g,c,w,0};ASSIGNinit(ferryman):=0;init(goat):=0;init(cabbage):=0;init(wolf):=0;init(carry):=0;next(ferryman):=!ferryman;next(goat):=casenext(carry):=caseferryman=goat&next(carry)=g:next(ferryman);ferryman=goat:g;1:goat;1:0;esac;esacunionnext(cabbage):=casecaseferryman=cabbage&next(carry)=c:next(ferryman);ferryman=cabbage:c;1:cabbage;1:0;esac;esacunionnext(wolf):=casecaseferryman=wolf&next(carry)=w:next(ferryman);ferryman=wolf:w;1:wolf;1:0;esac;esacunion0;

以上過河程序計(jì)算機(jī)在運(yùn)行時可以產(chǎn)生多個狀態(tài)遷移，關(guān)系圖如下：LTL

線性時態(tài)邏輯LTL(Linear-timeTemporalLogic)

帶有允許指示未來的連接詞，它將時間建模成狀態(tài)的序列，無限延伸到未來，這個狀態(tài)序列有時稱為計(jì)算路徑，一般我們考慮若干路徑，代表不同的可能未來，任何一種都可能是實(shí)現(xiàn)的“實(shí)際”路徑。在LTL語法定義的公式中，二元連接詞U(代表until)是最常見的一個，公式在一條路徑上成立，如果連續(xù)地成立直到成立，此外,實(shí)際上要求在某個未來狀態(tài)確實(shí)成立。如圖，沿著所示的路徑，

到的每個狀態(tài)都滿足pUq，但到不滿足。LTL語義中Until含義的解釋.假設(shè)p

在(且只在)點(diǎn)滿足q在(且只在)點(diǎn)滿足,那么沿著所示路徑只有到滿足pUq

運(yùn)行結(jié)果告訴我們這個取否定的表達(dá)式isfalse，并顯示了一條路徑來說明可以找到使船夫、狼、山羊、卷心菜都安全到達(dá)彼岸的方法。

這條路徑就是擺渡者難題的一個答案，也是我們一開始最希望計(jì)算機(jī)給出的。

由擺渡者難題可以看到計(jì)算機(jī)只是在機(jī)械地進(jìn)行遍歷，在遍歷過程中如果找到不滿足我們給的條件的路徑就顯示此條件為假，不然就一直遍歷完所有狀態(tài)顯示我們給的條件是真的。

問題分析擺渡者難題之所以我們能夠很快得到答案，是因?yàn)橛幸粋€隱含條件：只有船夫才能劃船，即船夫在渡河問題中既充當(dāng)了船的角色同時又是狼、羊、菜之間能夠安全相處的重要因素。八人渡河問題與擺渡者難題最大的不同在于，船夫的唯一性發(fā)生了改變，船夫由一人變?yōu)槿?。也就是說，船在哪岸會劃船的人不一定也在哪岸，不能再將船和劃船人等同看待，而要把船看作一個獨(dú)立的事物。同時還要設(shè)置一個記號來標(biāo)記由計(jì)算機(jī)選擇的船夫。{獵人、女人、老人}{獵人、狼、女人、孩子1、孩子2、老人、孩子3、孩子4}

next(hunter):=case(next(ferryman)=h|next(carry)=h)&boat=hunter:next(boat);--511:hunter;esac;next(female):=case(next(ferryman)=f|next(carry)=f)&boat=female:next(boat);--551:female;esac;next(older):=case(next(ferryman)=o|next(carry)=o)&boat=older:next(boat);1:older;esac;next(wolf):=casenext(child3):=caseboat=wolf&next(carry)=w:next(boat);boat=child3&next(carry)=c3:next(boat);1:wolf;1:child3;esac;esac;next(child1):=caseboat=child1&next(carry)=c1:next(boat);next(child4):=case1:child1;boat=child4&next(carry)=c4:next(boat);esac;1:child4;next(child2):=caseesac;boat=child2&next(carry)=c2:next(boat);1:child2;esac;

八人過河問題的安全性條件為：某一時刻包括狼在內(nèi)的八人都到達(dá)彼岸，且在這一時刻之前狼不能傷人，所有的孩子也不能挨打。這也就是說當(dāng)狼和除獵人以外的人同在一側(cè)河岸時，獵人也必須在這側(cè)河岸以保證狼不能咬人。女人或老人只有在對方也在時，才能和對方的孩子同處一地。用LTL公式表達(dá)如下：!((((female=child3|female=child4)->female=older)&((older=child1|older=child2)->older=female)&((wolf=female|wolf=child1|wolf=child2|wolf=older|wolf=child3|wolf=child4)->wolf=hunter))U(hunter&wolf&female&child1&child2&older&child3&child4))

如此建立模型,雖然可以得到一條安全路徑,但顯然計(jì)算機(jī)的工作量很大，會劃船的有3個人，每人都可以有2個狀態(tài)即此岸和彼岸，在每個狀態(tài)下都有可能載人，而需要被搭載的有8個人，每個人又有2個狀態(tài)(此岸或彼岸)被載等等，這樣看來整個遷移系統(tǒng)就非常龐大復(fù)雜了，是否能簡化一下整個系統(tǒng)呢？我們的做法是將所有人劃分為兩個類，會劃船的人和不會劃船的人，首先讓計(jì)算機(jī)在會劃船的人中選出1~2人坐船，這樣共有6個選擇(+)，而在選1個會劃船時,才再選不會劃船的人,又有6個選擇(5人和0人)，如此做法就會使整個遷移系統(tǒng)簡化不少，顯然機(jī)器遍歷時速度快了。

限時過橋問題某合唱團(tuán)的4名成員A,B,C,D趕往演出現(xiàn)場，他們途中要經(jīng)過一座小橋。當(dāng)他們趕到橋頭時，天已經(jīng)黑了，周圍沒有燈，他們只有一只手電筒。橋很窄一次最多只許2人一起過橋，過橋人手里必須有手電筒。4個人的步行速度都不同，若2人同行，則以較慢者的速度為準(zhǔn)。A需花1分鐘過橋，B過橋需要2分鐘，C需花5分鐘，D需花10分鐘過橋。請問：他們能在17分鐘內(nèi)過橋嗎？

問題分析很明顯，開始兩人拿著手電筒過橋后，手電筒就在橋的另一邊了，此時需要已經(jīng)過橋的那兩人中的一個人再把手電筒送回橋這邊。送手電筒回來過橋也要花時間，所以就要用限定的時間減去兩個人中較慢的那個人所花的時間，再減掉送手電筒那人用的時間。

過橋過程的程序如下：MODULEmaininit(torch):=0;init(person1):=0;VARinit(person2):=0;init(time):=0;personA:boolean;personB:boolean;init(total):=17;personC:boolean;personD:boolean;next(person1):=casetorch:boolean;person1:{1,2,5,10,0};personA=torch:1;person2:{1,2,5,10,0};total:-10..20;1:0;time:{1,2,5,10,0};esacunionASSIGNcaseinit(personA):=0;init(personB):=0;personB=torch:2;init(personC):=0;init(personD):=0;1:0;esacunion

上一次我們主要講了布爾型變量問題，這次主要內(nèi)容是非布爾型變量問題，包括枚舉型和整型。這里枚舉型例子包括一個符號枚舉型和一個整符枚舉型，當(dāng)然這里主要是同層次的枚舉型問題，非層次的枚舉問題將在下一次的內(nèi)容中進(jìn)行演示。猜猜誰是誰

老張、老王和老周，他們分別是教師、律師和醫(yī)生。他們之間有如下關(guān)系：（1）老王比教師矮一些；（2）老張比醫(yī)生高些；（3）老周比醫(yī)生矮一些；

猜猜看：他們誰是律師，誰是教師，誰是醫(yī)生呢？

MODULEmainVAR

wang:{d,t,l,0};next(zhou):=case

zhang:{d,t,l,0};next(zhang)=t:l;

zhou:{d,t,l,0};1:{t,l};ASSIGNesac;

init(wang):=0;LTLSPEC

init(zhang):=0;!F(wang!=zhang&wang!=zhou)

init(zhou):=0;

next(wang):={d,l};

next(zhang):=case

next(wang)=d:t;

1:{t,l};

esac;山羊買外套小白羊、小黑羊、小灰羊一起上街各買了一件外套。三件外套的顏色分別是白色、黑色、灰色?；丶衣飞?，一只小羊說：“我很久以前就想買白外套，今天終于買到了！”說到這里，她好像是發(fā)現(xiàn)了什么，驚喜地對同伴說：“今天我們可真有意思，白羊沒有買白外套，黑羊沒有買黑外套，灰羊沒有買灰外套?！毙『谘蛘f：“真是這樣，你要是不說，我還真沒注意這一點(diǎn)呢！”你能根據(jù)他們的對話，猜出小白羊、小黑羊、小灰羊各買了什么顏色的外套嗎？

建模過程：

根據(jù)畫線部分可以分析得出白羊goatw的外套顏色為黑色（b)或是灰色(g)，黑羊goatb的外套顏色為白色(w)或是灰色(g)，而灰羊goatg的外套顏色則為黑色(b)或是白色(w)。

而且黑羊的話說明他的外套顏色不可能是白色（題目中隱含了三只羊的外套顏色不能重復(fù)）。那么可以得出這個問題的LTL公式可以表示為：!F((goatw!=goatb)&(goatw!=goatg)&(goatb!=w))門鈴問題某戶的門鈴聲整天不斷，于是，他請人在大門前設(shè)計(jì)了一排6個按鈕，其中只有一個是通門鈴的。來訪者只要摁錯了一個按鈕，哪怕是和正確的同時摁，整個電鈴系統(tǒng)將立即停止工作。在大門的按鈕旁邊，貼有一張告示，上面寫著：“A在B的左邊；B是C右邊的第三個；C在D的右邊；D緊靠著E；E和A中間隔一個按鈕。請摁上面沒有提到的那個按鈕?！眴枺哼@6個按鈕中，通門鈴的按鈕處于什么位置？建模過程：根據(jù)分析，B是C右邊第三個門鈴，那么可以門鈴位置可以確定為CxxB。又D在C的左邊，那么就是說C的左邊仍然有門鈴，C的位置不可能是1，4，5，6，這樣就可以確定C的位置只能是2或者3。當(dāng)C的位置確定時，B的位置相應(yīng)的也就確定了；而D的位置可以根據(jù)C的位置來判斷，當(dāng)C的位置是2時，D的位置就只能是1

了；當(dāng)C的位置是３時，D的位置可能是１或者２；同理E的位置可以根據(jù)D的位置來判斷可能性，而Ａ呢可以根據(jù)Ｅ的位置來判斷。各門鈴位置不重復(fù)，所以Ａ、Ｅ、Ｃ位置各不同。用LTL公式表示為：

!F(a!=c&c!=e)

MODULEmainnext(b):=caseVARnext(c)=2:5;

a:{1,2,3,4,5,6,0};1:6;

b:{1,2,3,4,5,6,0};esac;

c:{1,2,3,4,5,6,0};next(e):=case

d:{1,2,3,4,5,6,0};next(d)=1:2;

e:{1,2,3,4,5,6,0};1:{1,3};ASSIGNesac;

init(a):=0;next(a):=case

init(b):=0;next(e)=1:3;

init(c):=0;next(e)=2:4;

init(d):=0;1:{1,5};

init(e):=0;esac;

next(c):={2,3};LTLSPEC

next(d):=case!F(a!=c&c!=e)

next(c)=2:1;

1:{1,2};

esac;

身份辨認(rèn)我畢業(yè)于一所政法大學(xué)，我的同學(xué)(包括我在內(nèi))不是做了法官就是做了律師。在一次同學(xué)聚會上，有16位同學(xué)出席。我統(tǒng)計(jì)了一