Bonjour à tous, je vous remercie par avance de l'aide que certains pourront m'apporter.

Je vous poste ici le code puis vous explique exactement ce que je n'arrive pas à faire après des heures et des heures de recherche :

Code : Sélectionner tout - Visualiser dans une fenêtre à part
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
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
#include <iostream>
#include <fstream>
#include <set>
#include <string>
#include <sstream>
#include <utility>
#include <algorithm>
#include <map>
#include <list>
 
 
 
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_) {}
 
};
 
std::ostream& operator<<(std::ostream& flux, clause& clause_){
		if(clause_.getFirstVar().isChecked() and clause_.getSecondVar().isChecked())
			flux << clause_.getFirstVar().get_variable() << " ou " << clause_.getSecondVar().get_variable() << " : " << clause_.verified() ;
		else if(clause_.getFirstVar().isChecked() and !clause_.getSecondVar().isChecked())
			flux << clause_.getFirstVar().get_variable() << " ou non" << clause_.getSecondVar().get_variable() << " : " << clause_.verified() ;
		else if(!clause_.getFirstVar().isChecked() and clause_.getSecondVar().isChecked())
			flux << "non " << clause_.getFirstVar().get_variable() << " ou " << clause_.getSecondVar().get_variable() << " : " << clause_.verified() ;
		else 
			flux << "non " << clause_.getFirstVar().get_variable() << " ou non " << clause_.getSecondVar().get_variable() << " : " << clause_.verified() ;
		return flux;
}
 
 
class problem {
 
private:
	typedef std::map<long int, std::map<long int, clause>> myClauses;
	myClauses clauses;
 
	typedef std::map<long int, int> myNegations;
	myNegations negations;
 
	typedef std::map<long int, int> myClaims;
	myClaims claims;
 
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_2, var_1, clause_)));
	}
 
	void remove_clause(long int var) {
		clauses.erase(var);
		for(auto e = map_iterator(); e!=noMap(); ++e){
			if(e->second.find(var) != e->second.end())
				e->second.erase(e->second.find(var));
		}
	}
 
	void create_negation(long int neg) {
		if(negations.find(neg) == no_more_negation()){
			negations[neg] = 1;
		}
		else
			negations[neg]++;
	}
 
	void create_claim(long int claim) {
		if(claims.find(claim) == no_more_claim()){
			claims[claim] = 1;
		}
		else{
			claims[claim]++;
		}
	}
 
	void remove_claim(long int claim) {
		if(claims.find(claim) != no_more_claim()){
			if(claims[claim] == 1)
				claims.erase(claim);
			else
				claims[claim]--;
		}
	}
 
	void remove_all_claim(long int claim) {
		claims.erase(claim);
	}
 
	void remove_all_negation(long int neg) {
		negations.erase(neg);
	}
 
	void remove_negation(long int neg) {
		if(negations.find(neg) != no_more_negation()){
			if(negations[neg] == 1)
				negations.erase(neg);
			else
				negations[neg]--;
		}
	}
 
	void remove_clause_(long int variable) {
		for(auto e = clauses[variable].begin(); e!=clauses[variable].end(); ++e){
			remove_claim(e->second.getSecondVar().get_variable());
			remove_negation(e->second.getSecondVar().get_variable());
			clauses[e->second.getSecondVar().get_variable()].erase(variable);
		}
 
		clauses.erase(variable);        // on supprime les contraintes liées à variable
	}
 
	myClauses get_clauses() {return clauses;};
	myNegations get_negations() {return negations;};
	myClaims get_claims() {return claims;};
 
	bool contains_claim(long int var) {if(claims.find(var) != no_more_claim()) return true; else return false;};
	bool contains_neg(long int neg) {if(negations.find(neg) != no_more_negation()) return true; else return false;};
 
	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::map<long int, int>::iterator negation_iterator() {return negations.begin();};
	std::map<long int, int>::iterator no_more_negation() {return negations.end();};
 
	std::map<long int, int>::iterator claim_iterator() {return claims.begin();};
	std::map<long int, int>::iterator no_more_claim() {return claims.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_claim(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_claim(var1);
			prob.create_negation(abs(var2));
		}
		else {
			prob.create_clause(variable1, variable2, variable1.isChecked() || variable2.isChecked());
			prob.create_claim(var1);
			prob.create_claim(var2);
		}
	}
 
	return prob;
}
 
