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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
| #include <iostream>
#include <fstream>
#include <set>
#include <string>
#include <sstream>
#include <utility>
#include <algorithm>
#include <map>
class variable {
private:
long int var;
bool checked;
public:
long int get_variable() {return var;};
bool isChecked() {return checked;};
void setChecked(bool boolean) {checked = boolean;};
variable(long int var_, bool checked_) : var(var_), checked(checked_) {}
};
class clause {
private:
variable var_1;
variable var_2;
bool expression;
public:
bool verified() {return expression;};
variable getFirstVar() const {return var_1;};
variable getSecondVar() const {return var_2;};
clause(variable var_1_, variable var_2_, bool clause_) : var_1(var_1_), var_2(var_2_), expression(clause_) {}
};
class problem {
private:
typedef std::map<long int, std::map<long int, clause>> myClauses;
myClauses clauses;
typedef std::set<long int> myVariables;
myVariables variables;
typedef std::set<long int> myNegations;
myNegations negations;
public:
void create_clause(variable var_1, variable var_2, bool clause_) {
clauses[var_1.get_variable()].insert(std::make_pair(var_2.get_variable(), clause(var_1, var_2, clause_)));
clauses[var_2.get_variable()].insert(std::make_pair(var_1.get_variable(), clause(var_1, var_2, clause_)));
}
void create_variable(long int var) {variables.insert(var);};
void create_negation(long int neg) {negations.insert(neg);};
void remove_variable(long int var) {variables.erase(var);};
std::set<long int>::iterator remove_variable_by_iterator(std::set<long int>::iterator it) {variables.erase(it); return it;};
void remove_negation(long int neg) {negations.erase((neg));};
void remove_clause(long int variable) {}
myClauses get_clauses() {return clauses;};
myVariables get_variables() {return variables;};
myNegations get_negations() {return negations;};
std::map<long int, std::map<long int, clause>>::iterator map_iterator() {return clauses.begin();};
std::map<long int, std::map<long int, clause>>::iterator noMap() {return clauses.end();};
std::map<long int, clause>::iterator clause_iterator(std::map<long int, clause> m) {return m.begin();};
std::map<long int, clause>::iterator noClause(std::map<long int, clause> m) {return m.end();};
std::set<long int>::iterator variable_iterator() {return variables.begin();};
std::set<long int>::iterator no_more_variable() {return variables.end();};
std::set<long int>::iterator negation_iterator() {return negations.begin();};
std::set<long int>::iterator no_more_negation() {return negations.end();};
};
problem parse(const char* filename) {
problem prob;
std::string line;
std::ifstream fichier(filename);
getline(fichier, line);
while(std::getline(fichier, line)){
std::istringstream iss(line);
long int var1, var2;
iss >> var1 >> var2;
variable variable1(abs(var1), true);
variable variable2(abs(var2), true);
if(var1 < 0 and var2 > 0) {
prob.create_clause(variable1, variable2, !variable1.isChecked() || variable2.isChecked());
prob.create_negation(abs(var1));
prob.create_variable(var2);
}
else if(var1 < 0 and var2 < 0) {
prob.create_clause(variable1, variable2, !variable1.isChecked() || !variable2.isChecked());
prob.create_negation(abs(var1));
prob.create_negation(abs(var2));
}
else if(var1 > 0 and var2 < 0) {
prob.create_clause(variable1, variable2, variable1.isChecked() || !variable2.isChecked());
prob.create_variable(var1);
prob.create_negation(abs(var2));
}
else {
prob.create_clause(variable1, variable2, variable1.isChecked() || variable2.isChecked());
prob.create_variable(var1);
prob.create_variable(var2);
}
}
return prob;
}
void simplify_problem(problem& prob) {
for(auto e = prob.variable_iterator(); e!= prob.no_more_variable(); ++e){
std::cout << *e << std::endl;
if(prob.get_negations().find(*e) == prob.no_more_negation()){
std::cout << "yo " << *e << std::endl;
e = prob.remove_variable_by_iterator(e);
}
else
++e;
}
}
int main(int argc, char* argv[]) {
problem prob = parse("2sat1.txt");
for(auto e = prob.map_iterator(); e!= prob.noMap(); ++e){
for(auto el = prob.clause_iterator(e->second); el!= prob.noClause(e->second); ++el)
std::cout << el->second.getFirstVar().get_variable() << " - " << el->second.getSecondVar().get_variable() << " ; " << el->second.verified() << std::endl;
}
std::cout << prob.get_variables().size() << std::endl;
std::cout << prob.get_negations().size() << std::endl;
/*for(auto e = prob.negation_iterator(); e!=prob.no_more_negation(); ++e){
std::cout << *e << std::endl;
}*/
simplify_problem(prob);
std::cout << *(prob.get_variables().find(3)) << std::endl;
std::cout << *(prob.get_negations().find(3)) << std::endl;
return 0;
}
/*
Make lists of all variables and negations.
If there is a variable that appears in one list but not the other then remove that variable
from the list it does appear in and all clauses containing that variable from the list of clauses.
If you want to keep track of what to set it to (I didn't, but wish I had and may go back and code it in)
then set the value for any variable that appears without negation to T and any that only appears negated to F.
Do this repeatedly until you reach a loop with no deletions. Remember to rebuild the lists of variables and
negations each time through (this is what I forgot to do when I coded it up in the wee hours of the morning).
Basically instead of looping over all clauses just loop over failing ones and flip values there.
So you need to maintain linked list of failing clauses and additionally dictionary of clauses indexed by variable
(use simple array for that). Every time algorithm flips the variable you only re-evaluate clauses in which this variable appears,
updating linked list of failing clauses accordingly.
*/ |
