3-CNF

3-CNF(slightly improved?)

A. Second Edition

This is a mission impossible approach and I can guarantee you that it is impossible to find a fast algorithm for

solution of 3-CNF question. The previous one is just choose the symbol which has a maximum coverage of the working

set. This is greedy algorithm. This version, I developed an idea of "independent determine set" and "converge".

B.The problem

What is 3-CNF problem?

(A17||A18||~A2)&&(~A10||~A11||~A19)&&(~A4||A10||A16)&&(A3||~A12||A7)&&(A13||A15||A14)&&
(~A16||A14||A11)&&(A10||~A3||A6)&&(A14||~A11||A16)&&(~A8||~A9||A10)&&(A2||A8||~A6)&&
(A19||A4||A7)&&(A7||A14||A1)&&(~A13||A9||A7)&&(A1||A8||A11)&&(~A7||~A2||~A16)&&
(A11||A17||A0)&&(A5||A16||A13)&&(~A12||~A18||A2)&&(~A6||A12||A11)&&(A8||A6||A17)&&
(~A18||~A1||A13)&&(A5||~A14||A3)&&(A15||A19||A13)&&(~A17||~A19||A13)&&(A18||A15||A12)&&
(~A12||~A14||~A9)&&(~A19||A13||~A9)&&(~A10||~A13||A0)&&(~A1||A15||~A9)&&(~A2||~A15||A7)&&
(A2||~A5||~A8)&&(A11||~A14||A15)&&(~A9||A12||~A11)&&(~A16||~A4||~A15)&&(~A14||A12||~A19)&&
(~A2||~A15||~A1)&&(A14||A1||A19)&&(A13||A12||~A2)&&(A16||A15||A2)&&(A5||~A3||~A13)

Each group is consisted of three symbols with no same name and each symbol in each group can be in either true or false states. Groups are in "and" and symbols in each group are in "or". Can you find a way to satisfy the whole expression? Or in other words, can you assign true, false for each symbol such that the whole expression is true?
C.The idea of program

My way is nothing but a simple test by using bitmaps to ease the calculation of sets. My idea is very straight forward:

Suppose there exists a set of variables ( including the negative format of a symbol) such that if each of them is assigned true, then the whole expression is true. Then I call them a determine set. i.e. {A13,A7,A11,A2,~A9,~A3,~A4,~A10,A12,A14,A17,~A1,A5,~A16}

So, my task becomes to how to find this determine set. I use a simple recursive function call to find the result. Observe, if a is chosen, then we remove all groups which includes this variable.

This version, I developed an idea of "independent determine set" and "converge".

If we choose variable X and its complement ~X would be the set we are interested in since it is the only possible place that our choice affects the solution. Suppose we can be sure that the complement set of that variable can also be solved, we can proceed on. Here I developed an idea of "converge". That is, if the complement set is solvable, I call it converge. How do I define solvable? I remove the symbol index of that variable and reduce the environment set to complement set(???). And repeat above procedure until working set is empty which means solvable. Or in other case if symbol set is empty which means not solvable it is not solvable.

D.The major functions

Originally I have some idea of better way than this, but I forget about them after almost one week.

E.Further improvement

When I wasted a lot of my precious game-playing time, I think it over and try to figure out why I am doing this.

I began to realize that I was trying to convert 3-CNF back to some form of "implication, equivalent..." relations

and most probably this 3-CNF is just from that format. Then this is totally useless. My effort is futile.

F.File listing

1. set.h

2. set.cpp

3. 3cnf.h

4. 3cnf.cpp

5. main.cpp

file name: set.h

#ifndef SET_H
#define SET_H

#include <iostream>
#include <bitset>

using namespace std;


const int MaxAttrNumber=100;

