「正式」證明是一種模糊的描述。我將畫出一個證明,大概將在一篇研究論文中出現的詳細程度(可能低於算法課程中設置的問題所需的詳細程度)。
貪婪算法顯然會產生有效的匹配。 (由於實踐中形式方法的困難,這實際上是對「清楚」這個詞的濫用。)
爲了表明這種匹配是最大尺寸,我們通過歸納證明以下技術說明。對於不大於這個尺寸的所有k,在貪婪匹配中存在匹配k個最少賣方的最大匹配。
基本情況是k = 0。我們可以採取任何舊的最大匹配,因爲聲明是真實的真實的(0最少是空集)。
對於k> 0,歸納步驟證明k-1的陳述意味着對於k的陳述。存在一個最大匹配M,它與k - 1最少銷售者的貪婪解決方案一致,但可能不是最不重要的,我們稱之爲sk。現在來一個案例的論點。
案例1:SK匹配M和貪婪的解決方案。讓bG成爲sk的買方,並且b是sk的買方。如果bG = bM,那麼我們就完成了。否則,由於貪婪解決方案選擇了除了僅有s1,...,sk-1(其與M中的相同方式相匹配)的買方之外的所有買方中的最小合格買方。如果M中有bG,則將sk的買方切換到bG。否則,將M與bM交換bG;先前從bG購買的賣方獲得更大的買方,所以交換是有效的。
案例2:sk在M中匹配,但不在貪婪的解決方案中。那麼貪婪的解決方案就是M的一個子集。這是不可能的,因爲sk中的買主在貪婪的解決方案中可用(貪婪的解決方案是最大的)。
案例3:sk在M中不匹配一些更大的賣家匹配;將其替換爲sk並應用其他案例之一。
正式驗證*很難*。 – 2014-10-05 02:51:32
我會建議嘗試將其轉換爲代碼或至少pududo代碼,並在http://codereview.stackexchange.com/上提出相同的問題。 – 2014-10-05 03:02:37