Problem about Davis Putman algorithm

[nndung179]

INPUT.txt

6
p q r s k m
6
~p|q
~q|r
~p|~r|s
~r|k
~k|m
r
m

right OUTPUT.txt

~p|q,~q|r,~p|~r|s,~r|k,~k|m,r,~m
p:
Resolve unsuccessfully
q:
~p|~r|s,~r|k,~k|m,r,~m,~p|r
r:
~k|m,~m,~p|s,k,~p|k
s:
Resolve unsuccessfully
k:
~m,~p|s,m,~p|m
m:
~p|s,0,~p
TRUE

My Program

include "stdafx.h"

include <string>

include <fstream>

include <vector>

include <iostream>

using namespace std;

typedef struct
{
char var;
int neg;
}Literal;

typedef struct
{
vector<Literal> arrList;

}Clause;

Clause parseClause(char *strClause)
{
Clause c;
Literal l;
char *kq;
//
//
//
kq = strtok(strClause, "|");
while(kq != NULL)
{
if(kq[0] == '~')
{
l.neg = 1;
l.var = kq[1];
}
else
{
l.neg = 0;
l.var = kq[0];
}
c.arrList.push_back(l);
kq = strtok(NULL, "|");
}
return c;
}
void fprintSentence(ofstream &f, vector<Clause> clauseArr)
{

for (int i = 0; i < clauseArr.size(); i++)
{
        if(clauseArr[i].arrList.size() == 0)
        {
            cout << "0";
        }
    for(int j = 0; j < clauseArr[i].arrList.size(); j++)
    {
        if (clauseArr[i].arrList[j].neg == 1)
        {
            if (j != clauseArr[i].arrList.size() - 1)
            {
                f << "~" << clauseArr[i].arrList[j].var << "|";
            }
            else
            {
                f << "~" << clauseArr[i].arrList[j].var;
            }
        }
        else
        {
            if (j != clauseArr[i].arrList.size() - 1)
            {
                f << clauseArr[i].arrList[j].var << "|";
            }
            else
            {
                f << clauseArr[i].arrList[j].var;
            }
        }
    }
    if(i != clauseArr.size() - 1)
    {
        f << ",";
    }
}

}

void printSentence(vector<Clause> clauseArr)
{
for (int i = 0; i < clauseArr.size(); i++)
{
if(clauseArr[i].arrList.size() == 0)
{
cout << "0";
}
for(int j = 0; j < clauseArr[i].arrList.size(); j++)
{
if (clauseArr[i].arrList[j].neg == 1)
{
if (j != clauseArr[i].arrList.size() - 1)
{
cout << "~" << clauseArr[i].arrList[j].var << "|";
}
else
{
cout << "~" << clauseArr[i].arrList[j].var;
}
}
else
{
if (j != clauseArr[i].arrList.size() - 1)
{
cout << clauseArr[i].arrList[j].var << "|";
}
else
{
cout << clauseArr[i].arrList[j].var;
}
}
}
if(i != clauseArr.size() - 1)
{
cout << ",";
}

}

}

bool Contain(Clause c, int neg, char var)
{
for(int i = 0; i < c.arrList.size(); i++)
{
if(c.arrList[i].neg == neg && c.arrList[i].var == var)
{
return true;
}
}
return false;
}

bool isEqual(Clause cl1, Clause cl2)
{
for (int i = 0; i < cl1.arrList.size(); i++)
{
if(Contain(cl2, cl1.arrList[i].neg, cl1.arrList[i].var) == false)
{
return false;
}
}
for (int j = 0; j < cl2.arrList.size(); j++)
{
if(Contain(cl1, cl2.arrList[j].neg, cl2.arrList[j].var) == false)
{
return false;
}
}
return true;
}

bool containClause(vector<Clause> arrClause, Clause c)
{
for(int i = 0; i < arrClause.size(); i++)
{
if(isEqual(c, arrClause[i]))
return true;
}
return false;
}

vector<Clause> findLiteral(vector<Clause> clauseArr, int neg, char var)
{
vector<Clause> clauseArr1;

for(int i = 0; i < clauseArr.size(); i++)
{
    if(Contain(clauseArr[i], neg, var) == true)
    {
        clauseArr1.push_back(clauseArr[i]);
    }
}
return clauseArr1;

}

Clause Resolve(Clause cl1, Clause cl2)
{
Clause c;
for(int i = 0; i < cl1.arrList.size(); i++)
{
c.arrList.push_back(cl1.arrList[i]);
}

for(int j = 0; j < cl2.arrList.size(); j++)
{
    c.arrList.push_back(cl2.arrList[j]);
}

for(int i = 0; i < c.arrList.size();)
{
    Literal temp = c.arrList[i];
    if(Contain(c, !temp.neg, temp.var))
    {
        for(int j = c.arrList.size() - 1; j >= i; j--)
        {
            if(c.arrList[j].var == temp.var)
            {
                c.arrList.erase(c.arrList.begin() + j);
            }
        }
    }
    else
        i++;
}

for(int i = 0; i < c.arrList.size();)
{
    Literal temp = c.arrList[i];
    if(Contain(c, temp.neg, temp.var))
    {
        for(int j = c.arrList.size() - 1; j > i; j--)
        {
            if(c.arrList[j].var == temp.var)
            {
                c.arrList.erase(c.arrList.begin() + j);
            }
        }
    }
    i++;
}
return c;

}

