/* 	SAT solver
		Bin Fu binf@cs.cmu.edu
		2009.02.17

		modified by Byron Boots
		2009.02.17
		
		compile with g++ -O3 satSolver.cpp -o satSolver
*/

#include <iostream>
#include <fstream>
#include <string>
#include <time.h>

#define MAX_CLAUSE_SIZE 3

using namespace std;

int varNum;
int clauseNum;

int* varDec;	//0 unassined. 1 pos, -1 neg
int** clauseVar;
int* clauseVal; //0 pending. 1 pos, -1 neg
int* clauseLength;

inline int decidedVar(int index)	//index: clause index.
{
	int sum = 0;
	for(int i=0; i < clauseLength[index];i++)
	{
		sum = sum+abs(varDec[abs(clauseVar[index][i])]);
	}
	return sum;
}

inline int evaluateClause(int index)	//index: clause index
//1= true. -1=false. 0=pending
{
	for(int i = 0; i<clauseLength[index];i++)
	{
		if (varDec[abs(clauseVar[index][i])]!=0 && varDec[abs(clauseVar[index][i])]*clauseVar[index][i]>0)
			return 1;
	}
	if (decidedVar(index)==clauseLength[index])
		return -1;
	else
		return 0;
}

inline bool updateClause()	//false=conflict!
{
	for (int i=0;i<clauseNum;i++)
	{
		clauseVal[i]=evaluateClause(i);
		if (clauseVal[i]==-1)
			return false;
	}
	return true;
}

inline int hornHeuristic(int index)	//-1 Not choose. 0,1,2 choose
{
	int numPos=0;
	if (clauseVal[index]==1)
		return -1;
	
	int choose=-1;
	for (int j=0;j<clauseLength[index];j++)
	{
		if (varDec[abs(clauseVar[index][j])]==0 && clauseVar[index][j]>0)
		{
			choose=j;
			numPos++;
		}
	}
	if (numPos>1)
		return choose;
	else
		return -1;
}

void readformula(char * filename)
{
	// read into data structure
	ifstream fin;
	fin.open(filename);
	if (fin.bad()) {
		cerr << "Cannot open " << filename << "!" << endl;
		exit(-1);
	}
	string s;
	int state=0;
	int currentClauseNum=0;
	while (getline(fin,s))
	{
		if (state==0)
		{
			if (s.substr(0,1)=="p")
			{
				state=1;
				int pos=s.find(" ",6);

				varNum = atoi(s.substr(5,pos-5).c_str());
				clauseNum = atoi(s.substr(pos,s.size()-pos).c_str());
				varDec = new int[varNum+1];
				

				for (int i=1;i<=varNum;i++)
					varDec[i]=0;
				
				clauseVar = new int*[clauseNum];
				clauseVal = new int[clauseNum];
				clauseLength = new int[clauseNum];
				
				for (int i=0;i<clauseNum;i++)
				{
					clauseVar[i] = new int[MAX_CLAUSE_SIZE];
					clauseVal[i] = 0;
					clauseLength[i] = 0;
				}
			}
		}
		else if (state==1)
		{
			if (s.substr(0,1)=="%")
			{
				state=2;
			}
			else
			{
				int start=0;
				while (s.substr(start,1)==" ")
					start++;

				int lit = 1;
				int litNum = 0;
				int posNew = 0;
				int posOld = 0;
				while(lit != 0)
				{	
					posOld = posNew;
					while(s.substr(posOld,1)==" ")
						posOld++;
					
					posNew=s.find(" ",posOld+1);
					
					lit = atoi(s.substr(posOld,posNew-posOld).c_str());
					if(lit != 0)
					{
						clauseVar[currentClauseNum][litNum] = lit;
						litNum++;
					}
				}
				clauseLength[currentClauseNum] = litNum;
				currentClauseNum++;
			}
		}
	}
	fin.close();
}


bool generateSolution()	//recursive search function
{
	if (!updateClause())
		return false;

	//check success
	bool suc=true;
	for (int i=0;i<clauseNum;i++)
	{
		if (clauseVal[i]!=1)
		{
			suc=false;
			break;
		}
	}
	if (suc)
		return true;

	//unit propagation
	for (int i=0;i<clauseNum;i++)
	{
		if (decidedVar(i)==(clauseLength[i]-1) && clauseVal[i]==0)	//take care!!! clauseVal==0
		{
			int unit;
			for(int j=0; j<clauseLength[i]; j++)
			{
				if (varDec[abs(clauseVar[i][j])]==0)
					unit=j;
			}	

			if (clauseVar[i][unit]>0)
				varDec[clauseVar[i][unit]]=1;
			else
				varDec[-clauseVar[i][unit]]=-1;

			//no backtrack
			if (generateSolution())
				return true;
			
			varDec[abs(clauseVar[i][unit])]=0;
			return false;
		}
	}

	//heuristic: Simple one. Choose a positive variable in a non-Horn clause
	for (int i=0;i<clauseNum;i++)
	{
		int unit;
		if ((unit=hornHeuristic(i))>=0)
		{
			int dec;
			if (clauseVar[i][unit]>0)
			{
				varDec[clauseVar[i][unit]]=1;
				dec=1;
			}
			else
			{
				varDec[-clauseVar[i][unit]]=-1;
				dec=-1;
			}
			
			if (generateSolution())
			{
				return true;
			}
			else
			{
				varDec[abs(clauseVar[i][unit])]=-dec;
				if (generateSolution())
					return true;
				else
				{
					varDec[abs(clauseVar[i][unit])]=0;
					return false;
				}
			}
		}
	}

	return false;
}







int main(int argc, char** argv)	//argv[1] = data file. argv[2] = out file
{
	clock_t start,finish;
	start=clock();

	if (argc!=3)
	{
		cout<<"satSolver data_file output_file"<<endl;
		return 0;
	}
	// read from file
	readformula(argv[1]);
	
	//output
	ofstream out(argv[2]);
	
	//find solution
	if (generateSolution()==true)
	{
		for (int k=1;k<=varNum;k++)
		{
			if (varDec[k]>0)
				out<<k<<" 1"<<endl;
			else if (varDec[k]<0)
				out<<k<<" 0"<<endl;
			else
			{
				cout<<"wow!"<<endl;
				out<<"v"<<k<<"\t"<<"False"<<endl;
			}
		}
	}

	else
	{
		cout<<"Failed to Find a Satisfying Assignment"<<endl;
	}


	out.close();
	
	finish = clock();
	cout<<"Elasp time: "<<(double)(finish-start)/CLOCKS_PER_SEC<<" seconds"<<endl;
	
	return 0;
}