标签：
Alice recently started to work for a hardware design company and as a part of her job, she needs to identify defects in fabricated ntegrated circuits. An approach for identifying these defects boils down to solving a satisfiability instance. She needs your help to write a program to do this task.
The first line of input contains a single integer, not more than 5, indicating the number of test cases to follow. The first line of each test case contains two integers n and m where 1 ≤ n ≤ 20 indicates he number of variables and 1 ≤ m ≤ 100 indicates the number of clauses. Then, m lines follow corresponding to each clause. Each clause is a disjunction of literals in the form Xi or ~Xi for some 1 ≤ i ≤ n, where Xi indicates the negation of the literal Xi. The “or” operator is denoted by a ‘v’ character and is seperated from literals with a single pace.
For each test case, display satisfiable on a single line if there is a satisfiable assignment; otherwise
display unsatisfiable.
2
3 3
X1 v X2
~X1
~X2 v X3
3 5
X1 v X2 v X3
X1 v ~X2
X2 v ~X3
X3 v ~X1
~X1 v ~X2 v ~X3
satisfiable
unsatisfiable
解题:以为可以用位运算优化，结果，却发现，错了！好吧，还是上暴力的吧
1 #include <bits/stdc++.h> 2 #define pii pair<int,int> 3 using namespace std; 4 const int maxn = 200; 5 char str[maxn]; 6 vector< pii >s[maxn]; 7 int n,m; 8 void exp2num(int idx) { 9 bool flag = true; 10 for(int i = 0,ret = 0; str[i];) { 11 if(str[i] == ‘~‘) flag = false; 12 if(isdigit(str[i])) { 13 while(isdigit(str[i])) ret = ret*10 + (str[i++]-‘0‘); 14 s[idx].push_back(make_pair(ret-1,flag)); 15 ret = 0; 16 flag = true; 17 } else i++; 18 } 19 } 20 bool check(int o){ 21 for(int i = 0; i < m; ++i){ 22 bool flag = false; 23 for(int j = s[i].size()-1; j >= 0; --j){ 24 if(s[i][j].second == ((o>>s[i][j].first)&1)){ 25 flag = true; 26 break; 27 } 28 } 29 if(!flag) return false; 30 } 31 return true; 32 } 33 int main(){ 34 int T; 35 scanf("%d",&T); 36 while(T--){ 37 scanf("%d %d",&n,&m); 38 getchar(); 39 for(int i = 0; i < m; ++i){ 40 s[i].clear(); 41 gets(str); 42 exp2num(i); 43 } 44 bool ok = false; 45 for(int i = 0; i < (1<<n) && !ok; ++i) 46 ok = check(i); 47 puts(ok?"satisfiable":"unsatisfiable"); 48 } 49 return 0; 50 }
CSUOJ 1637 Yet Satisfiability Again!
标签：
原文地址：http://www.cnblogs.com/crackpotisback/p/4551487.html
