遞迴_CH0303_遞迴實現排列型列舉_遞迴演算法正確性證明範例
先給出AC程式碼, 然後給出程式正確性的形式化證明.
//CH0303_遞迴實現排列型列舉 #include <iostream> #include <cstdio> #include <vector> using namespace std; const int MAX = 1e2; int n; vector<int> choosn; bool used[MAX];//used[i]為true對應choosn中包含元素i, false則不包含 void solve(){ if(choosn.size() == n){ for(int i = 0; i < n; ++i) cout << choosn[i] << " "; cout << endl; return; } for(int i = 1; i <= n; ++i) if(!used[i]) used[i] = true, choosn.push_back(i), solve(), choosn.pop_back(), used[i] = false; } int main(){ scanf("%d", &n); solve(); return 0; }
程式正確性的形式化證明:
定義集合 = { x | x為一次對solve的呼叫, 且choosn.size() = i, choosn[0...i - 1]對應{1...n}取i個元素的一個排列, 且對於所有的j choosn[0...i - 1], 滿足used[ j ]為false, 除此之外used中的元素均為true }
歸納基礎: 對於集中的所有元素程式能夠按字典序遞增的順序列印1,...,n的所有前n的元素對應choosn[0...choosn.size() - 1]的全排列, 並且在返回上級呼叫函式時, choosn和used被還原為初始呼叫的狀態.
遞推: 假設對於集 (2 =< k <= n)中的所有元素程式能夠按字典序遞增的順序列印1,...,n的所有前choosn.size()個元素為choosn[0...choosn.size() - 1]的全排列, 並且在返回上級呼叫函式時, choosn和used被還原為初始呼叫的狀態. 容易推知設對於集中的所有元素程式能夠按字典序遞增的順序列印1,...,n的所有前n的元素對應choosn[0...choosn.size() - 1]的全排列, 並且在返回上級呼叫函式時, choosn和used被還原為初始呼叫的狀態.
綜上述, 對於集中的所有元素程式能夠按字典序遞增的順序列印1,...,n的所有前n的元素對應choosn[0...choosn.size() - 1]的全排列, 並且在返回上級呼叫函式時, choosn和used被還原為初始呼叫的狀態. 進一步分析, 對於(初始choosn為空)中的所有元素能夠按字典序遞增的順序列印1,...,n的所有全排列. 並且在返回上級呼叫函式時, choosn和used被還原為初始呼叫的狀態. 從而程式正確性得證.
常見的用於生成全排列的還有如下演算法, 但是下面這種演算法並非按照字典序遞增(或遞減)列印每個全排列, 同上, 在給出程式碼後將給出程式正確性的形式化證明.
//CH0303_遞迴實現排列型列舉
#include <iostream>
#include <cstdio>
using namespace std;
const int MAX = 1e2;
int seq[MAX], n;
void solve(int cur){
if(cur == n){
for(int i = 1; i <= n; ++i) cout << seq[i] << " "; cout << endl;
return;
}
for(int i = cur; i <= n; ++i)
swap(seq[cur], seq[i]), solve(cur + 1), swap(seq[cur], seq[i]);
}
int main(){
scanf("%d", &n); for(int i = 1; i <= n; ++i) seq[i] = i;
solve(1);
return 0;
}
定義集合 = { x | x為一次對solve(i)的呼叫, 且seq[1...n]對應1...n的一個全排列}
歸納基礎: 對於集中的所有元素a, 程式均能夠按字典序遞增的順序列印1,...,n的所有前n - 1個元素對應seq[1...n - 1]的全排列, 並且在返回上級呼叫函式時, seq被還原為初始呼叫狀態.
遞推. 假設對於集 (3 =< k <= n)中的所有元素a, 程式均能夠按字典序遞增的順序列印1,...,n的所有前k - 1個元素對應seq[1...k - 1]的全排列, 並且在返回上級呼叫函式時, seq被還原為初始呼叫狀態. 對於集中的元素, 根據程式第12, 13行的程式碼很容易確定程式均能夠按字典序遞增的順序列印1,...,n的所有前k - 2個元素對應seq[1...k - 2]的全排列, 並且在返回上級呼叫函式時, seq被還原為初始呼叫狀態.
綜上述, 對於集中的所有元素a, 程式均能夠按字典序遞增的順序列印1,...,n的所有前1個元素對應seq[1...1]的全排列, 並且在返回上級呼叫函式時, seq被還原為初始呼叫狀態. 再次根據根據程式第12, 13行的程式碼可知對於集中的所有元素, 程式均能夠按字典序遞增的順序列印1,...,n的所有全排列, 並且在返回上級呼叫函式時, seq被還原為初始呼叫狀態. 也即程式正確性得證.
特別的, 如果將上述程式修改為下面所示程式碼, 那麼仍能夠按照字典序遞增輸出1...n的所有全排列, 並且AC, 至於程式正確性的證明過程, 此處不再贅述.
//CH0303_遞迴實現排列型列舉
#include <iostream>
#include <cstdio>
#include <map>
using namespace std;
const int MAX = 1e2;
int seq[MAX], n;
void solve(int cur){
if(cur == n){
for(int i = 1; i <= n; ++i) cout << seq[i] << " "; cout << endl;
return;
}
map<int, int> sq;//key: 元素值, value: 元素在seq中下標
for(int i = cur; i <= n; ++i) sq[seq[i]] = i;
for(map<int, int>::iterator it = sq.begin(); it != sq.end(); ++it)
swap(seq[cur], seq[it->second]), solve(cur + 1), swap(seq[cur], seq[it->second]);
}
int main(){
scanf("%d", &n); for(int i = 1; i <= n; ++i) seq[i] = i;
solve(1);
return 0;
}