Sat问题——穷举（这里读文件时间很浪费，最初写的，可以进行很多优化，其他优化算法目前不能发布）

说明：

1、此方法可做以下几点优化：

（1）文件读一次即可，保存在一个二维数组里面

（2）自增形式的穷举是比较浪费时间的，或许可以利用二进制进行，二进制的布尔运算效率应该很高

2、穷举法是比较笨拙的方式，可以使用其他算法实现，今后合适的情况下，将会陆续公布新的解决方案。

3、请大家注意，这是本人所作的练习，不具有代表性，如参考请慎重。

/*使用穷举法找出测试结果
*实现思路
* 1、初始化數組
* 2、列出數組所有的組合
* 2.1 验证组合是否满足sat，即是否是它的解
* 2.2 如果找到解，那么退出
*/
#include<iostream>
#include<fstream>
#include<string>
#include<math.h>
#include <stdlib.h>
using namespace std;
#define ARRAYLENGTH 20
#define VARIABLE 3
//定义数组存储变元个数
int array[ARRAYLENGTH];
int variable[VARIABLE];
//初始化数组
void initialArray(int temp[],int length)
{
for(int i=0;i<length;i++)
{
temp[i]=0;
}
}
//自增的數組，模仿二進制加法 ,当数组元素都是1时，说明已经遍历完，则返回false；如果没有遍历完，那么返回true；
bool addByOne(int temp[],int length)
{
for(int i=length-1;i>=0;i--)
{
if(temp[i]==1)
{
if(i==0)
{
return false;
}
temp[i]=0;
}
else
{
temp[i]=1;
return true;
}
}
}
//把字符串转化为int类型
int stringToInt(string str)
{
int result=0;
if(str[0]=='-')
{
for(int i=str.size()-1,j=0;i>0;i--,j++)
{
//cout<<str[i]<<"bbbb"<<pow(10,j)<<"cccc"<<str[i]-'0'<<"dddd"<<endl;
result+=(str[i]-'0')*pow(10,j);
//cout<<result<<"aaaaa"<<endl;
}
return 0-result;
}
else
{
for(int i=str.size()-1,j=0;i>=0;i--,j++)
{
result+=(str[i]-'0')*pow(10,j);
//cout<<result<<"aaaaa"<<endl;
}
return result;
}
}
//字符串分割， 参数str是目标字符串，temp是长度为3的数组，spiltChar是分割字符
void spiltForStr(string str, int temp[], char spiltChar)
{
int index=0;
int j=0;
for(int i=0;str[i]!='\0';i++)
{
if(str[i]==spiltChar)
{
string substring=str.substr(index,i-index);

//cout<<"hehe"<<substring<<"beiju"<<endl;

int result = stringToInt(substring);
temp[j]=result;
//cout<<result<<"aaaaaa"<<endl;
index=i+1;
j++;
}
}
//cout<<temp[0]<<" + "<<temp[1]<<" + "<<temp[2]<<endl;
}
bool testArrayIsSat(int temp[],int length,int totalArray[],int totalLength)
{
int sum=0;
for(int i=0;i<length;i++)
{
if(temp[i]<0)
{
if(totalArray[0-temp[i]-1]==0)
{
sum+=1;
}
}
else
{
sum+=totalArray[temp[i]-1];
}
}
if(sum>0)
return true;
else
return false;
}
bool checkForSat(int temp[],int length)
{
//ofstream fout;
//fout.open("10212764\\satresult.txt");
//fout<<"# 10212764"<<endl;
ifstream fin("test\\t1.txt");
string str="";
while(getline(fin,str))
{
if(str[0]!='c'&&str[0]!='0'&&str[0]!='%'&&str[0]!='p')
{
if(str[0]==' ')
{
//cout<<str<<endl;
str=str.substr(1,str.size());
spiltForStr(str,variable, ' ');
if(!testArrayIsSat(variable,VARIABLE,array,ARRAYLENGTH))
{
return false;
}
//cout<<endl;
}
else
{
//cout<<str<<endl;
spiltForStr(str,variable, ' ');
if(!testArrayIsSat(variable,VARIABLE,array,ARRAYLENGTH))
{
return false;
}
//cout<<endl;
}

}
else
{
if(str[0]=='p')
{
;
}
}
}
//fout.close();
fin.close();
return true;
}
int main()
{
//初始化Array
initialArray(array,ARRAYLENGTH);
/*
cout<<"數組初始化數據"<<endl;
for(int i=0;i<ARRAYLENGTH;i++)
{
cout<<array[i]<<" ";
}
cout<<"數組初始化數據結束"<<endl;
*/
bool flag=true;
//用来标识枚举所有组合之后是否找到解，找到则为true，否则则为false；
bool isSatOrNot=false;
for(int i=0;flag;i++)
{
//枚举所有的组合
flag = addByOne(array,ARRAYLENGTH);
//测试是否符合预期的枚举所有组合
/*
for(int i=0;i<ARRAYLENGTH;i++)
{
cout<<array[i]<<" ";
}
cout<<endl<<"the end of sample"<<endl;
*/

isSatOrNot = checkForSat(array,ARRAYLENGTH);
if(isSatOrNot)
{
//if(checkForSat(array,ARRAYLENGTH))
//{
for(int j=0;j<ARRAYLENGTH;j++)
{

cout<<array[j]<<" ";
if(j%50==0&&j!=0)
{
cout<<endl;
}

}
//}
flag=false;
}

}

system("pause");
return 0;
}