class Set
{
	//this is a long-pain for me, I have no other way to 
	//let compiler recognize this "friend" function outside declaration
	friend ostream& operator<<(ostream& out, const Set& dummy)	
	{
		for (int i=0; i<dummy.size; i++)
		{
			if (dummy.theSet.test(i))
			{
				out<<'1';
			}
			else
			{
				out<<'0';
			}
		}
		return out;
	}
private:
	bitset<MaxAttrNumber> theSet;
	int size;
	int current;
public:
	void setSize(const Set& dummy);
	int getSize(){ return size;}
	int next(int current) const;
	int first() const;	
	int count() const;
	Set intersection(const Set& dummy) const;
	Set unionSet(const Set& dummy) const;
	Set difference(const Set& dummy) const;
	bool isEmpty();
	//I am crazy about operator overloading!!!:)
	Set operator-(const Set& dummy) const;
	Set operator+(const Set& dummy) const;
	Set operator*(const Set& dummy) const;
	void operator=(const Set& dummy);
	bool operator==(const Set& dummy) const;
	bool operator!=(const Set& dummy) const;
	bool operator>(const Set& dummy) const;
	bool operator>=(const Set& dummy) const;
	bool operator<(const Set& dummy) const;
	bool operator<=(const Set& dummy) const;
	void set(int pos);
	void forEachSubSet(Set& dummy) const;//must be called before "eachSub()"
	bool eachSub(Set& dummy) const;
	bool eachSub(Set& dummy, const Set& excluding) const;
	void set();
	void reset(int pos);
	void reset();
	bool test(int pos) const;
	bool isIn(const Set& dummy) const;
	void setSize(int theSize) {size=theSize;}
	Set(int theSize=10);
	void print();
};

#endif

file name: set.cpp

#include "Set.h"

void Set::print()
{
	char str[MaxAttrNumber+1];
	strcpy(str, (theSet.to_string()).c_str()+MaxAttrNumber-size);
	printf("%s", str);
}

bool Set::isEmpty()
{
	for (int i=0; i<size; i++)
	{
		if (theSet.test(i))
		{
			return false;
		}
	}
	return true;
}

bool Set::isIn(const Set& dummy) const
{
	for (int i=0; i<size; i++)
	{
		if (theSet.test(i))
		{
			if (!dummy.test(i))//here I use Set.test() instead of set.test()
			{
				return false;
			}
		}
	}
	return true;		
}

bool Set::test(int pos) const
{
	return (pos<size&&theSet.test(pos));
}

//current=-1;//initialize to -1 to prepare for being called
int Set::next(int current) const
{
	for (int i=current+1; i<size; i++)//include situation current>=size
	{
		if (theSet.test(i))
		{
			return i;
		}
	}
	return -1;//not found
}

bool Set::operator !=(const Set& dummy)const
{
	return !(this->operator ==(dummy));
}

bool Set::operator <(const Set& dummy)const
{
	return (this->isIn(dummy)&&this->operator !=(dummy));
}

bool Set::operator <=(const Set& dummy)const
{
	return isIn(dummy);
}

bool Set::operator >(const Set& dummy)const
{
	return !(this->operator <=(dummy));
}

bool Set::operator >=(const Set& dummy)const
{
	return !(this->operator <(dummy));
}

bool Set::operator ==(const Set& dummy)const
{
	for (int i=0; i<(size>dummy.size?size:dummy.size); i++)
	{
		if (test(i)^dummy.test(i))
		{
			return false;
		}
	}
	return true;
}

void Set::setSize(const Set& dummy)
{
	size=dummy.size;
}

void Set::operator =(const Set& dummy)
{
	size=dummy.size;
	for (int i=0; i<size; i++)
	{
		if (dummy.test(i))
		{
			theSet.set(i);
		}
		else
		{
			theSet.reset(i);
		}
	}
}


Set::Set(int theSize)
{
	size=theSize;
	reset();
}

void Set::reset()
{
	for (int i=0; i<size; i++)
	{
		theSet.reset(i);
	}
}

void Set::reset(int pos)
{
	if (pos<size)
	{
		theSet.reset(pos);
	}
}

void Set::set()
{
	theSet.set();
}

void Set::set(int pos)
{
	theSet.set(pos);
}
	
void Set::forEachSubSet(Set& dummy) const
{
	dummy.size=size;
	dummy.reset();//emptyset
}

bool Set::eachSub(Set& dummy, const Set& excluding) const
{
	int index=first();//starting from very first

	while (index!=-1)//not exceeding boundery
	{
		if (!excluding.test(index))//exluding this set
		{
			if (dummy.test(index))
			{
				dummy.reset(index);				
			}
			else
			{
				dummy.set(index);
				//return true;
							
				if (dummy<*this)//only return the proper subset
				{
					return true;
				}			
			}
		}
		index=next(index);

	}
	return false;
}