vector<Clause> RemoveClause(vector<Clause> clauseArr, char var)
{
vector<Clause> clauseArr1;
bool flag = false;
for (int i = 0; i < clauseArr.size(); i++)
{
flag = false;
for(int j = 0; j < clauseArr[i].arrList.size(); j++)
{
if(clauseArr[i].arrList[j].var == var)
flag = true;
}
if(flag == false) {
clauseArr1.push_back(clauseArr[i]);
}
}
return clauseArr1;
}

void main()
{
Clause c;
Clause conclusion;
Literal l;
vector<Clause> cl ;
string line;
int dem;
int dem1;
char arrChar;
bool check = false;
// Doc file
ifstream file;
file.open("Release/INPUT.txt"); // Mo file Input
// Ghi file
ofstream f;
f.open("Release/OUTPUT.txt");
//
//
//
if(file.is_open())
{
char *ch;
//
// Read file: 2 line
//
file >> dem1;
cout << dem1 << endl;
//
ch = (char)line.c_str();
arrChar = new char[dem1];
for(int i = 0; i < dem1; i++)
{
file >> ch;
cout << ch << " ";
arrChar[i] = ch[0];
}
//
// Read file: next 7 line
//
cout << endl;
file >> dem;
cout << dem << endl;
for(int i = 0; i < dem; i++)
{
file >> ch;
cout << ch << " " << endl;
c = parseClause(ch);
cl.push_back(c);
}
//
// Read file: last line
//
file >> ch;
cout << ch << endl;
if(ch[0] == '~')
{
l.neg = 1;
l.var = ch[1];
}
else
{
l.var = ch[0];
}
conclusion.arrList.push_back(l);
conclusion.arrList[0].neg = !conclusion.arrList[0].neg;

    cl.push_back(conclusion);
    //
    //
    //
    printSentence(cl);
    fprintSentence(f, cl);
}
else
{
    cout << "Unable to open file" << endl;
}
cout << endl << endl;

vector<Clause> newSentence = cl;
fprintSentence(f, cl);
vector<Clause> c1, c2;
Clause kq;


for(int i = 0; i < dem1; i++)
{
    cout << endl << arrChar[i] << ": " << endl;
    f << endl << arrChar[i] << ": " << endl;
    c1 = findLiteral(newSentence, 0 ,arrChar[i]);
    c2 = findLiteral(newSentence, 1 ,arrChar[i]);
    if(c1.size() > 0 && c2.size() > 0)
    {
        newSentence = RemoveClause(newSentence, arrChar[i]);
        for(int j = 0; j < c1.size(); j++)
        {
            for(int k = 0; k < c2.size(); k++)
            {
                kq = Resolve(c1[j], c2[k]);
                if(kq.arrList.size() == 0)
                {
                    printSentence(newSentence);
                    fprintSentence(f, newSentence);
                    cout << "TRUE" << endl;
                    f << "TRUE" << endl;
                    return;
                }
                else
                {
                    if(!containClause(newSentence, kq))
                    {
                        newSentence.push_back(kq); 
                    }
                }
            }
        }
        printSentence(newSentence);
        fprintSentence(f, newSentence);
    }
    else
    {
        cout << "Resolve unsuccessfully" << endl;
        f << "Resolve unsuccessfully" << endl;
    }
}
f.close();

}

My wrong OUTPUT.txt

~p|q,~q|r,~p|~r|s,~r|k,~k|m,r,m~p|q,~q|r,~p|~r|s,~r|k,~k|m,r,m
p:
Resolve unsuccessfully

q:
~p|~r|s,~r|k,~k|m,r,m,~p|r
r:
~k|m,m,~p|s,k,~p|k
s:
Resolve unsuccessfully

k:
m,~p|s,~p|m
m:
Resolve unsuccessfully

I want to it give me the right OUTPUT. But something went wrong on my program and I don't know how to fix that. Please help !!!

Thank you so much !!!Source Code

DavisPutman.zip

[raptr_dflo]

For one thing, if printSentence() and fprintSentence() are identical except for whether you pass in and use an ofstream&, or just use cout ... then why not just do:

void printSentence(vector<Clause> clauseArr)
{
    fprintSentence(cout, clauseArr);
}

Then, is it obvious to you that your first incorrect output line looks very much like the correct first output line, except duplicated? Among other things, this should indicate to you that your fprintSentence() function should probably output endl at the end of the loop.

Then look at what's different in your literal-parsing code between lines 33-43 and lines 309-318. Maybe you should move the correct code into a parseLiteral() function that you can call from each place?

Once you have the correct set of initial clauses, we can see what needs to be fixed next.

[MonsieurPointer]

This is a double post. Just because someone didn't fix your code, it still doesn't give you the right to re-post the same question!