Untitled
unknown
plain_text
a year ago
20 kB
6
Indexable
#include<iostream>
#include<string>
#include<fstream>
#include<vector>
using namespace std;
enum State{UNSAT = 0, SAT, CONTIN};
struct info
{
int vari;
char DF;
};
State DPLL(vector<int>, vector<vector<struct info>>, vector<int>, vector<vector<int>>);
State check(vector<vector<struct info>> &);
void input();
void select(int &, int &, vector<vector<int>> &);
void insert0(int, int, vector<int> &, vector<vector<struct info>> &, vector<int> &, vector<vector<int>> &);
void insert1(int, int, vector<int> &, vector<vector<struct info>> &, vector<int> &, vector<vector<int>> &);
void Unit_propagation(vector<int> &, vector<vector<struct info>> &, vector<int> &, vector<vector<int>> &);
void Pure_Literal_Assign(vector<int> &, vector<vector<struct info>> &, vector<int> &, vector<vector<int>> &);
vector<vector<struct info>> Equ;
vector<int> Ans;
vector<vector<int>> Times;
vector<int> Literals;
int main()
{
input();
if(DPLL(Literals, Equ, Ans, Times) == SAT)
{
cout << "s SATISFIABLE" << endl;
for(int i = 1; i < Ans.size(); i++)
{
cout << "v “ " << i << " ” -> ";
if(Ans[i] == 0)
{
cout << "False" << endl;
}
else if(Ans[i] == 1)
{
cout << "True" << endl;
}
else
{
cout << "True" << endl;
}
}
cout << "Done";
cout << endl;
for(int i = 1; i < Ans.size(); i++)
{
if(Ans[i] == 0)
{
cout << "-1 ";
}
else
{
cout << "1 ";
}
}
}
else
{
cout << "s UNSATISFIABLE";
}
}
void input()
{
int m;
int n;
int v;
int j = 0;
string filename;
string s;
ifstream file;
cout << "Enter the file name: ";
cin >> filename;
file.open(filename);
while(file.fail())
{
cout << "File could not be opened." << endl;
cout << "Please enter the input file name: ";
cin >> filename;
file.open(filename);
}
file >> s >> s;
file >> m >> n;
Times.push_back(vector<int>(0));
Times.push_back(vector<int>(0));
for(int i = 1; i <= n; i++)
{
Equ.push_back(vector<struct info>(0));
Literals.push_back(0);
}
for(int i = 0; i <= m; i++)
{
Ans.push_back(2); //initial set 2
Times[0].push_back(0);
Times[1].push_back(0); //complement
}
while(file >> v)
{
if(v == 0 && j == Equ.size()-1)
{
break;
}
else
{
if(v == 0)
{
j++;
}
else
{
struct info R;
R.vari = v;
Equ[j].push_back(R);
Literals[j]++;
if(v > 0)
{
Times[0][v]++;
}
else
{
Times[1][-1*v]++; //complement
}
}
}
}
}
void select(int &m, int &n, vector<vector<int>> ×)
{
m = 0;
n = 1;
int largest = times[m][n];
if(largest < times[1][1])
{
largest = times[1][1];
m = 1;
}
for(int i = 2; i < times[0].size(); i++)
{
if(times[0][i] > largest)
{
largest = times[0][i];
m = 0;
n = i;
}
if(times[1][i] > largest)
{
largest = times[1][i];
m = 1;
n = i;
}
}
}
void insert0(int m, int n, vector<int> &literals, vector<vector<struct info>> &equ0, vector<int> &ans0, vector<vector<int>> ×0)
{
if(m == 0)
{
int v = n;
ans0[v] = 0;
times0[0][n] = 0;
times0[1][n] = 0;
for(int i = 0; i < equ0.size(); i++)
{
if(equ0[i][0].DF == 'D')
continue;
for(int j = 0; j < equ0[i].size(); j++)
{
if(equ0[i][j].vari == v)
{
equ0[i][j].DF = 'F';
literals[i]--;
}
else if(equ0[i][j].vari == -1*v) //be the complement
{
equ0[i][0].DF = 'D';
literals[i] = 0;
for(int k = 0; k < equ0[i].size(); k++)
{
if(equ0[i][k].vari > 0)
{
int t = equ0[i][k].vari;
if(times0[0][t] > 0)
{
times0[0][t]--;
}
}
else //be an complement
{
int t = -1*(equ0[i][k].vari);
if(times0[1][t] > 0)
{
times0[1][t]--;
}
}
}
}
}
}
}
else if(m == 1) //be the complement
{
int v = -1*n; //~A
ans0[n] = 1;
times0[0][n] = 0;
times0[1][n] = 0;
for(int i = 0; i < equ0.size(); i++)
{
if(equ0[i][0].DF == 'D')
continue;
for(int j = 0; j < equ0[i].size(); j++)
{
if(equ0[i][j].vari == v) //~A = 0
{
equ0[i][j].DF = 'F';
literals[i]--;
}
else if(equ0[i][j].vari == -1*v) //A = 1
{
equ0[i][0].DF = 'D';
literals[i] = 0;
for(int k = 0; k < equ0[i].size(); k++)
{
if(equ0[i][k].vari > 0)
{
int t = equ0[i][k].vari;
if(times0[0][t] > 0)
{
times0[0][t]--;
}
}
else //be an complement
{
int t = -1*(equ0[i][k].vari);
if(times0[1][t] > 0)
{
times0[1][t]--;
}
}
}
}
}
}
}
}
void insert1(int m, int n, vector<int> &literals, vector<vector<struct info>> &equ1, vector<int> &ans1, vector<vector<int>> ×1)
{
if(m == 0)
{
int v = n;
ans1[v] = 1;
times1[0][n] = 0;
times1[1][n] = 0;
for(int i = 0; i < equ1.size(); i++)
{
if(equ1[i][0].DF == 'D')
continue;
for(int j = 0; j < equ1[i].size(); j++)
{
if(equ1[i][j].vari == -1*v) //be the complement
{
equ1[i][j].DF = 'F';
literals[i]--;
}
else if(equ1[i][j].vari == v) //assign true to delete clause
{
equ1[i][0].DF = 'D';
literals[i] = 0;
for(int k = 0; k < equ1[i].size(); k++)
{
if(equ1[i][k].vari > 0)
{
int t = equ1[i][k].vari;
if(times1[0][t] > 0)
{
times1[0][t]--;
}
}
else //be an complement
{
int t = -1*(equ1[i][k].vari);
if(times1[1][t] > 0)
{
times1[1][t]--;
}
}
}
}
}
}
}
else if(m == 1) //be the complement
{
int v = -1*n; //~A has to be ture
ans1[n] = 0;
times1[0][n] = 0;
times1[1][n] = 0;
for(int i = 0; i < equ1.size(); i++)
{
if(equ1[i][0].DF == 'D')
continue;
for(int j = 0; j < equ1[i].size(); j++)
{
if(equ1[i][j].vari == -1*v) //A = 0
{
equ1[i][j].DF = 'F';
literals[i]--;
}
else if(equ1[i][j].vari == v) //~A = 1
{
equ1[i][0].DF = 'D';
literals[i] = 0;
for(int k = 0; k < equ1[i].size(); k++)
{
if(equ1[i][k].vari > 0)
{
int t = equ1[i][k].vari;
if(times1[0][t] > 0)
{
times1[0][t]--;
}
}
else //be an complement
{
int t = -1*(equ1[i][k].vari);
if(times1[1][t] > 0)
{
times1[1][t]--;
}
}
}
}
}
}
}
}
State check(vector<vector<struct info>> &equ)
{
int sat = 1;
for(int i = 0; i < equ.size(); i++)
{
if(equ[i][0].DF != 'D')
{
sat *= 0;
}
int unsat = 1;
for(int j = 0; j < equ[i].size(); j++)
{
if(equ[i][j].DF != 'F')
{
unsat *= 0;
}
}
if(unsat == 1)
{
return UNSAT;
}
}
if(sat == 1)
{
return SAT;
}
return CONTIN;
}
State DPLL(vector<int> literals, vector<vector<struct info>> equ, vector<int> ans, vector<vector<int>> times)
{
int m, n;
//copy one as insert 0's
Unit_propagation(literals, equ, ans, times);
if(check(equ) == SAT)
{
Ans = ans;
return SAT;
}
else if(check(equ) == UNSAT)
{
return UNSAT;
}
Pure_Literal_Assign(literals, equ, ans, times);
if(check(equ) == SAT)
{
Ans = ans;
return SAT;
}
else if(check(equ) == UNSAT)
{
return UNSAT;
}
vector<int> literals0 = literals;
vector<vector<struct info>> equ0 = equ;
vector<int> ans0 = ans;
vector<vector<int>> times0 = times;
select(m, n, times);
//first call function to insert 1
//if it's sat return sat and assign current ans to global variable
//else if it's unsat then use the copy and insert 0
// if it's sat return sat and assign current ans to global variable
// else if it's unsat return unsat
// else call DPLL pass current equ and ans by value
//else call DPLL pass current equ and ans by value
insert1(m, n, literals, equ, ans, times);
if(check(equ) == SAT)
{
Ans = ans;
return SAT;
}
else if(check(equ) == UNSAT)
{
insert0(m, n, literals0, equ0, ans0, times0);
if(check(equ0) == SAT)
{
Ans = ans0;
return SAT;
}
else if(check(equ0) == UNSAT)
{
return UNSAT;
}
else
{
return DPLL(literals0, equ0, ans0, times0);
}
}
else
{
if(DPLL(literals, equ, ans, times) == SAT)
{
return SAT;
}
else if(DPLL(literals, equ, ans, times) == UNSAT)
{
insert0(m, n, literals0, equ0, ans0, times0);
if(check(equ0) == SAT)
{
Ans = ans0;
return SAT;
}
else if(check(equ0) == UNSAT)
{
return UNSAT;
}
else
{
return DPLL(literals0, equ0, ans0, times0);
}
}
}
}
void Unit_propagation(vector<int> &literals, vector<vector<struct info>> &equ, vector<int> &ans, vector<vector<int>> ×)
{
for(int i = 0; i < literals.size(); i++)
{
if(literals[i] == 1)
{
int v = equ[i][0].vari;
if(v > 0)
{
ans[v] = 1;
times[0][v] = 0;
times[1][v] = 0;
equ[i][0].DF = 'D';
literals[i] = 0;
for(int j = 0; j < equ.size(); j++)
{
if(equ[j][0].DF == 'D')
continue;
for(int k = 0; k < equ[j].size(); k++)
{
if(equ[j][k].vari == -1*v) //be the complement
{
equ[j][k].DF = 'F';
literals[j]--;
}
else if(equ[j][k].vari == v) //assign true to delete clause
{
equ[j][0].DF = 'D';
literals[j] = 0;
for(int w = 0; w < equ[j].size(); w++)
{
if(equ[j][w].vari > 0)
{
int t = equ[j][w].vari;
if(times[0][t] > 0)
{
times[0][t]--;
}
}
else //be an complement
{
int t = -1*(equ[j][w].vari);
if(times[1][t] > 0)
{
times[1][t]--;
}
}
}
}
}
}
}
else
{
ans[-1*v] = 0;
times[0][-1*v] = 0;
times[1][-1*v] = 0;
equ[i][0].DF = 'D';
literals[i] = 0;
for(int j = 0; j < equ.size(); j++)
{
if(equ[j][0].DF == 'D')
continue;
for(int k = 0; k < equ[j].size(); k++)
{
if(equ[j][k].vari == -1*v) //be the complement
{
equ[j][k].DF = 'F';
literals[j]--;
}
else if(equ[j][k].vari == v) //assign true to delete clause
{
equ[j][0].DF = 'D';
literals[j] = 0;
for(int w = 0; w < equ[j].size(); w++)
{
if(equ[j][w].vari > 0)
{
int t = equ[j][w].vari;
if(times[0][t] > 0)
{
times[0][t]--;
}
}
else //be an complement
{
int t = -1*(equ[j][w].vari);
if(times[1][t] > 0)
{
times[1][t]--;
}
}
}
}
}
}
}
}
}
}
void Pure_Literal_Assign(vector<int> &literals, vector<vector<struct info>> &equ, vector<int> &ans, vector<vector<int>> ×)
{
for(int i = 1; i < times[0].size(); i++)
{
if(times[0][i] == 0 && times[1][i] > 0) //has only complement
{
ans[i] = 0;
times[1][i] = 0;
for(int j = 0; j < equ.size(); j++)
{
if(equ[j][0].DF == 'D')
continue;
for(int k = 0; k < equ[j].size(); k++)
{
if(equ[j][k].vari == -1*i)
{
equ[j][0].DF = 'D';
literals[j] = 0;
for(int m = 0; m < equ[j].size(); m++)
{
if(equ[j][m].vari > 0)
{
if(times[0][equ[j][m].vari] > 0)
{
times[0][equ[j][m].vari]--;
}
}
else
{
if(times[1][-1*(equ[j][m].vari)] > 0)
{
times[1][-1*(equ[j][m].vari)]--;
}
}
}
}
}
}
}
else if(times[0][i] > 0 && times[1][i] == 0) //has no complement
{
ans[i] = 1;
times[0][i] = 0;
for(int j = 0; j < equ.size(); j++)
{
if(equ[j][0].DF == 'D')
continue;
for(int k = 0; k < equ[j].size(); k++)
{
if(equ[j][k].vari == i)
{
equ[j][0].DF = 'D';
literals[j] = 0;
for(int m = 0; m < equ[j].size(); m++)
{
if(equ[j][m].vari > 0)
{
if(times[0][equ[j][m].vari] > 0)
{
times[0][equ[j][m].vari]--;
}
}
else
{
if(times[1][-1*(equ[j][m].vari)] > 0)
{
times[1][-1*(equ[j][m].vari)]--;
}
}
}
}
}
}
}
}
}
Editor is loading...
Leave a Comment