bool Set::eachSub(Set& dummy) const
{
	int index=first();//starting from very first

	while (index!=-1)//not exceeding boundery
	{
		if (dummy.test(index))
		{
			dummy.reset(index);
			index=next(index);
		}
		else
		{
			dummy.set(index);
			//return true;
						
			if (dummy<*this)
			{
				return true;
			}			
		}
	}
	return false;
}

int Set::first()const
{
	return next(-1);
}

int Set::count()const
{
	return theSet.count();
}

Set Set::unionSet(const Set& dummy) const
{
	Set result;
	result.size=size>dummy.size?size:dummy.size;
	for (int i=0; i<result.size; i++)
	{
		if (test(i)||dummy.test(i))
		{
			result.set(i);
		}
	}
	return result;//this is a temparory object;
}

Set Set::difference(const Set& dummy) const
{
	Set result;
	result.size=size>dummy.size?size:dummy.size;
	for (int i=0; i<result.size; i++)
	{
		if (test(i)&&!dummy.test(i))
		{
			result.set(i);
		}
	}
	return result;
}

Set Set::operator +(const Set& dummy) const
{
	return unionSet(dummy);
}

Set Set::operator -(const Set& dummy) const
{
	return difference(dummy);
}

Set Set::intersection(const Set& dummy) const
{
	Set result;
	result.size=size<dummy.size?size:dummy.size;
	for (int i=0; i<result.size; i++)
	{
		if (test(i)&&dummy.test(i))
		{
			result.set(i);
		}
	}
	return result;
}

Set Set::operator *(const Set& dummy) const
{
	return intersection(dummy);
}

file name: 3cnf.h

#include "set.h"


const int MaxSymbolCount=50;
const int MaxExprCount=MaxSymbolCount*8;

class CNF
{
private:
	char* symbols[MaxSymbolCount];
	int expr[MaxExprCount][3];//expression
	Set cnf_pos[MaxSymbolCount];//positive set of simbol
	Set cnf_neg[MaxSymbolCount];//neg all starts from 1
	int symbolCount;//
	int exprCount;
	int chooseSymbol(Set& symbolSet, Set& exprSet);
	int chooseMaxCover(Set& symbolSet, Set& exprSet);
	int chooseComplement(Set& symbolSet, Set& exprSet);
	bool solve(Set& symbolSet, Set& exprSet, int resultSet[]=NULL, int* count=NULL);
	bool converge(Set& symbolSet, Set& environSet, Set& workingSet);
public:
	void randomGenerate(int symCount, int expCount);
	void printSymbol(int index);
	void displayExpr();
	bool satisfy(int resultSet[], int* count, int option);
};

	

		
file name: 3cnf.cpp

#include "3CNF.H"
#include <stdlib.h>
#include <string.h>

int optionIndex;

void CNF::randomGenerate(int symCount, int expCount)
{	
	symbolCount=symCount;
	exprCount=expCount;
	for (int i=0; i<symbolCount; i++)
	{
		symbols[i]=new char[4];
		sprintf(symbols[i], "A%d", i);
		cnf_pos[i].setSize(exprCount);
		cnf_neg[i].setSize(exprCount);
	}	
	for (i=0; i<exprCount; i++)
	{
		for (int j=0; j<3; j++)
		{
			//must check if there is repeat, otherwise never satisfy
			//i.e. ~A&&A ==false
			while (true)
			{
				expr[i][j]=rand()%symbolCount;
				if (j==0)
				{
					break;
				}
				if (j==1)
				{
					if (expr[i][j]!=expr[i][j-1]&&expr[i][j]!=-expr[i][j-1])
					{
						break;
					}
				}
				if (j==2)
				{
					if (expr[i][j]!=expr[i][j-1]&&expr[i][j]!=-expr[i][j-1]
						&&expr[i][j]!=expr[i][j-2]&&expr[i][j]!=-expr[i][j-2])
					{
						break;
					}
				}
			}
			if (rand()%2==0)
			{
				cnf_pos[expr[i][j]].set(i);
			}
			else
			{
				cnf_neg[expr[i][j]].set(i);
				expr[i][j]*=-1;
			}
		}
	}

}
	