int simplify_problem(problem& prob) {
	int nb_deletions(0);
	for(auto e = prob.claim_iterator(); e != prob.no_more_claim(); ++e){
		if(!prob.contains_neg(e->first)){
			prob.remove_clause_(e->first);
			prob.remove_all_claim(e->first);
			nb_deletions++;
		}
	}
 
	for(auto e = prob.negation_iterator(); e != prob.no_more_negation(); ++e){
		if(!prob.contains_claim(e->first)){
			prob.remove_clause_(e->first);
			prob.remove_all_negation(e->first);
			nb_deletions++;
		}
	}
 
	return nb_deletions;
}
 
int main(int argc, char* argv[]) {
 
	problem prob = parse("2sat1.txt");
 
	long int k(0);
	for(auto e = prob.map_iterator(); e!= prob.noMap(); ++e){
		for(auto l = e->second.begin(); l!= e->second.end(); ++l){
			k++;
		}
	}
 
 
	std::cout << k << std::endl;
 
	int nb_deletions(-1);
	while(nb_deletions != 0){
		nb_deletions = simplify_problem(prob);
		std::cout << nb_deletions << std::endl;
	}
 
	k = 0;
	for(auto e = prob.map_iterator(); e!= prob.noMap(); ++e){
		for(auto l = e->second.begin(); l!= e->second.end(); ++l)
			k++;
	}
	std::cout << k / 2 << " constraints " << std::endl;
 
	for(auto e = prob.claim_iterator(); e != prob.no_more_claim(); ++e){
		if(!prob.contains_neg(e->first))
			std::cout << "un intrus " << e->first << std::endl;
	}
 
	for(auto e = prob.negation_iterator(); e!=prob.no_more_negation(); ++e){
		if(!prob.contains_claim(e->first))
			std::cout << "un intrus " << e->second << std::endl;
	}
 
	return 0;
}
Le fond du problème ce sont les fonctions simplify_problem et remove_clause. En fait je dois simplifier mon problème selon le principe suivant, prenons l'exemple : (les variables sont toutes booleennes)

contrainte 1 : A ou non(B)
contrainte 2 : B ou non(C)
contrainte 3 : A ou C

On voit que non(A) n'apparait jamais donc on peut supprimer A de la liste des variables et toutes les clauses qui impliquent A soit les contraintes 1 et 3. Mais en faisant cela on s'aperçoit que maintenant C et non(B) n'apparaissent jamais donc on peut supprimer B et C ainsi que toutes les clauses impliquant B et C.

Et bien ma fonction simplify_problem a pour but de faire une itération et la boucle

Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
int nb_deletions(-1);
	while(nb_deletions != 0){
		nb_deletions = simplify_problem(prob);
		std::cout << nb_deletions << std::endl;
	}
a pour but de répéter l'opération tant qu'on peut supprimer des contraintes.

Pour ce faire voici comment j'opère, je parcours la map dans laquelle se trouvent mes variables claims (les variables qui apparaissent sous la forme A) et je regarde si ma variable se trouve aussi dans mes variables negations (celles qui apparaissent dans les contraintes sous la forme non(A)). Si elle n'apparait pas c'est que je peux la supprimer et toutes les contraintes qui vont avec !

Ca c'est a priori relativement facile, ce qui l'est moins (pour moi en tout cas). C'est que pour reprendre l'exemple basique que j'ai montré une fois que j'ai supprimé la contrainte 1, non(B) n'apparait plus dans mes negations et donc je dois l'enlever.

En fait ce qui est compliqué c'est que j'ai 100 000 contraintes dans le fichier qui décrit l'instance de mon problème : et A peut apparaitre plusieurs fois dans claims ou dans negations.

Si c'est la variable que je regarde et qu'elle n'appartient pas à mes deux maps (claims et negations) alors je supprime complètement la variable de claims ou de négations mais si c'est une variable impliquée dans une contrainte comme par exemple B dans mon exemple je ne supprime que "une présence" (elle peut apparaitre dans plusieurs contraintes sous la forme non(B) par exemple A et non(B), D et non(B) et donc je ne dois pas la supprimer d'un coup).

Pour ce faire j'ai codé remove_claim et remove_negation mais ça ne marche pas, il me reste à la fin 34 975 contraintes alors qu'il devrait m'en rester 6...