SAT问题

《实验二SAT问题 》实验报告 题目 SAT问题 姓名及分工 日期 2012/11/23 问题描述 SAT问题也称为合取范式的可满足问题，一个合取范式形如：A1∧A2∧…∧An，子句Ai（1≤i≤n）形如：a1∨a2∨…∨ak，其中，ai称为文字，为某一布尔变量或该布尔变量的非。SAT问题是指：是否存在一组对所有布尔变量的赋值（TRUE或FALSE），使得整个合取范式取值为真。 2. 实验目的 （1）掌握NP完全问题的特点； （2）理解这样一个观点：NP完全问题的算法具有指数时间，而指数时间算法的计算时间随着问题规模的增长而快速增长。 3. 实验要求 （1）设计算法求解SAT问题； （2）设定问题规模为3、5、10、20、50，设计实验程序考察算法的时间性能。 算法思路 1.将一个长度为n的二进制串s初始化为00…0； 2.循环直到串s为11…1 2.1 将二进制串s代入给定的合取范式中； 2.2 若合取范式取值为TRUE，则将串s作为结果输出，算法结束； 2.3 否则，将串s加1； 3. 输出“无解” (对于合取范式，可以手工输入，也可以在程序开头直接初始化) 算法实现 #include #include #include #include //函数声明 void input(); void output(); //全局变量 int m,k;//m：析取范式个数，k:数据规模 //结构体 struct satlist { int result;//判断当前析取范式是否取值‘1’ int n;//当前析取范式的文字个数 int a[50];//当前析取范式的具体内容 satlist *next; }SAT[50]; void main() { input(); output(); } void input() { printf("请输入析取范式A的个数,问题规模k的值(如：3 4)
"); scanf("%d%d",&m,&k); for(int i=0;i",i+1); scanf("%d",&SAT[i].n); while(SAT[i].n>k) { printf("输入有误：文字个数超过问题规模，请再次输入
"); printf("请输入第%d个析取范式中文字的个数
",i+1); scanf("%d",&SAT[i].n); } for(int j=0;j",i+1,j+1); scanf("%d",&SAT[i].a[j]); while(SAT[i].a[j]>k) { printf("输入有误：文字下标超过问题规模，请再次输入
"); j=j-1; } for(int w=0;w"); j=j-1; break; } } } } } void output() { int s[50]={0};//各个文字对应的取值 int j=0;//指向各个析取范式 double time=pow(2,k);//从000-111的次数，2的K次方 double fab;//绝对值 int i=0;//result：是否使得合取范式=1，i：依次从000-111 int h=0;//把当前i的值转换为二进制即各个文字对应的取值 int w=0;//转换二进制中用来指示下标位置 printf("测试1
"); for(int t=0;t"); fab=fabs(SAT[j].a[t]);//求绝对值 if(((SAT[j].a[t])/fab)==1)//符号正或负时 { printf("测试 判断正号
"); SAT[j].result=(SAT[j].result||s[(int)fab-1]);//输入文字下标对应符号正号则该文字取值不变 } if(((SAT[j].a[t])/fab)==-1) { printf("测试 判断负号
"); SAT[j].result=(SAT[j].result||(