void CNF::displayExpr()
{
	printf("print the 3CNF format:\n");
	for (int i=0; i<exprCount; i++)
	{
		if (i%5==0)
		{
			printf("\n");
		}
		printf("(");
		for (int j=0; j<3; j++)
		{
			if (expr[i][j]<0)
			{
				printf("~%s", symbols[-expr[i][j]]);
			}
			else
			{
				printf("%s", symbols[expr[i][j]]);
			}
			if (j!=2)
			{
				printf("||");
			}
		}		
		printf(")");
		
		if (i!=exprCount-1)
		{
			printf("&&");
		}

	}
	printf("\n");
}
		
bool CNF::satisfy(int resultSet[], int* count, int option)
{
	Set symbolSet, exprSet;
	symbolSet.setSize(symbolCount);
	exprSet.setSize(exprCount);	
	symbolSet.set();
	exprSet.set();
	//symbolSet.print();
	optionIndex=option;
	return solve(symbolSet, exprSet, resultSet, count);
}


bool CNF::solve(Set& symbolSet, Set& exprSet, int resultSet[], int* count)
{
	int index;
	//printf("no.%d call of solve: \n", count);
	//printf("symbolSet=");
	//symbolSet.print();
	//printf("exprSet=");
	//exprSet.print();
	//printf("\n");
	if (exprSet.isEmpty())
	{
		return true;
	}
	if (symbolSet.isEmpty())
	{
		return false;
	}

	//index must return absolue value bigger than 1
	//so that allow -1,1
	index=chooseSymbol(symbolSet, exprSet);
	//printf("\nand choose index of %d\n", index);
	//0 means the symbol set cannot cover expression set
	if (index==0)
	{
		return false;
	}
	if (resultSet!=NULL&&count!=NULL)
	{
		resultSet[*count]=index;
		(*count)++;
	}
	if (index<0)
	{
		index*=-1;
		index-=1;
		exprSet=exprSet-cnf_neg[index];
	}
	else
	{
		index-=1;
		exprSet=exprSet-cnf_pos[index];
	}
	//printf("and expr is\n");
	//exprSet.print();
	//in any case, we reduce the symbol set
	symbolSet.reset(index);
	return solve(symbolSet, exprSet, resultSet, count);
}

bool CNF::converge(Set& symbolSet, Set& environSet, Set& workingSet)
{
	int index;
	
	if (workingSet.isEmpty())
	{
		return true;
	}
	//here it implied workingset is NOT empty
	if (symbolSet.isEmpty())
	{
		return false;
	}
	//a simple 
	index=chooseMaxCover(symbolSet, workingSet);
	if (index==0)
	{
		return false;
	}

	if (index<0)
	{
		index=-index-1;
		
		workingSet=workingSet-cnf_neg[index];//reduced working set
		//* means intersection, + is union
		workingSet=workingSet+(environSet*cnf_pos[index]);
	}
	else
	{
		
		index-=1;
		
		workingSet=workingSet-cnf_pos[index];
		workingSet=workingSet+(environSet*cnf_neg[index]);
	}
	symbolSet.reset(index);
	
	return converge(symbolSet, environSet, workingSet);
}


int CNF::chooseMaxCover(Set& symbolSet, Set& exprSet)
{
	int count=exprCount, result, index=0;
	Set temp;
	//printf("symbol set is\n");
	//symbolSet.print();
	for (int i=0; i<symbolCount; i++)
	{
		if (symbolSet.test(i))
		{
			result=(exprSet-cnf_pos[i]).count();
			if (result<count)
			{
				count=result;
				index=i+1;
			}
			result=(exprSet-cnf_neg[i]).count();
			if (result<count)
			{
				count=result;
				index=(i+1)*(-1);
			}
		}
	}
	return index;
}

int CNF::chooseComplement(Set& symbolSet, Set& exprSet)
{
	int index;
	Set workingSet, curSymbolSet;
	index=symbolSet.first();
	while (index!=-1)
	{
		//try positive first
		workingSet=cnf_neg[index] - exprSet;
		curSymbolSet=symbolSet;
		curSymbolSet.reset(index);
		if (converge(curSymbolSet, exprSet, workingSet))
		{	
			return index+1;
		}
		//try negative secondly
		workingSet=cnf_pos[index]-exprSet;
		curSymbolSet=symbolSet;
		curSymbolSet.reset(index);
		if (converge(curSymbolSet, exprSet, workingSet))
		{			
			return (index+1)*(-1);
		}	
		
		index=symbolSet.next(index);
	}
	if (index==-1)
	{
		return 0;//cannot find
	}
}




