Theorem Prover

mathe

今天使用了一下cvc3,一种一阶逻辑证明工具（类似的工具还有Z3,simplify等) 起因是看到百度数学吧中一个题目: 五名网球队员参加一次双打比赛，设选手A的分数为R(A),任意两名选手的分数不同，任意2名选手的分数和也各不相同。若R(A)+R(B)>R(C)+R(D)则称(A,B)这对选手胜(C，D)这对选手。于是将(C,D)拆散，另外两队选手(C,E)或(D,E)之一与(A,B)继续下一场比赛。直到某两对以前曾经交过手的组合再次相遇(相遇时比赛停止)，求比赛最多能进行多少场 由此写了一个使用cvc3的程序:

1. #include <stdio.h>
3. #define A 'A'
4. #define B 'B'
5. #define C 'C'
6. #define D 'D'
7. #define E 'E'
8. struct Match{
9. char a,b,c,d;//a<b, c<d,a<c
10. }M[15]={
11. {A,B,C,D},
12. {A,B,C,E},
13. {A,B,D,E},
14. {A,C,B,D},
15. {A,C,B,E},
16. {A,C,D,E},
17. {A,D,B,C},
18. {A,D,B,E},
19. {A,D,C,E},
20. {A,E,B,C},
21. {A,E,B,D},
22. {A,E,C,D},
23. {B,C,D,E},
24. {B,D,C,E},
25. {B,E,C,D}
26. };
27. int edges[15][15];
28. #define SET_EDGES(u1,v1,u2,v2) \
29. edges[i][j]=1;\
31. void init_edges()
32. {
33. int i,j;
34. for(i=0;i<15;i++)for(j=0;j<15;j++){
35. if(i==j)continue;
36. if(M[i].a==M[j].a&&M[i].b==M[j].b){
37. edges[i][j]=1;
38. }else if(M[i].c==M[j].c&&M[i].d==M[j].d){
39. if(M[i].b>M[i].d){
40. edges[i][j]=1;
41. }
42. }else if(M[i].a==M[j].c&&M[i].b==M[j].d){
43. edges[i][j]=1;
44. }else if(M[i].c==M[j].a&&M[i].d==M[j].b){
45. if(M[i].b>M[i].d){
46. edges[i][j]=1;
47. }
48. }
49. }
50. }
52. void dump_edges()
53. {
54. int i,j;
55. for(i=0;i<15;i++)for(j=0;j<15;j++){
56. if(edges[i][j]){
57. printf("%c%c%c%c=>%c%c%c%c\n",M[i].a,M[i].b,M[i].c,M[i].d,M[j].a,M[j].b,M[j].c,M[j].d);
58. }
59. }
60. printf("\n");
61. }
63. int best=8;
64. int depth=0;
65. int used[15];
66. int stacks[15];
68. void dump()
69. {
70. int i;
71. printf("Candidate depth %d:\t",depth);
72. for(i=0;i<depth;i++){
73. int p=stacks[i];
74. printf("%c%c%c%c ",M[p].a,M[p].b,M[p].c,M[p].d);
75. }
76. printf("\n");
77. }
79. static int cc;
80. int check_succ()
81. {
82. char line[100];
83. FILE *f=fopen("1.cvc","w");
84. fprintf(f,"A,B,C,D,E:INT;\n");
85. fprintf(f,"ASSERT A>B AND B>C AND C>D AND D>E;\n");
86. int i;
87. for(i=0;i<depth-1;i++){
88. int p=stacks[i],q=stacks[i+1];
89. if(M[p].a==M[q].a&&M[p].b==M[q].b){
90. fprintf(f,"ASSERT %c+%c>%c+%c;\n",M[p].a,M[p].b,M[p].c,M[p].d);
91. }else if(M[p].c==M[q].c&&M[p].d==M[q].d){
92. fprintf(f,"ASSERT %c+%c>%c+%c;\n",M[p].c,M[p].d,M[p].a,M[p].b);
93. }else if(M[p].a==M[q].c&&M[p].b==M[q].d){
94. fprintf(f,"ASSERT %c+%c>%c+%c;\n",M[p].a,M[p].b,M[p].c,M[p].d);
95. }else if(M[p].c==M[q].a&&M[p].d==M[q].b){
96. fprintf(f,"ASSERT %c+%c>%c+%c;\n",M[p].c,M[p].d,M[p].a,M[p].b);
97. }
98. }
99. fprintf(f,"CHECKSAT;");
100. fclose(f);
101. system("cvc3 < 1.cvc >cvc.out");
102. f=fopen("cvc.out","r");
103. fgets(line,100,f);
104. fclose(f);
105. if(strncmp(line,"Uns",3)==0){
106. return 0;
107. }else{
108. sprintf(line,"mv 1.cvc cvc%d.cvc",cc);
109. cc++;
110. system(line);
111. return 1;
112. }
113. }
115. void search()
116. {
117. int i;
118. int p=stacks[depth-1];
119. if(depth>=best){
120. if(check_succ()){
121. best=depth;
122. dump();
123. }
124. }
125. for(i=0;i<15;i++){
126. if(!used[i]&&edges[p][i]!=0){
127. used[i]=1;stacks[depth++]=i;
128. search();
129. used[i]=0;depth--;
130. }
131. }
132. }
134. int main()
135. {
136. int i;
137. init_edges();
138. //dump_edges();
139. for(i=0;i<15;i++){
140. stacks[0]=i;
141. used[i]=1;
142. depth=1;
143. search();
144. used[i]=0;
145. }
146. }

复制代码