forked from AlexFanw/HUSTER-CS
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathmain.c
194 lines (169 loc) · 7.71 KB
/
main.c
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
//
// main.c
// 2019SAT_word
//
// Created by 范唯 on 2019/3/8.
// Copyright © 2019 范唯. All rights reserved.
//
#include <stdio.h>
#include <stdlib.h>
#include <stdbool.h>
#include <string.h>
#include <math.h>
#include <time.h>
#include "Header.h"
int main() {
printf("Checking File...\n");
char*filename;
FILE*fp;
filename="/Users/alexfan/Desktop/University/2019数据结构课程设计/综合程序设计任务及指导学生包/SAT测试备选算例/基准算例/功能测试/sat-20.cnf";
filename="/Users/alexfan/Desktop/University/2019数据结构课程设计/综合程序设计任务及指导学生包/SAT测试备选算例/满足算例/M/sud00001.cnf";
// filename="/Users/alexfan/Desktop/University/2019数据结构课程设计/综合程序设计任务及指导学生包/SAT测试备选算例/基准算例/性能测试/ais10.cnf";//算不出来
// filename="/Users/alexfan/Desktop/University/2019数据结构课程设计/综合程序设计任务及指导学生包/SAT测试备选算例/满足算例/S/problem3-100.cnf";//很慢
// filename="/Users/alexfan/Desktop/University/2019数据结构课程设计/综合程序设计任务及指导学生包/SAT测试备选算例/满足算例/M/problem5-200.cnf";//算不出来
// filename="/Users/alexfan/Desktop/University/2019数据结构课程设计/综合程序设计任务及指导学生包/SAT测试备选算例/满足算例/M/problem12-200.cnf";//算不出来
// filename="/Users/alexfan/Desktop/University/2019数据结构课程设计/综合程序设计任务及指导学生包/SAT测试备选算例/满足算例/M/bart17.shuffled-231.cnf";//算不出来
// filename="/Users/alexfan/Desktop/University/2019数据结构课程设计/综合程序设计任务及指导学生包/SAT测试备选算例/满足算例/M/m-mod2c-rand3bip-sat-220-3.shuffled-as.sat05-2490-311.cnf";//算不出来
//filename="";
// filename="/Users/alexfan/Desktop/University/2019数据结构课程设计/综合程序设计任务及指导学生包/SAT测试备选算例/满足算例/L/eh-dp04s04.shuffled-1075.cnf";
fp=fopen(filename,"r");
int ch;
char p[50],cnf[50];
char pp='p';
int bol_number=0;
int clause_number=0;
fscanf(fp,"%s",p);
while (1) {
if(strcmp(p,&pp)==0){
printf("File in order\n");
break;
}
else fscanf(fp,"%s",p);
}//跳过第一行
fscanf(fp, "%s %d %d",cnf,&bol_number,&clause_number);
printf("%s %s %d %d\n",p,cnf,bol_number,clause_number);//读取打印第一行有效信息
fscanf(fp,"%d",&ch);
clock_t start,finish;
double duration;
start=clock();
//模块1:创建所有bool元素
bool_element one;
bool_element *b_element=&one;
bool_element *b_element_cal=b_element;
for (int i=1; i<=bol_number; ++i) {
b_element_cal->sts=true;
b_element_cal->name=i;
b_element_cal->lock=false;//不上锁
b_element_cal->back=false;//不在判定列表
if((b_element_cal->next=(bool_element*)malloc(sizeof(bool_element)))==NULL)exit(-5);
if(i<bol_number)b_element_cal=b_element_cal->next;
else{
free(b_element_cal->next);
b_element_cal->next=NULL;
break;
}
}
bool_element*b_element_point[bol_number];
bool_element*b=b_element;
for (int i=0; b!=NULL; i++) {
b_element_point[i]=b;
b=b->next;
}
//模块1:end——创建所有的bol值
//模块2：创建所有子句
clause_root *first_root;
first_root=(clause_root*)malloc(sizeof(clause_root));
first_root->exit=true;
first_root->root=(clause_line*)malloc(sizeof(clause_line));
if(ch!=0){
int ch_abs_first=abs(ch);
first_root->root->c_element=b_element_point[ch_abs_first-1];
first_root->root->exit=true;
if(ch<0) first_root->root->c_element_head=false;
else first_root->root->c_element_head=true;
// printf("第一个子句的根为%d",first_root->root->c_element->name);
}//创建第一个子句的根
else exit(-1);
clause_root*root_cal=first_root;
while (1) {
if(ch==0){
if(fscanf(fp, "%d", &ch)>0){
if(ch==0) exit(-1);//空子句，错误
else if (ch!=0){//如果新读入的ch不为0，那么就创建一个新的根
if((root_cal->next_root=(clause_root*)malloc(sizeof(clause_root)))==NULL)exit(-6);
root_cal=root_cal->next_root;
root_cal->exit=true;
int ch_abs_0=abs(ch);
// printf("根:%d\n",ch);
if ((root_cal->root=(clause_line*)malloc(sizeof(clause_line)))==NULL)exit(-7);
root_cal->root->c_element=b_element_point[ch_abs_0-1];
root_cal->root->exit=true;
if(ch<0) root_cal->root->c_element_head=false;
else root_cal->root->c_element_head=true;
}
else break;
}
else break;
}
else if(ch!=0){
clause_line*clause_element=root_cal->root;
while(ch!=0){//当前ch是根，需要再读一次
if(fscanf(fp, "%d", &ch)>0){
if(ch==0) {
clause_element->next=NULL;//创建一个循环链表
break;
}
else{
if((clause_element->next=(clause_line*)malloc(sizeof(clause_line)))==NULL)exit(-8);
clause_element=clause_element->next;
int ch_abs_1=abs(ch);
clause_element->c_element=b_element_point[ch_abs_1-1];
clause_element->exit=true;//该元素在子句中是存在的
if(ch<0)clause_element->c_element_head=false;
else clause_element->c_element_head=true;
}}}}}
//模块2:end——创建所有子句
//模块1和2结束后，我们现在获得了fisrt_root 和b_elementl两个指针，一个里面存了所有的子句，一个存了y所有的元素
//模块3:将所有子句内部按照大小重排列
clause_root*exchange_clause=first_root;
while(exchange_clause!=NULL) {
clause_line*range_clause=exchange_clause->root;
range_clause=re_range_clause(range_clause);
for (; range_clause!=NULL; ) {
range_clause=range_clause->next;
}
exchange_clause=exchange_clause->next_root;
}
//模块3——end
//模块4:将所有子句的根按照大小重新排列
// clause_root*exchange_root=first_root;
// first_root=re_range_root(exchange_root);
// root_print(first_root);
//模块4-end
//模块5:DPLL算法
dpll_cnf(first_root, bol_number, b_element_point);
// 模块5——end
if(all_cnf_true(first_root)==false)printf("s:0\n");
else printf("s:1\n");
bool_element*bool_element_cal=b_element;
printf("v:");
while (bool_element_cal!=NULL) {
if (bool_element_cal->sts==true) {
printf("%d ",bool_element_cal->name);
}
else printf("-%d ",bool_element_cal->name);
bool_element_cal=bool_element_cal->next;
}//打印所有元素的状态。最终结果
fclose(fp);
fp=NULL;
free(first_root->next_root);
first_root->next_root=NULL;
free(b_element->next);
free(first_root);
first_root=NULL;
b_element->next=NULL;
finish=clock();
duration=(double)(finish - start)/CLOCKS_PER_SEC;
printf("\nt:%fms\n",1000*duration);
return 0;
}