//if no max symbol can be found, index is 0
int CNF::chooseSymbol(Set& symbolSet, Set& exprSet)
{
	if (optionIndex==0)
	{
		return chooseMaxCover(symbolSet, exprSet);		
	}
	else
	{
		return chooseComplement(symbolSet, exprSet);
	}
	
}
	

void CNF::printSymbol(int index)
{
	printf("%s", symbols[index]);
}

file name: main.cpp

#include "3cnf.h"
#include <time.h>

int main()
{
	CNF cnf;
	int count=0;
	int resultSet[MaxSymbolCount]={0};
	srand(time(0));
	cnf.randomGenerate(10, 20);
	cnf.displayExpr();
	if (cnf.satisfy(resultSet, &count, 0))
	{
		printf("\nchooseMaxCover works and it is satisfiable\n");
		for (int i=0; i<count; i++)
		{
			if (resultSet[i]<0)
			{
				printf("~");
				cnf.printSymbol(resultSet[i]*(-1)-1);
			}
			else
			{
				cnf.printSymbol(resultSet[i]-1);
			}
			printf(",");
		}				
	}
	else
	{
		printf("\nchooseMaxCover unsatisfiable\n");
	}
	printf("\n");
	count=0;
	if (cnf.satisfy(resultSet, &count, 0))
	{
		printf("\nchooseComplement works and it is satisfiable\n");
		for (int i=0; i<count; i++)
		{
			if (resultSet[i]<0)
			{
				printf("~");
				cnf.printSymbol(resultSet[i]*(-1)-1);
			}
			else
			{
				cnf.printSymbol(resultSet[i]-1);
			}
			printf(",");
		}				
	}
	else
	{
		printf("\nchooseComplement unsatisfiable\n");
	}
	printf("\n");
	return 0;
}

How to run? The result is not very interesting. First I am not sure if the "unsatisfied" message really means

there is no solution. This is completely beyond my knowledge.

print the 3CNF format:

(A1||~A14||~A10)&&(~A20||~A15||A10)&&(A6||~A26||~A8)&&(~A12||~A6||~A19)&&(A0||~A19||~A22)&&
(~A28||~A12||A4)&&(~A12||A17||A15)&&(A20||A17||A14)&&(A20||~A7||~A3)&&(A6||A12||~A11)&&
(A27||~A13||~A23)&&(~A26||~A20||A24)&&(~A20||~A22||A16)&&(A1||A12||A15)&&(A28||A23||~A6)&&
(~A20||A0||~A7)&&(~A21||~A2||~A10)&&(A14||~A4||~A27)&&(A14||A24||A0)&&(A3||A19||A0)&&
(~A16||A19||~A11)&&(A27||~A5||A4)&&(A23||A29||~A15)&&(~A12||~A7||A26)&&(~A21||A29||~A9)&&
(~A15||~A26||~A16)&&(~A18||A12||A19)&&(A10||~A29||~A28)&&(~A28||A17||A14)&&(~A23||~A3||~A15)&&
(~A8||A7||A0)&&(A17||~A20||~A15)&&(~A14||A2||~A16)&&(A4||A5||A20)&&(~A23||~A9||~A5)&&
(A9||A11||~A2)&&(A18||~A23||~A22)&&(A27||A11||~A15)&&(~A5||~A9||A1)&&(~A3||A20||~A29)&&
(A27||A6||~A9)&&(A10||A12||A17)&&(~A16||~A2||~A25)&&(A3||A4||A12)&&(~A1||~A6||~A8)&&
(~A5||~A11||A3)&&(~A22||A0||A25)&&(A25||~A29||~A10)&&(A12||A5||A29)&&(~A28||A8||~A20)

chooseMaxCover works and it is satisfiable
A12,~A15,~A0,~A5,A20,~A28,~A2,~A6,~A22,~A8,~A9,~A10,~A16,~A4,~A7,~A13,A17,A24,

chooseComplement works and it is satisfiable
A12,~A15,~A0,~A5,A20,~A28,~A2,~A6,~A22,~A8,~A9,~A10,~A16,~A4,~A7,~A13,A17,A24,
Press any key to continue