3-CNF
A. First 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.
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 programMy 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.
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
กก
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=50;
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);
bool solve(Set& symbolSet, Set& exprSet, int resultSet[], int& count);
public:
void randomGenerate(int symCount, int expCount);
void printSymbol(int index);
void displayExpr();
bool satisfy(int resultSet[], int& count);
};
กก
file name: 3cnf.cpp
#include "3CNF.H"
#include <stdlib.h>
#include <string.h>
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)
{
Set symbolSet, exprSet;
symbolSet.setSize(symbolCount);
exprSet.setSize(exprCount);
symbolSet.set();
exprSet.set();
//symbolSet.print();
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;
}
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);
}
//if no max symbol can be found, index is 0
int CNF::chooseSymbol(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;
}
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(20, 40);
cnf.displayExpr();
if (cnf.satisfy(resultSet, count))
{
printf("\nit 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("unsatisfiable\n");
}
printf("\n");
return 0;
}
How to run?
print the 3CNF format:
(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)
it is satisfiable
A13,A7,A11,A2,~A9,~A3,~A4,~A10,A12,A14,A17,~A1,A5,~A16,
Press any key to continue
กก