Theorem Prover
今天使用了一下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的程序:#include <stdio.h>
#define A 'A'
#define B 'B'
#define C 'C'
#define D 'D'
#define E 'E'
struct Match{
char a,b,c,d;//a<b, c<d,a<c
}M={
{A,B,C,D},
{A,B,C,E},
{A,B,D,E},
{A,C,B,D},
{A,C,B,E},
{A,C,D,E},
{A,D,B,C},
{A,D,B,E},
{A,D,C,E},
{A,E,B,C},
{A,E,B,D},
{A,E,C,D},
{B,C,D,E},
{B,D,C,E},
{B,E,C,D}
};
int edges;
#define SET_EDGES(u1,v1,u2,v2) \
edges=1;\
void init_edges()
{
int i,j;
for(i=0;i<15;i++)for(j=0;j<15;j++){
if(i==j)continue;
if(M.a==M.a&&M.b==M.b){
edges=1;
}else if(M.c==M.c&&M.d==M.d){
if(M.b>M.d){
edges=1;
}
}else if(M.a==M.c&&M.b==M.d){
edges=1;
}else if(M.c==M.a&&M.d==M.b){
if(M.b>M.d){
edges=1;
}
}
}
}
void dump_edges()
{
int i,j;
for(i=0;i<15;i++)for(j=0;j<15;j++){
if(edges){
printf("%c%c%c%c=>%c%c%c%c\n",M.a,M.b,M.c,M.d,M.a,M.b,M.c,M.d);
}
}
printf("\n");
}
int best=8;
int depth=0;
int used;
int stacks;
void dump()
{
int i;
printf("Candidate depth %d:\t",depth);
for(i=0;i<depth;i++){
int p=stacks;
printf("%c%c%c%c ",M.a,M.b,M.c,M.d);
}
printf("\n");
}
static int cc;
int check_succ()
{
char line;
FILE *f=fopen("1.cvc","w");
fprintf(f,"A,B,C,D,E:INT;\n");
fprintf(f,"ASSERT A>B AND B>C AND C>D AND D>E;\n");
int i;
for(i=0;i<depth-1;i++){
int p=stacks,q=stacks;
if(M.a==M.a&&M.b==M.b){
fprintf(f,"ASSERT %c+%c>%c+%c;\n",M.a,M.b,M.c,M.d);
}else if(M.c==M.c&&M.d==M.d){
fprintf(f,"ASSERT %c+%c>%c+%c;\n",M.c,M.d,M.a,M.b);
}else if(M.a==M.c&&M.b==M.d){
fprintf(f,"ASSERT %c+%c>%c+%c;\n",M.a,M.b,M.c,M.d);
}else if(M.c==M.a&&M.d==M.b){
fprintf(f,"ASSERT %c+%c>%c+%c;\n",M.c,M.d,M.a,M.b);
}
}
fprintf(f,"CHECKSAT;");
fclose(f);
system("cvc3 < 1.cvc >cvc.out");
f=fopen("cvc.out","r");
fgets(line,100,f);
fclose(f);
if(strncmp(line,"Uns",3)==0){
return 0;
}else{
sprintf(line,"mv 1.cvc cvc%d.cvc",cc);
cc++;
system(line);
return 1;
}
}
void search()
{
int i;
int p=stacks;
if(depth>=best){
if(check_succ()){
best=depth;
dump();
}
}
for(i=0;i<15;i++){
if(!used&&edges!=0){
used=1;stacks=i;
search();
used=0;depth--;
}
}
}
int main()
{
int i;
init_edges();
//dump_edges();
for(i=0;i<15;i++){
stacks=i;
used=1;
depth=1;
search();
used=0;
}
}
页:
[1]