Geeks To Go is a helpful hub, where thousands of volunteer geeks quickly serve friendly answers and support. Check out the forums and get free advice from the experts. Register now to gain access to all of our features, it's FREE and only takes one minute. Once registered and logged in, you will be able to create topics, post replies to existing threads, give reputation to your fellow members, get your own private messenger, post status updates, manage your profile and so much more.

Create Account How it Works

# SAT c++

### #1 Javier Posted 23 May 2005 - 02:30 PM

Javier

New Member

• Member
• 8 posts
Im a beginner trying to write a SAT program but get a segmentation fault error.
I cant figure out what the problem is. Its almost like a character vs. a string problem.
can anyone help. here is the code. sorry about the couts i ws truoble shooting. Input file should look something li this: x y z \$ x !y p \$ z y z \$\$. Where the formula is in Conjunctive normal form, \$ seperates clauses and \$\$ indicates end of formula. So the above input would really be: ((x OR y OR z)AND (x OR NOTy OR p)AND (z OR y OR z)). If anyone can help that would be great!.

#include <iostream>
#include <vector>
#include <string>
#include <cctype>

using namespace std;

class atom
{
public:
string variable;
bool form;
atom();
atom (string,bool);
bool operator == (atom);
};

class clause
{
vector<atom> atoms;
public:
bool contains(atom);
void insert(atom);
void remove(atom);
bool empty();
};

class formula
{
vector<clause> clauses;
vector<string> variables;
vector<atom> values;
public:
void remove(atom);
bool satisfiable();
void pure();
formula();
formula(formula & f, atom a);
};

int main() //do i need Bool since it is returning true or false??
{
cout << "entering main" << endl;
formula f; // declare a formula variable

if(f.satisfiable())
{
cout <<"marker 200"<< endl;
return true;
}
else
{
cout << "exiting main" << endl;
return false;
}
}
atom:: atom (string s, bool b)
{
cout << "entering atom:: atom" << endl;

variable = s;
form = b;
cout << "exiting atom:: atom" << endl;
}

atom:: atom()
{
cout<< "entering /exiting atom::atom()" <<endl;
}

bool atom:: operator==(atom a)
{
cout << "entering atom:: operator" << endl;
if(a.variable == variable && a.form == form)
return true;

cout << "exiting atom:: operator" << endl;
return false;
}

bool clause:: contains(atom a)
{
cout << "entering clause :: contains" << endl;
for(int i=0;i < atoms.size(); ++i)
if(atoms[i]==a)
{
cout <<" in clause:: contains"<< endl;
return true;
}
{
cout << "exiting clause :: contains" << endl;
return false;
}
}

void clause:: insert(atom a)
{
cout <<"entering clause:: insert" << endl;
atoms.push_back(a);
cout <<"exiting clause:: insert" << endl;
}

void clause:: remove(atom a)
{
cout <<"entering clause:: remove" << endl;
for(vector<atom>::iterator i = atoms.begin(); i != atoms.end(); ++i)
if(*i == a)
atoms.erase(i);
cout <<"exiting clause:: remove" << endl;
}

bool clause:: empty()
{
cout<< "entering clause:: empty"<< endl;

cout <<"exiting clause:: empty"<< endl;
return atoms.empty();
}
void formula:: remove(atom a)
{
cout << "entering formula:: remove" << endl;
for(int i=clauses.size()-1;i>=0;i--)
if(clauses[i].contains(a))
clauses.erase(clauses.begin()+i);
a.form=!a.form;
for(int i=0;i<clauses.size();i++)
if(clauses[i].contains(a))
clauses[i].remove(a);
cout << "exiting formula:: remove" << endl;
}

formula:: formula()
{
cout << "entering formula()" << endl;
string s("");
clause* c=new clause();

for(int i = 0;s != string("\$\$"); ++i)
{

cin >> s; // reads a string

{
if(s == string("\$\$"))

{
cout<< "if \$\$" << endl;
return;
}
if(s == string("\$"))
{
clauses.push_back(*c); // stores clause in
c=new clause();
cout<< "if \$" << endl;
}
if(s[0]=='!')// creates an atom
{
s.erase(s.begin());

cout<< "if!" << endl;
c->insert(atom(s,false));

}
else
{
c->insert(atom(s,true)); //stores atom in clause c.
cout << "exiting formula()" << endl;
}
}
}
}

formula:: formula(formula &f, atom a)
{
cout << "entering formula:: formula" << endl;
clauses = f.clauses;
variables = f.variables;
values = f.values;

remove(a);
cout << "exiting formula:: formula" << endl;
}

