-
Notifications
You must be signed in to change notification settings - Fork 0
/
Sat.h
62 lines (50 loc) · 1.07 KB
/
Sat.h
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
/*
* Sat.h
*
* Created on: Mar 6, 2016
* Author: RLi
*/
#ifndef SAT_H_
#define SAT_H_
#include <fstream>
#include <iostream>
#include <cstdlib>
#include <string>
#include <vector>
#include <sstream>
#include <algorithm>
#include <stack>
#include <iterator>
using namespace std;
class Sat {
public:
// function prototypes
Sat();
void printInfo();
void printClauses();
void updateNums(int varAssigned, int sign);
vector<int> * getClause(int num);
int reduceUnitClause();
double pureVarSolve();
double solveSSAT();
int RAND();
int MOMS();
int MAX_SAT(vector<int> numPos, vector<int> numNeg);
int returnUCP() {return UCP;}
int returnPVE() {return PVE;}
int returnVOS() {return VOS;}
// variables
vector<int> numActive;
vector<int> assignment;
vector<int> numPos;
vector<int> numNeg;
private:
vector<double> varProb;
vector<vector<int> > posClauses;
vector<vector<int> > negClauses;
vector<vector<int> > clauses;
int UCP;
int PVE;
int VOS;
};
#endif /* SAT_H_ */