Problem about Davis Putman algorithm

Question

nndung179 0 Light Poster

12 Years Ago

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

c++

This attachment is potentially unsafe to open. It may be an executable that is capable of making changes to your file system, or it may require specific software to open. Use caution and only open this attachment if you are comfortable working with zip files.

DavisPutman.zip (14.28 KB)

3 Contributors
2 Replies
121 Views
1 Day Discussion Span
Latest Post 12 Years Ago Latest Post by MonsieurPointer

All 2 Replies

raptr_dflo 48 Posting Pro

12 Years Ago

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.

Reply to this topic

Be a part of the DaniWeb community

We're a friendly, industry-focused community of developers, IT pros, digital marketers, and technology enthusiasts meeting, networking, learning, and sharing knowledge.

MonsieurPointer · Answer 1 · 2011-11-07T19:58:31+00:00

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!

Problem about Davis Putman algorithm

Recommended Answers Collapse Answers

All 2 Replies

Recommended Answers