void formula:: pure()
{
cout << "entering formula:: pure" << endl;
for(vector<string>::iterator i = variables.begin();i != variables.end();++i)
{
atom w1(*i,true);
atom w2(*i,false);
atom t;
bool pf=false, nf=false;
for(vector<clause>::iterator j = clauses.begin();j != clauses.end();++j)
{
if((*j).contains(w1))
pf = true;
if((*j).contains(w2))
nf = true;
t = (pf ?w1:w2);// whqat does this do agian?
}
if(!(pf && nf))
{
for(vector<clause>::iterator j = clauses.begin();j != clauses.end();++j)

if((*j).contains(t) )
clauses.erase(j);
}
}
cout << "exiting formula :: pure" << endl;
}

bool formula::satisfiable()
{

cout << "entering formula::satisfiable" << endl;
// call pure, declare 2 variables F1, F2.
// check if its empty.
// create formula F1 and F2
// If either F1 or F2 is satisfiable, return True

pure();
if(clauses.empty())
return true;
cout<< "marker0"<< endl;

//CAN YOU CHEK HERE!!!!!!!!!!
for(vector<clause>::iterator i= clauses.begin(); i != clauses.end();++i)

if((*i).empty())

{
cout << "marker1"<< endl;
return false;
}
//cout << "marker2" << endl;
atom p(variables[0],true);
//cout << "100" <<endl;
atom q(variables[0],false);
//cout << "101" << endl;
variables.erase(variables.begin());
//cout << "102" << endl;
formula F1(*this,p);
//cout << "103" << endl;
formula F2(*this,q);

if(F1.satisfiable())
{
cout<< "105" << endl;
return true;
}
if(F2.satisfiable())
{
cout << "106" << endl;
return true;
}
else
{
cout << "exiting formula :: satisfiable" << endl;
return false;
}
}
• 0

### #2 Javier Posted 23 May 2005 - 02:37 PM

Javier

New Member

• Topic Starter
• Member
• 8 posts
• 0

### #3 bdlt Posted 23 May 2005 - 03:43 PM

bdlt

Member

• Member
• 876 posts
there may not be any memory allocated for 's' near line 140.
string s("");

the following runs better, allowing for a 20 character string:
string s("12345678901234567890");
• 0

### #4 Javier Posted 23 May 2005 - 03:57 PM

Javier

New Member

• Topic Starter
• Member
• 8 posts
I tried that s("12345678901234567890"). It didt work. It gets as far as "marker 0".
Do you see anything wrong between "marker 0" and "marker 1"? lines 237 - 247.
• 0

### #5 bdlt Posted 23 May 2005 - 05:52 PM

bdlt

Member

• Member
• 876 posts
it looks like variables[0] is null here:
atom p(variables[0],true);

the program fails before "marker 2" has had enough time to display

to help debug you can use getch() to halt the program:
cout << "marker2" << endl;
getch();

how does adding getch() help? - it allows the 'cout' to execute while waiting for a keystroke

your challenge is to find out what is wrong with variables[0] .
• 0

### #6 Javier Posted 23 May 2005 - 09:39 PM

Javier

New Member

• Topic Starter
• Member
• 8 posts
bdlt,
Input file should look something li this: x y z \$ x !y p \$ z y z \$\$. Where the formula is in Conjunctive normal form, \$ seperates clauses and \$\$ indicates end of formula. So the above input would really be: ((x OR y OR z)AND (x OR NOTy OR p)AND (z OR y OR z)).

so an example of a string is x, !y, etc..
I agree variables[0] seems to be null. I dont know why though.
• 0

### #7 Javier Posted 23 May 2005 - 09:45 PM

Javier

New Member

• Topic Starter
• Member
• 8 posts
getch() doesnt work, it doesnt even compile when i add getch().
• 0

### #8 bdlt Posted 23 May 2005 - 11:33 PM

bdlt

Member

• Member
• 876 posts
you need to add the following to use getch()

#include <conio.h>
• 0

### #9 bdlt Posted 26 May 2005 - 01:37 PM

bdlt

Member

• Member
• 876 posts
Javier,
I've taken a second look at 'your' code(I'm assuming you did not write this). I will be happy to help you with this, but will not write the code for you.

Your previous 'assignment' was to evaluate variables[0]. If you can't see why this is null, then this code may be beyond your knowledge at this time.

The code up to the variables[0] line seems to be well written. If this were my code, I would remove the few lines of code from the variables[0] line to the end of the file. Then add a loop which iterates through clauses, extract the logic value of each atom in each clause, then apply the logic values to a formula.

Can you see why variables[0] is null?
• 0

### #10 Javier Posted 26 May 2005 - 04:40 PM

Javier

New Member

• Topic Starter
• Member
• 8 posts
bdlt,
Hey thanks for looking at this again.
I would be happy with understanding variables[0] is null and why this doesnt work.
• 0

### #11 bdlt Posted 26 May 2005 - 04:49 PM

bdlt

Member

• Member
• 876 posts
if you look at the code, varaiables is declared, but no values are ever inserted into variables. when it tries to use variables[0], it crashes.
• 0

### Similar Topics

#### 0 user(s) are reading this topic

0 members, 0 guests, 0 anonymous users