Discussion :

[isangoma]

Tu peux éventuellement passer sur une map<int, bool>, si les variables ne sont pas numérotées continuellement de 0 à max

Je pense qu'il est plus efficace dans ce cas de faire une fonction qui va mapper les variables de 0 a N.
L'avantage du vecteur sur les map/set ... est l'acces en temps constant, mais bon, a la fin, cela ne doit pas vraiment faire une grosse difference.

[ternel]

si on sait d'avance avoir des variables de 0 à N (ou même de k à k+N), il vaut mieux avoir un vector.

On peut même écrire std::vector<bool> bools(N, false);, ce qui évitera normalement toute réallocation.

Le mapping est linéaire sur le nombre de variable, il faut le faire deux fois, certes, mais ca peut faire gagner du temps.
Je ne suis pas sur que le problème soit si sensible en performance, par rapport à l'algo pur.

[ImmoTPA]

Désolé les gars mais je crois que je m'emmêle les pinceaux, j'en suis là :

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
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
#include <iostream>
#include <fstream>
#include <set>
#include <string>
#include <sstream>
#include <utility>
#include <algorithm>
#include <map>
#include <list>
#include <ctime>
#include <cmath>
 
using id_t_ = long int;
 
class variable {
 
private:
	id_t var;
	bool checked;
 
public:
	variable(id_t_ var_, bool checked_) : var(var_), checked(checked_) {}
 
	id_t_ operator* () const {return var;}
	operator bool() const {return checked;}
	bool operator !() const {return !checked;}
 
	bool isChecked() {return checked;};
	void setChecked(bool boolean) {checked = boolean;};
 
	id_t_ id() const {return var;};
	bool toggle() {return checked = !checked;};
 
};
 
std::ostream& operator<<(std::ostream& os, variable const& that) {
	if (!that) os << "non ";
	return os << *that;
}
 
class clause {
 
private:
	variable var_1;
	variable var_2;
	bool expression;
 
public:
	bool verified() const {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, const clause& that) {
	return flux << that.getFirstVar() << " ou " << that.getSecondVar() << " : " << that.verified() ;
}
 
/*struct clause_compare {
	bool operator() (clause const& c1, clause const& c2){
		return c1.getFirstVar().id() < c2.getFirstVar().id() ;
	}
};*/
 
class problem {
 
private:
	typedef std::map<id_t_, clause> clause_t;
	typedef std::map<id_t_, clause_t> myClauses;
	myClauses clauses;
 
	typedef std::map<id_t_, int> myNegations;
	myNegations negations;
 
	typedef std::map<id_t_, int> myClaims;
	myClaims claims;
 
	typedef std::map<id_t_, bool> myVariables;
	myVariables variables;
 
	/*typedef std::set<clause, clause_compare> myfailedClauses;
	myfailedClauses failedClauses;*/
 
	typedef myClauses myfailedClauses;
	myfailedClauses failedClauses;
 
public:
	void create_clause(variable const& var_1, variable const& var_2, bool clause_) {
		clauses[*var_1].insert(std::make_pair(*var_2, clause(var_1, var_2, clause_))); // on ajoute chaque contrainte deux fois
		clauses[*var_2].insert(std::make_pair(*var_1, clause(var_2, var_1, clause_))); // sous la forme clauses[x1][x2] et clauses[x2][x1]
	}
 
	void create_negation(id_t_ neg) {
		if(negations.find(neg) == no_more_negation()){
			negations[neg] = 1;
		}
		else
			negations[neg]++;
	}
 
	void create_claim(id_t_ claim) {                // si la variable n'existe pas dans claim on la crée et l'ajoute 
		if(claims.find(claim) == no_more_claim()){
			claims[claim] = 1;
		}
		else{
			claims[claim]++;                          // sinon on ajoute 1 au nombre de fois que la variable apparait (en positif)
		}
	}
 
	void remove_claim(id_t_ claim) {               
		if(claims.find(claim) != no_more_claim()){  // si la variable existe dans claim
			if(claims[claim] == 1)                   // si elle est présente une fois elle va disparaitre donc on la supprime de la map
				claims.erase(claim);
			else
				claims[claim]--;                      // sinon on décrémente le nombre d'apparitions de 1
		}
	}
 
	void remove_all_claim(id_t_ claim) {
		claims.erase(claim);
	}
 
	void remove_all_negation(id_t_ neg) {
		negations.erase(neg);
	}
 
	void remove_negation(id_t_ neg) {
		if(negations.find(neg) != no_more_negation()){
			if(negations[neg] == 1)
				negations.erase(neg);
			else
				negations[neg]--;
		}
	}
 
	void remove_clause_(id_t_ variable) {
		for(auto e = clauses[variable].begin(); e!=clauses[variable].end(); ++e){
			if(e->second.getSecondVar().isChecked()){
				remove_claim(e->second.getSecondVar().id()); 	
			}	
			else{																	//on décrémente le nbr d'apparations dans claims ou négations de la variation impliquée 
				remove_negation(e->second.getSecondVar().id());
			}																		// dans la contrainte avec la variable "variable"
			clauses[e->second.getSecondVar().id()].erase(variable);		// on supprime les contraintes du style map[x][variable] qui sont les symétriques de
		}																			// celles qu'on supprime juste après
 
		clauses.erase(variable);        // on supprime les contraintes liées à variable dans map[variable] donc ça supprime une map<long int(la variable), clause>
	}
 
	void rem_clause(id_t_ var) {
		clauses.erase(var);
	}
 
	myClauses get_clauses() {return clauses;};
	myNegations get_negations() {return negations;};
	myClaims get_claims() {return claims;};
	myfailedClauses get_failed_clauses() {return failedClauses;};
	myVariables get_variables() {return variables;};
 
	bool contains_claim(id_t var) {if(claims.find(var) != no_more_claim()) return true; else return false;};
	bool contains_neg(id_t neg) {if(negations.find(neg) != no_more_negation()) return true; else return false;};
 
	myClauses::iterator map_iterator() {return clauses.begin();};
	myClauses::iterator noMap() {return clauses.end();};
 
	clause_t::iterator clause_iterator(std::map<id_t_, clause> m) {return m.begin();};
	clause_t::iterator noClause(std::map<id_t_, clause> m) {return m.end();};
 
	myNegations::iterator negation_iterator() {return negations.begin();};
	myNegations::iterator no_more_negation() {return negations.end();};
 
	myClaims::iterator claim_iterator() {return claims.begin();};
	myClaims::iterator no_more_claim() {return claims.end();};
 
	int size() {
		clause_t::size_type count = 0;
		for(auto e = map_iterator(); e!= noMap(); ++e){
			count += e->second.size();
		}
		return count;
	}
 
	myNegations::size_type negates_count() const {
		return negations.size();
	}
 
 	myClaims::size_type claims_count() const {
		return claims.size();
	}
 
	myfailedClauses::size_type fails_count() const {
		return failedClauses.size();
	}
 
	myVariables::size_type var_count() const {
		return variables.size();
	}
 
	void compute_failed_clauses() {
		for(auto e = map_iterator(); e != noMap(); ++e){
			for(auto l = e->second.begin(); l != e->second.end(); ++l){
				if(!l->second.verified()){
					failedClauses[e->first].insert(std::make_pair(l->first, l->second));
				}
			}
		}
	}
};
 
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;
 
		if(var1 < 0 and var2 > 0) {	
			variable variable1(abs(var1), false);
			variable variable2(var2, true);
			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) {
			variable variable1(abs(var1), false);
			variable variable2(abs(var2), false);
			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) {
			variable variable1(var1, true);
			variable variable2(abs(var2), false);
			prob.create_clause(variable1, variable2, variable1.isChecked() || !variable2.isChecked());
			prob.create_claim(var1);
			prob.create_negation(abs(var2));
		}
		else {
			variable variable1(var1, true);
			variable variable2(var2, true);
			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){ // on parcourt les claims et on vérifie qu'elles sont dans les negations
		if(!prob.contains_neg(e->first)){ 
			prob.remove_clause_(e->first);	 
			prob.remove_all_claim(e->first);              //si c'est pas le cas	// on supprime les clauses liées à la variable en question																// on supprime la variable de la map claims
			nb_deletions++;
		}
	}
 
	for(auto e = prob.negation_iterator(); e != prob.no_more_negation(); ++e){  // on parcourt les negations et ...
		if(!prob.contains_claim(e->first)){
			prob.remove_clause_(e->first);						
			prob.remove_all_negation(e->first);
			nb_deletions++;
		}
	}
 
	return nb_deletions;
}
 
void initialize(problem& prob) {
 
	// créer un assignment random
 
	for(auto e = prob.map_iterator(); e != prob.noMap(); ++e){
		int r(rand()%2);
		if(r==0){
			prob.get_variables()[e->first] = true;
		}
		else
			prob.get_variables()[e->first] = false;
 
		for(auto l = e->second.begin(); l != e->second.end(); ++l){
			int r(rand()%2);
			if(r==0){
				prob.get_variables()[l->first] = true;
			}
			else 
				prob.get_variables()[l->first] = false;
 
		}
	}
}
 
void flip_value(problem& prob, clause& clause_) {
	int r(rand()%2);
	if(r==0){
		bool update = clause_.getFirstVar().toggle();
		prob.get_variables()[clause_.getFirstVar().id()] = update;
	}
	else{
		clause_.getSecondVar().toggle();
		bool update = clause_.getSecondVar().toggle();
		prob.get_variables()[clause_.getFirstVar().id()] = update;
	}
}
 
clause pick_random_clause(problem& prob){
	int size = prob.fails_count();
	int r = 2*rand()%size;
	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++;
			if(k%r == 0){
				return l->second;
			}
		}
	}
}
 
 
bool papadimitriou(problem& prob) {
	int nb_deletions(-1);
	while(nb_deletions != 0){
		nb_deletions = simplify_problem(prob);
	}
 
	for(auto e = prob.map_iterator(); e != prob.noMap(); ++e){ 						//pour remove les doublons
		for(auto el = e->second.begin(); el != e->second.end(); ++el){
			prob.rem_clause(el->first);
		}
	}
 
	int steps(prob.var_count());
	for(int k(0); k < log2(steps); k++){
		initialize(prob);
		for(int j(0); j < 2*pow(steps, 2); ++j){
			prob.compute_failed_clauses();
			if(prob.fails_count() > 0){
				std::cout << prob.fails_count() << "cou" << std::endl;
				clause c = pick_random_clause(prob);
				flip_value(prob, c);
			}
			else {
				std::cout << 1 << std::endl;
				return true;
			}
		}
	}
	std::cout << 0 << std::endl;
	return false;
}
 
 
int main(int argc, char* argv[]) {
 
	problem prob = parse("2sat1.txt");
 
	papadimitriou(prob);
 
	problem prob2 = parse("2sat2.txt");
 
	papadimitriou(prob2);
 
	problem prob3 = parse("2sat3.txt");
 
	papadimitriou(prob3);
 
	problem prob4 = parse("2sat4.txt");
 
	papadimitriou(prob4);
 
	problem prob5 = parse("2sat5.txt");
 
	papadimitriou(prob5);
 
	problem prob6 = parse("2sat6.txt");
 
	papadimitriou(prob6);
/*	int k(0);
	for(auto e = prob.map_iterator(); e!=prob.noMap(); ++e){
		for(auto el = e->second.begin(); el!=e->second.end(); el++){
			std::cout << el->second << std::endl;
			k++;
		}
	}
 
	std::cout << k << std::endl;*/
 
	return 0;
}

L'execution me retourne 000000 (ce qui au delà d'être faux ne semble pas cohérent puisque si le problème n'a pas de solution j'aurai au moins du rentrer dans la boucle if(prob.fails_count() > 0)
std::cout << prob.fails_count << "cou" << std::endl;

Le problème c'est que je suis perdu entre, d'une part initialiser mes variables quand je lis le fichier pour pouvoir le simplifier, donner un état initial qui soit cohérent et ensuite réussir quand je modifie une variable à correctement mettre à jours les clauses non respectées. Je crois que j'ai plusieurs problème aussi bien dans ma fonction initialize que compute_fails mais si jamais quelque chose vous saute aux yeux je vous serai reconnaissant.

[ternel]

Pour moi, le début du problème, c'est que tu n'as pas l'air d'avoir posé la bonne représentation.
Mais comme je n'ai pas encore pris le temps de comprendre les maths de l'algo, je ne sais pas encore.

Quoi qu'il en soit, ceci n'est pas un code satisfaisant pour une première implémentation d'algo (je ne parle pas encore d'optimisation):

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
bool papadimitriou(problem& prob) {
	int nb_deletions(-1);
	while(nb_deletions != 0){
		nb_deletions = simplify_problem(prob);
	}
 
	for(auto e = prob.map_iterator(); e != prob.noMap(); ++e){ 						//pour remove les doublons
		for(auto el = e->second.begin(); el != e->second.end(); ++el){
			prob.rem_clause(el->first);
		}
	}
 
	int steps(prob.var_count());
	for(int k(0); k < log2(steps); k++){
		initialize(prob);
		for(int j(0); j < 2*pow(steps, 2); ++j){
			prob.compute_failed_clauses();
			if(prob.fails_count() > 0){
				std::cout << prob.fails_count() << "cou" << std::endl;
				clause c = pick_random_clause(prob);
				flip_value(prob, c);
			}
			else {
				std::cout << 1 << std::endl;
				return true;
			}
		}
	}
	std::cout << 0 << std::endl;
	return false;
}

J'aimerai clairement avoir un code ou chaque paire de parenthèse signifie quelque chose de mathématique.

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
bool papadimitriou(problem& prob) {
	while(prob.simplify());
	prob.trimDuplicates();
	//et encore, ca pourrait etre
	//prob.simplifyAll();
 
 	const int steps = prob.var_count());
	for(int k = 0; k < log2(steps); k++){
		prob.initialize();
		for(int j = 0; j < 2*steps*steps; ++j){
			const int failed = prob.compute_failed_clauses();
			if(failed == 0){
				return true;
			}
			std::cout << failed << "cou" << std::endl;
			prob.flipRandomClause();
		}
	}
	return false;
}

[ImmoTPA]

Voilà j'ai réarrangé le code comme tu me l'as demandé c'est vrai que c'est plus propre, par contre j'ai une erreur à la ligne 289 et 293 à cause de

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

clause c(l->second);

je sais que la portée de cette variable ne va pas au delà du for mais je ne sais pas comment me débrouiller autrement. Si je fais clause c; avant le for il me dit naturellement que le constructeur en question n'existe pas.
Je pourrai créer un constructeur par défaut avec des variables bidons mais ça m'ennuie car ça serait source d'erreurs.

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
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
#include <iostream>
#include <fstream>
#include <set>
#include <string>
#include <sstream>
#include <utility>
#include <algorithm>
#include <map>
#include <list>
#include <ctime>
#include <cmath>
 
using id_t_ = long int;
 
class variable {
 
private:
	id_t var;
	bool checked;
 
public:
	variable(id_t_ var_, bool checked_) : var(var_), checked(checked_) {}
 
	id_t_ operator* () const {return var;}
	operator bool() const {return checked;}
	bool operator !() const {return !checked;}
 
	bool isChecked() {return checked;};
	void setChecked(bool boolean) {checked = boolean;};
 
	id_t_ id() const {return var;};
	bool toggle() {return checked = !checked;};
 
};
 
std::ostream& operator<<(std::ostream& os, variable const& that) {
	if (!that) os << "non ";
	return os << *that;
}
 
class clause {
 
private:
	variable var_1;
	variable var_2;
	bool expression;
 
public:
	bool verified() const {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, const clause& that) {
	return flux << that.getFirstVar() << " ou " << that.getSecondVar() << " : " << that.verified() ;
}
 
class problem {
 
private:
	typedef std::map<id_t_, clause> clause_t;
	typedef std::map<id_t_, clause_t> myClauses;
	myClauses clauses;
 
	typedef std::map<id_t_, int> myNegations;
	myNegations negations;
 
	typedef std::map<id_t_, int> myClaims;
	myClaims claims;
 
	typedef std::map<id_t_, bool> myVariables;
	myVariables variables;
 
	typedef myClauses myfailedClauses;
	myfailedClauses failedClauses;
 
public:
	void create_clause(variable const& var_1, variable const& var_2, bool clause_) {
		clauses[*var_1].insert(std::make_pair(*var_2, clause(var_1, var_2, clause_))); // on ajoute chaque contrainte deux fois
		clauses[*var_2].insert(std::make_pair(*var_1, clause(var_2, var_1, clause_))); // sous la forme clauses[x1][x2] et clauses[x2][x1]
	}
 
	void create_negation(id_t_ neg) {
		if(negations.find(neg) == no_more_negation()){
			negations[neg] = 1;
		}
		else
			negations[neg]++;
	}
 
	void create_claim(id_t_ claim) {                // si la variable n'existe pas dans claim on la crée et l'ajoute 
		if(claims.find(claim) == no_more_claim()){
			claims[claim] = 1;
		}
		else{
			claims[claim]++;                          // sinon on ajoute 1 au nombre de fois que la variable apparait (en positif)
		}
	}
 
	void remove_claim(id_t_ claim) {               
		if(claims.find(claim) != no_more_claim()){  // si la variable existe dans claim
			if(claims[claim] == 1)                   // si elle est présente une fois elle va disparaitre donc on la supprime de la map
				claims.erase(claim);
			else
				claims[claim]--;                      // sinon on décrémente le nombre d'apparitions de 1
		}
	}
 
	void remove_all_claim(id_t_ claim) {
		claims.erase(claim);
	}
 
	void remove_all_negation(id_t_ neg) {
		negations.erase(neg);
	}
 
	void remove_negation(id_t_ neg) {
		if(negations.find(neg) != no_more_negation()){
			if(negations[neg] == 1)
				negations.erase(neg);
			else
				negations[neg]--;
		}
	}
 
	void remove_clause_(id_t_ variable) {
		for(auto e = clauses[variable].begin(); e!=clauses[variable].end(); ++e){
			if(e->second.getSecondVar().isChecked()){
				remove_claim(e->second.getSecondVar().id()); 	
			}	
			else{																	//on décrémente le nbr d'apparations dans claims ou négations de la variation impliquée 
				remove_negation(e->second.getSecondVar().id());
			}																		// dans la contrainte avec la variable "variable"
			clauses[e->second.getSecondVar().id()].erase(variable);		// on supprime les contraintes du style map[x][variable] qui sont les symétriques de
		}																			// celles qu'on supprime juste après
 
		clauses.erase(variable);        // on supprime les contraintes liées à variable dans map[variable] donc ça supprime une map<long int(la variable), clause>
	}
 
	void rem_clause(id_t_ var) {
		clauses.erase(var);
	}
 
	myClauses get_clauses() {return clauses;};
	myNegations get_negations() {return negations;};
	myClaims get_claims() {return claims;};
	myfailedClauses get_failed_clauses() {return failedClauses;};
	myVariables get_variables() {return variables;};
 
	bool contains_claim(id_t var) {if(claims.find(var) != no_more_claim()) return true; else return false;};
	bool contains_neg(id_t neg) {if(negations.find(neg) != no_more_negation()) return true; else return false;};
 
	myClauses::iterator map_iterator() {return clauses.begin();};
	myClauses::iterator noMap() {return clauses.end();};
 
	myfailedClauses::iterator fail_iterator() {return failedClauses.begin();};
	myfailedClauses::iterator no_more_fail() {return failedClauses.end();};
 
	clause_t::iterator clause_iterator(std::map<id_t_, clause> m) {return m.begin();};
	clause_t::iterator noClause(std::map<id_t_, clause> m) {return m.end();};
 
	myNegations::iterator negation_iterator() {return negations.begin();};
	myNegations::iterator no_more_negation() {return negations.end();};
 
	myClaims::iterator claim_iterator() {return claims.begin();};
	myClaims::iterator no_more_claim() {return claims.end();};
 
	int size() {
		clause_t::size_type count = 0;
		for(auto e = map_iterator(); e!= noMap(); ++e){
			count += e->second.size();
		}
		return count;
	}
 
	myNegations::size_type negates_count() const {
		return negations.size();
	}
 
 	myClaims::size_type claims_count() const {
		return claims.size();
	}
 
	myfailedClauses::size_type fails_count() const {
		return failedClauses.size();
	}
 
	myVariables::size_type var_count() const {
		return variables.size();
	}
 
	int compute_failed_clauses() {
		int nb_fails(0);
		for(auto e = map_iterator(); e != noMap(); ++e){
			for(auto l = e->second.begin(); l != e->second.end(); ++l){
				if(!l->second.verified()){
					failedClauses[e->first].insert(std::make_pair(l->first, l->second));
					nb_fails++;
				}
			}
		}
		return nb_fails;
	}
 
	int simplify_problem() {
		int nb_deletions(0);
		for(auto e = claim_iterator(); e != no_more_claim(); ++e){ // on parcourt les claims et on vérifie qu'elles sont dans les negations
			if(!contains_neg(e->first)){ 
				remove_clause_(e->first);	 
				remove_all_claim(e->first);              //si c'est pas le cas	// on supprime les clauses liées à la variable en question																// on supprime la variable de la map claims
				nb_deletions++;
			}
		}
 
		for(auto e = negation_iterator(); e != no_more_negation(); ++e){  // on parcourt les negations et ...
			if(!contains_claim(e->first)){
				remove_clause_(e->first);						
				remove_all_negation(e->first);
				nb_deletions++;
			}
		}
 
		return nb_deletions;
	}
 
	void simplifyAll(){
		int nb_deletions(-1);
		while(nb_deletions != 0){
			nb_deletions = simplify_problem();
		}
		for(auto e = map_iterator(); e != noMap(); ++e){ 						//pour remove les doublons
			for(auto el = e->second.begin(); el != e->second.end(); ++el){
				rem_clause(el->first);
			}
		}
	}
 
	void initialize() {
 
	// créer un assignment random
 
		for(auto e = map_iterator(); e != noMap(); ++e){
			int r(rand()%2);
			if(r==0){
				get_variables()[e->first] = true;
			}
			else
				get_variables()[e->first] = false;
			for(auto l = e->second.begin(); l != e->second.end(); ++l){
				int r(rand()%2);
				if(r==0){
					get_variables()[l->first] = true;
				}
				else 
					get_variables()[l->first] = false;
			}
		}
	}
 
	void flip_value(clause& clause_) {
		int r(rand()%2);
		if(r==0){
			bool update = clause_.getFirstVar().toggle();
			get_variables()[clause_.getFirstVar().id()] = update;
		}
		else{
			clause_.getSecondVar().toggle();
			bool update = clause_.getSecondVar().toggle();
			get_variables()[clause_.getFirstVar().id()] = update;
		}
	}
 
	void flipRandomClause() {
		int size = fails_count();
		int r = rand()%size;
		int k(0);
		for(auto e = fail_iterator(); e != no_more_fail(); ++e){
			for(auto l = e->second.begin(); l != e->second.end(); ++l){
				k++;
				if(k == r){
					clause c(l->second);
				}
			}
		}
		int r2(rand()%2);
		if(r2 == 0){
			bool update = c.getFirstVar().toggle();
			get_variables()[c.getFirstVar().id()] = update;
		}
		else{
			c.getSecondVar().toggle();
			bool update = c.getSecondVar().toggle();
			get_variables()[c.getFirstVar().id()] = update;
		}
	}
};
 
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;
 
		if(var1 < 0 and var2 > 0) {	
			variable variable1(abs(var1), false);
			variable variable2(var2, true);
			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) {
			variable variable1(abs(var1), false);
			variable variable2(abs(var2), false);
			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) {
			variable variable1(var1, true);
			variable variable2(abs(var2), false);
			prob.create_clause(variable1, variable2, variable1.isChecked() || !variable2.isChecked());
			prob.create_claim(var1);
			prob.create_negation(abs(var2));
		}
		else {
			variable variable1(var1, true);
			variable variable2(var2, true);
			prob.create_clause(variable1, variable2, variable1.isChecked() || variable2.isChecked());
			prob.create_claim(var1);
			prob.create_claim(var2);
		}
	}
 
	return prob;
}
 
 
bool papadimitriou(problem& prob) {
 
	prob.simplifyAll();
 
	const int steps(prob.var_count());
	for(int k(0); k < log2(steps); k++){
		std::cout << k << std::endl;
		prob.initialize();
		for(int j(0); j < 2*steps*steps; ++j){
			const int fails = prob.compute_failed_clauses();
			if(fails == 0){
				return true;
			}
			else{
				std::cout << prob.fails_count() << "coucou" << std::endl;
				prob.flipRandomClause();
			}
		}
	}
	return false;
}
 
 
int main(int argc, char* argv[]) {
 
	problem prob = parse("2sat1.txt");
 
	papadimitriou(prob);
 
	int k(0);
	for(auto e = prob.map_iterator(); e!=prob.noMap(); ++e){
		for(auto el = e->second.begin(); el!=e->second.end(); el++){
			std::cout << el->second << std::endl;
			k++;
		}
	}
 
	std::cout << k << std::endl;
 
	problem prob2 = parse("2sat2.txt");
 
	papadimitriou(prob2);
 
	problem prob3 = parse("2sat3.txt");
 
	papadimitriou(prob3);
 
	k = 0;
	for(auto e = prob2.map_iterator(); e!=prob2.noMap(); ++e){
		for(auto el = e->second.begin(); el!=e->second.end(); el++){
			std::cout << el->second << std::endl;
			k++;
		}
	}
 
	std::cout << k << std::endl;
 
	problem prob4 = parse("2sat4.txt");
 
	papadimitriou(prob4);
 
	problem prob5 = parse("2sat5.txt");
 
	papadimitriou(prob5);
 
	problem prob6 = parse("2sat6.txt");
 
	papadimitriou(prob6);
 
 
	return 0;
}

[isangoma]

Salut,
Je viens de relire ton code, et je pense vraiment que tu te compliques beaucoup la vie. Mais bon.

Alors pour ton dernier probleme.

je sais que la portée de cette variable ne va pas au delà du for

Meme pas, la porte de ton

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

clause c(l->second);

est uniquement dans le if.

Ce que tu peux faire c'est de creer un pointeur vers un objet clause a la ligne 278.
Dans ton if, tu vas creer l'objet clause.
Et tu n'oublies pas de le detruire a la fin.

Autre option, tu vas creer un constructeur par defaut pour ta classe clause. Et tu permets une initialisation des variables plus tard.

Sinon d'un point de vue conceptuel, quelque chose me derange.
Une variable n'est ni positive ni negative, c'est juste une variable.
Par contre dans un clause, on peut considerer une variable ou sa negation.
Du coup j'aurais plus definit clause comme ca :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
 
class clause { 
private:
	variable var_1;
	bool var_1_sign;
        variable var_2;
        bool var_2_sign
	bool expression;

Ou alors avec une pair, mais l'idee est la.
Je pense que cela simplifie beaucoup le reste. Car tu peux par la suite creer une fonction dans la classe clause qui repond true ou false selon si la clause est verifie ou non.
Cette fonction appelle ses variables, regarde leur valeur actuelle et renvois le resultat.
Il suffit ensuite de boucler sur toute tes clauses pour savoir si ton probleme est satisfait avec la distribution actuelle.

Pour finir, tu devrais commenter plus ton code
Et si tu peux, envois un fichier .txt avec tes clauses/variables.

[ImmoTPA]

Merci beaucoup ! Okay je vais essayer de davantage commenter. Et j'ai pensé à quelque chose comme ça hier soir je me suis rendu compte que mn problème principal c'est que je ne peux pas vérifier simplement si une clause est vérifiée ou non, en fin d'après-midi j'aurai du temps pour essayer quelque chose comme ce que tu m'as dit.

Pour le coup du pointeur sur objet c'est :

créer un pointeur initialiser à null

créer l'objet clause et mettre à jour le pointeur à l'adresse de la clause ?

[ternel]

Quitte à revoir le code, reprends de zéro. Ce que tu as déjà fait est utile, mais va t'entraver dans la reprise.

Les classes sont normalement conçues pour leur comportement (commenté), pas leur code.

Tu devrais a priori avoir

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
class problem {
private:
    ...
public:
    problem();
 
    void add(clause const&);
    void simplify();
 
    //true if affectation is solution of this problem
    bool isSolution(affectation const&) const;
 
    //return clauses failing under the given affectation
    errors asSolution(affectation const&) const;
    bool hasSolution() const;
};

En choisissant ou créant un type pratique pour affectation et clause.

[isangoma]

C'est une solution oui

[ternel]

Je me suis un peu amusé, j'ai recodé l'ensemble, en séparant en plusieurs fichiers.
Ca manque d'un passage au compilateur, mais au boulot je n'ai qu'un pauvre gcc 4.1;
Ca manque aussi de test, mais ca devrait être plus simple.

tout d'abord, le traitement souhaité:

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
#include <iostream>
 
#include "problem.hpp"
 
void flipRandomClause(logika::affectation & affectation, logika::problem::solution_errors const& errors) {
	bool that& = affectation.at(rand()%errors.size());
	that = ! that;
}
 
bool papadimitriou(logika::problem const& prob) {
 
	auto steps = prob.variables().size();
 
	for (int k = 0; k < log2(steps); k++) {
		std::cout << k << std::endl;
 
		logika::affectation affectation = logika::affectation(prob.variables());
 
		for (int j = 0; j < 2*steps*steps; ++j) {
			auto errors = prob.asSolution(affectation);
			if (errors.empty()) {
				return true;
			}
 
			flipRandomClause(affectation, errors);
		}
	}
	return false;
}
 
 
 
 
void test(const char* filename) {
	problem prob = parse(file);
	prob.simplify();
	std::cout << "le probleme " << file << (papadimitriou(prob) ? " est" : " n'est pas") << " solvable." << std::endl;
}
 
int main(int argc, char* argv[]) {
	if (argc >1) {
		for (int i = 1; i < argc; ++i) {
			test(argv[i]);
		}
		return 0;
	}
 
	const char* files[]={
		"2sat1.txt",
		"2sat2.txt",
		"2sat3.txt",
		"2sat4.txt",
		"2sat5.txt",
		"2sat6.txt",
	};
 
	for (auto file : files) {
		test(file);
	}
	return 0;
}

puis l'en-tête du code effectif:

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
#ifndef PROBLEM_H_INCLUDED
#define PROBLEM_H_INCLUDED 1
 
#include <string>
#include <map>
#incldue <vector>
#include <set>
 
#include <cmath>
#include <iosfwd>
 
namespace logika {
 
using id_t = long int;
 
using affectation = std::map<id_t, bool>;
 
class clause {
private:
	id_t a;
	id_t b;
	bool notA;
	bool notB;
public:
	clause(id_t left, id_t right): 
		a(abs(left)), b(abs(right)),
		notA(left<0), notB(right<0)
		{}
 
	id_t left() const {return a;}
	id_t right() const {return b;}
 
	bool leftNegated() const {return notA;}
	bool rightNegated() const {return notB;}
 
	//might throw std::out_of_range
	bool eval(affectation const& affectation) const;
};
 
std::ostream& operator<<(std::ostream&, clause const&);
 
 
class problem {
public:
	typedef id_t clause_id;
private:
	std::set<id_t> vars;
	typedef std::map<clause_id, clause> clauses_type;
 
	typedef std::multimap<id_t, clause_id> dependency_map;
 
	clauses_type clauses;
	dependency_map claims, negations;
 
	clause_id last_clause_id;
public:
	problem() : last_clause_id(0){}
 
	//construction
	void add(clause const&);
 
	//simplifying
public:
	void simplify();
 
private:
	std::pair<id_t, bool> simplifiableVar() const;
 
public:
	std::set<id_t> const& variables() const {return vars;}
 
	clause const& operator()(clause_id id) const{
		return clauses.at(id);
	}
 
	clause& operator()(clause_id id) {
		return clauses.at(id);
	}
 
	typedef clauses_type::const_iterator const_iterator;
	const_iterator begin() const {return clauses.begin();}
	const_iterator end() const {return clauses.end();}
 
	//affectation operations might throw std::out_of_range, see clause.eval()
 
    //true if affectation is solution of this problem
    bool isSolution(affectation const&) const;
 
	typedef std::vector<clause_id> solution_errors;
 
    //returns the clauses failing under the given affectation
    solution_errors asSolution(affectation const&) const;
 
 
 
 
};
 
std::ostream& operator<<(std::ostream&, problem const&);
 
problem parse(const char* filename);
 
 
}//logika::
#endif

et enfin, l'implémentation:

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
#include "problem.hpp"
 
#include <string>
#include <map>
#incldue <vector>
#include <list>
#include <set>
 
#include <cmath>
 
#include <iostream>
#include <sstream>
 
#include <utility>
#include <algorithm>
#include <ctime>
 
 
namespace logika {
 
bool clause::eval(affectation const& affectation) const {
	bool A = affectation.at(a);
	bool B = affectation.at(b);
	return (notA ? !A : A) || (notB ? !B : B);
}
 
 
std::ostream& operator<<(std::ostream& os, clause const& c) {
	return os << (c.leftNegated() ? '!' : ' ') << c.left() << " ou "<< (c.rightNegated() ? '!' : ' ') << c.right();
}
 
 
void problem::add(clause const& clause) {
    clause_id id = ++last_clause_id;
	clauses.emplace(id, clause);
 
	vars.add(clause.left());
	vars.add(clause.right());
 
	(clause.leftNegated() ? negations : claims) .emplace(clause.left(), id);
	(clause.rightNegated() ? negations : claims) .emplace(clause.right(), id);
}
 
/*
	if exists X where not exists !X, remove X and any clause about X
	if exists !X where not exists X, remove !X and any clause about !X
*/
 
void problem::simplify() {
	std::pair<id_t, bool> s;
	while ((s = simplifiableVar()).first!=-1) {
		if (s.second) {
			auto those = claims.equal_range(s.first);
			for(auto it = those.first; it!=those.second; ++it) {
				clauses.erase(it->first);
			}
			claims.erase(those.first, those.second);
		}
	}
}
 
namespace {
id_t pick(problem::dependency_map const& source, problem::dependency_map const& checks) {
	for (dependency_map::iterator it = source.begin(), end = source.end(); it != end; it = source.upper_bound(it->first)) {
		const id_t var = it->first;
		if (checks.find(var)==checks.end()) {
			return var;
		}
	}
	return -1;
}
 
}//::
 
std::pair<id_t, bool> problem::simplifiableVar() const {
	const id_t id = pick(claims, negates);
	if (id!=-1) {
		return std::make_pair(id, true);
	}
	return std::make_pair(pick(negates, claims), false);
}
 
std::ostream& operator<<(std::ostream& os, problem const& p) {
	for(auto const& that : p) {
		os << (that.second) << '\n';
	}
	return os;
}
 
 
affectation affectation(std::set<id_t> const & vars) {
	affectation values;
	for (id_t id : vars) {
		values.emplace(id, rand()%2==0);
	}
	return values;
}
 
//true if affectation is solution of this problem
bool problem::isSolution(affectation const& affectation) const {
	for (auto it = begin(); it!=end(); ++it) {
		!(it->second.eval(affectation) return false;
	}
	return true;
}
 
//return clauses failing under the given affectation
std::vector<clause_id> problem::asSolution(affectation const&) const {
	std::vector<clause_id> errors;
	for (auto it = begin(); it!=end(); ++it) {
		!(it->second.eval(affectation) errors.push_back(it->first);
	}
	return errors;
}
 
 
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;
		prob.inject(var1, var2);
	}
 
	return prob;
}
 
}//logika::

Tu remarqueras l'usage d'un namespace arbitraire (logika, parce que j'ai trouvé ce nom joli)

[JolyLoic]

Ca manque aussi de test, mais ca devrait être plus simple.

Une bonne pratique aurait été d'ajouter les tests avant de faire le refactoring. (je ne parle pas pour leternel, qui fait ça pour s'amuser, mais plus pour le posteur initial).

[ternel]

Je l'ai surtout fait loin de tout compilateur... ça me rappelle le temps des examens de C++, à la fac
J'avoue que la testabilité est importante, très importante

[ImmoTPA]

J'ai étudié ton code leternel et si ça ne t'ennuie pas je t'ai laissé comme la dernière fois quelques questions dans le code. Par ailleurs avec quoi dois-je compiler le fichier parce que pour l'instant j'ai quelques erreurs à la compilation (j'ai compilé avec g++ -Wall -std=c++11 main.cpp problem.cpp -o papa)
?

Je te remercie encore une fois énormément pour l'effort que tu as fait . Par ailleurs j'ai pu corrigé quelques erreurs (notamment un typedef qui était private, un include oublié des logika:: ou problem:: oubliés etc...) La plupart des erreurs qu'il reste sont liées aux questions que je t'ai posé donc je n'ose pas trop y toucher tant que tu ne m'auras pas expliqué ce qu'il en est.

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
#include <iostream>
 
#include "problem.hpp"
 
void flipRandomClause(logika::affectation & affectation, logika::problem::solution_errors const& errors) {
	bool that& = affectation.at(rand()%errors.size());   // bool that& ça crée une référence sur une variable booléenne ? est ce que c'est pour modifier that et non une copie ? 
	that = ! that;
}
 
bool papadimitriou(logika::problem const& prob) {
 
	auto steps = prob.variables().size();
 
	for (int k = 0; k < log2(steps); k++) {
		std::cout << k << std::endl;
 
		logika::affectation affectation = logika::affectation(prob.variables());
 
		for (size_t j = 0; j < 2*steps*steps; ++j) {
			auto errors = prob.asSolution(affectation);
			if (errors.empty()) {
				return true;
			}
 
			flipRandomClause(affectation, errors);
		}
	}
	return false;
}
 
 
 
 
void test(const char* filename) {
	logika::problem prob = logika::parse(filename);
	prob.simplify();
	std::cout << "le probleme " << filename << (papadimitriou(prob) ? " est" : " n'est pas") << " solvable." << std::endl; // syntaxe marrante dont je déduis le sens mais
																												// si tu peux l'expliquer en une ptite phrase ça serait vraiment super
}
 
int main(int argc, char* argv[]) {
	if (argc >1) {
		for (int i = 1; i < argc; ++i) {
			test(argv[i]);
		}
		return 0;
	}
 
	const char* files[]={
		"2sat1.txt",
		"2sat2.txt",
		"2sat3.txt",
		"2sat4.txt",
		"2sat5.txt",
		"2sat6.txt",
	};
 
	for (auto file : files) {
		test(file);
	}
	return 0;
}
 
//encore un grand merci pour ton travail.

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
#ifndef PROBLEM_H_INCLUDED
#define PROBLEM_H_INCLUDED 
 
#include <string>
#include <map>
#include <vector>
#include <set>
 
#include <cmath>
#include <iosfwd>
 
namespace logika {
 
using id_t = long int; // la dernière fois cette ligne m'a empeché de compiler probablement pareil ici, j'avais mis using id_t_ = long int pour résoudre
 
using affectation = std::map<id_t, bool>;
 
class clause {
private:
	id_t a;
	id_t b;
	bool notA;
	bool notB;
public:
	clause(id_t left, id_t right): 
		a(abs(left)), b(abs(right)),
		notA(left<0), notB(right<0)
		{}
 
	id_t left() const {return a;}
	id_t right() const {return b;}
 
	bool leftNegated() const {return notA;}
	bool rightNegated() const {return notB;}
 
	//might throw std::out_of_range
	bool eval(affectation const& affectation) const;
};
 
std::ostream& operator<<(std::ostream&, clause const&);
 
 
class problem {
public:
	typedef id_t clause_id;
	typedef std::multimap<id_t, clause_id> dependency_map;
private:
	std::set<id_t> vars;
	typedef std::map<clause_id, clause> clauses_type;
 
 
 
	clauses_type clauses;
	dependency_map claims, negations;
 
	clause_id last_clause_id;           
public:
	problem() : last_clause_id(0){}
 
	//construction
	void add(clause const&);
 
	//simplifying
public:
	void simplify();
 
private:
	std::pair<id_t, bool> simplifiableVar() const;     
 
public:
	std::set<id_t> const& variables() const {return vars;}
 
	clause const& operator()(clause_id id) const{                 // récupérer une clause quand on connait une variable impliquée ? 
		return clauses.at(id);
	}
 
	clause& operator()(clause_id id) {                      // pareil mais on récupère une référence sur la clause ? A quoi ça peut bien servir ? 
		return clauses.at(id);
	}
 
	typedef clauses_type::const_iterator const_iterator;
	const_iterator begin() const {return clauses.begin();}
	const_iterator end() const {return clauses.end();}
 
	//affectation operations might throw std::out_of_range, see clause.eval()        
 
    //true if affectation is solution of this problem
    bool isSolution(affectation const&) const;
 
	typedef std::vector<clause_id> solution_errors;                            // stratégiquement tu choisis de renvoyer une liste de variables et non une liste de clauses si je comprends bien
 
    //returns the clauses failing under the given affectation                  //clause_id c'est un alias de id_t, comment cela pourrait-il renvoyer un vector de clauses ? 
    solution_errors asSolution(affectation const&) const;
 
 
 
 
};
 
std::ostream& operator<<(std::ostream&, problem const&);
 
problem parse(const char* filename);
 
 
}//logika::             // t'es doué pour trouver des noms classes Oo
#endif

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
 
#include <iostream>
#include <sstream>
 
#include <utility>
#include <algorithm>
#include <ctime>
 
#include <fstream>
 
 
namespace logika {
 
bool clause::eval(affectation const& affectation) const {
	bool A = affectation.at(a);
	bool B = affectation.at(b);
	return (notA ? !A : A) || (notB ? !B : B);        // je me rappelle avoir vu la notation il y a longtemps mais ...
}
 
 
std::ostream& operator<<(std::ostream& os, clause const& c) {
	return os << (c.leftNegated() ? '!' : ' ') << c.left() << " ou "<< (c.rightNegated() ? '!' : ' ') << c.right();
}
 
 
void problem::add(clause const& clause) {
    clause_id id = ++last_clause_id;           //pour garder trace de la taille du problem ou il y a autre chose ? 
	clauses.emplace(id, clause);
 
	vars.insert(clause.left());
	vars.insert(clause.right());
 
	(clause.leftNegated() ? negations : claims) .emplace(clause.left(), id);      // je ne comprends pas les deux lignes mais j'ai l'impression que ta syntaxe remplace une
	(clause.rightNegated() ? negations : claims) .emplace(clause.right(), id);    // espèce de if
}
 
/*
	if exists X where not exists !X, remove X and any clause about X                // euh en fait on remove toutes les clauses relatives à X dans les deux cas, que ce soit
	if exists !X where not exists X, remove !X and any clause about !X             // celles qui contiennent X ou !X
*/
 
void problem::simplify() {
	std::pair<id_t, bool> s;
	while ((s = simplifiableVar()).first!=-1) {
		if (s.second) {
			auto those = claims.equal_range(s.first);
			for(auto it = those.first; it!=those.second; ++it) {
				clauses.erase(it->first);
			}
			claims.erase(those.first, those.second);
		}
	}
}
 
namespace { // normal que le namespace n'ait pas de nom ? 
id_t pick(problem::dependency_map const& source, problem::dependency_map const& checks) {
	for (problem::dependency_map::iterator it = source.begin(), end = source.end(); it != end; it = source.upper_bound(it->first)) { // j'ai trouvé ce que faisait upper_bound,
		const id_t var = it->first; 																						// mais pk pas juste ++it ?
		if (checks.find(var)==checks.end()) { // j'ai du mal à voir c'est quoi exactement source et checks, une dependency_map c'est std::multimap<id_t, clause_id>
			return var;						 // ou std::multimap<long int, long int> donc contient probablement les id des deux variables d'une clause si j'ai compris
		}
	}
	return -1;
}                        // désolé mais au final je ne comprends pas à quoi sert la fonction, checks.find(var)==checks.end() ça veut dire que var n'est pas dans checks
 						// mais je ne vois pas ce que tu comptes faire de la var
}//::
 
std::pair<id_t, bool> problem::simplifiableVar() const {
	const id_t id = pick(claims, negations);
	if (id!=-1) {
		return std::make_pair(id, true);   // n'ayant pas compris l'utilité de pick je ne suis pas certain de celle de simplifiableVar non plus
	}
	return std::make_pair(pick(negations, claims), false);
}
 
std::ostream& operator<<(std::ostream& os, problem const& p) {
	for(auto const& that : p) {
		os << (that.second) << '\n';
	}
	return os;
}
 
 
affectation affectation(std::set<id_t> const & vars) {
	affectation values;
	for (id_t id : vars) {
		values.emplace(id, rand()%2==0);    // là tu crées un random assignment !
	}
	return values;
}
 
//true if affectation is solution of this problem
bool problem::isSolution(affectation const& affectation) const {
	for (auto it = begin(); it!=end(); ++it) {
		!(it->second.eval(affectation)) return false;   // euh je ne comprends pas non plus désolé, tu as pas mis le if ? 
	}
	return true;
}
 
//return clauses failing under the given affectation
std::vector<problem::clause_id> problem::asSolution(affectation const&) const {
	std::vector<clause_id> errors;
	for (auto it = begin(); it!=end(); ++it) {
		!(it->second.eval(affectation) errors.push_back(it->first); // pareil que celui d'avant, normal que ta parenthèse ne se ferme pas ? (pareil pour problem::isSolution)
	}
	return errors;
}
 
 
problem parse(const char* filename) {
	problem prob;
 
	std::string line;
	std::ifstream fichier(filename, std::ios::in);
 
	getline(fichier, line);
 
	while(std::getline(fichier, line)){
		std::istringstream iss(line);
 
		long int var1, var2;
 
		iss >> var1 >> var2;
		prob.inject(var1, var2);
	}
 
	return prob;
}
 
}//logika::

[ternel]

Pour les erreurs de compilation, c'est sûr qu'il y en a.
Je ne suis pas capable de pondre 300 lignes sans erreurs.
En écoutant le compilateur, ca devrait être simple de les corriger

Un point qui te chiffonne sur la syntaxe: l'opérateur ternaire, c'est à dire a ? b : c.
Petite introduction:
1 + 2 est une expression composite, constituée ainsi:

• l'expression 1, qui est la constante entière 1 (de type signed int)
• l'expression 2, sur le même principe
• l'opérateur +, qui prend deux expressions comme opérandes, et s'évalue comme la somme dont il est la notation

Cette expression 1 + 2 à pour valeur 3;
En tant qu'expression, je peux l'utiliser partout où j'attends une valeur:

• a = 1 + 2
• f(1 + 2)
• -(1 + 2)

En résumé, une expression est une valeur fixe ou calculée, utilisable dans une autre expression.

Le ternaire est construit sur le même principe:
? : prends trois opérandes, et s'évalue ainsi: condition ? si_vrai : si_faux vaut si condition est vrai, si_vrai, sinon si_faux.

Ca se passe comme si on avait une fonction test telle que:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
template<typename T>
T test(bool a, T b, T c) {
	if (a) {
		return b;
	} else {
		return c;
	}
}

a ? b : c est équivalent à test(a, b, c).
L'avantage, c'est que c'est une expression, il n'y a pas de cout d'appel d'une fonction.
Et ce n'est pas non plus une instruction, donc on peut l'appeler dans une expression.
En effet, on ne peut pas écrire string message = (if(condition) "vrai" else "faux");.

Pour information, condition est une expression évaluée comme un booléen: un entier est vrai si non nul, tout comme les pointeurs nus différents de null.
Par ailleurs, si_vrai et si_faux sont deux expressions qui doivent être du même type.


Passons à tes questions:
Je m'excuse, j'ai fait quelques fautes de logique, plus ou moins importante.

Commençons par l'en-tête.
pour id_t, il doit y avoir un type tordu que j'ignore.
comme c'est dans un namespace particulier, ca ne devrait pas poser de problème.
Sinon, change le complètement par variable_id ou variable_id_type

Dans la partie construction de problem:
Ma première erreur:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

typedef id_t clause_id;

Ici, j'aurai dû écrire typedef long clause_id; (car long est long int). En effet, il n'y a aucun lien sémantique entre variable_id et clause_id. Ils sont juste le même type.
Cela t'a induit en erreur.

Cela répond à plusieurs questions:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
	clause const& operator()(clause_id id) const{
		// récupérer une clause quand on connait une variable impliquée ?
		return clauses.at(id);
	}
 
	clause& operator()(clause_id id) {
		// pareil mais on récupère une référence sur la clause ? A quoi ça peut bien servir ?
		return clauses.at(id);
	}

Le premier est un accesseur constant à une clause (via son id). Ca sert pour l'affichage
Le second est l'accesseur non-constant correspondant. Ca pourrait permettre de modifier la clause.
Ce second accesseur n'est pas utilisable sur une variable constante (vu que la fonction n'est pas const)

Tu remarqueras les signatures:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
valeur & get(cle const&);//accesseur modifiant
valeur const& get(cle const&) const;//accesseur constant. ici, le const& sur la valeur n'est pas forcément requis, si valeur est un type constant

Tu as la même chose avec les itérateurs de vector:
vector::begin() retourne un iterator, tandis que vector::begin() const retourne un const_iterator


Dans la partie utilisation:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
typedef std::vector<clause_id> solution_errors;
	// stratégiquement tu choisis de renvoyer une liste de variables et non une liste de clauses si je comprends bien
 
    //returns the clauses failing under the given affectation
	//clause_id c'est un alias de id_t, comment cela pourrait-il renvoyer un vector de clauses ?
    solution_errors asSolution(affectation const&) const;

Non non, c'est bien une liste d'identifiants de clause. Encore une fois, désolé de t'avoir perturbé avec le typedef.

Pour problem.cpp

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
bool clause::eval(affectation const& affectation) const {
	bool A = affectation.at(a);
	bool B = affectation.at(b);
	return (notA ? !A : A) || (notB ? !B : B);        // je me rappelle avoir vu la notation il y a longtemps mais ...
}

Voici deux applications du ternaire.
j'aurai pu jouer avec les opérateurs logiques, mais c'a n'aurait pas été plus clair.

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
void problem::add(clause const& clause) {
    clause_id id = ++last_clause_id;           //pour garder trace de la taille du problem ou il y a autre chose ?
	clauses.emplace(id, clause);
 
	vars.insert(clause.left());
	vars.insert(clause.right());
 
	(clause.leftNegated() ? negations : claims) .emplace(clause.left(), id);      // je ne comprends pas les deux lignes mais j'ai l'impression que ta syntaxe remplace une
	(clause.rightNegated() ? negations : claims) .emplace(clause.right(), id);    // espèce de if
}

Pour l'identifiant, c'est parce qu'on pourrait supprimer des clauses, puis en ajouter. et qu'on ne veut pas qu'un identifiant soit utilisé deux fois.
Là encore, j'ai utilisé le ternaire, pour sa faculté d'être une expression.
Sans lui, j'aurai dû écrire ceci:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
if (clause.leftNegated) {
	negations.emplace(clause.left(), id);
} else {
	claims.emplace(clause.left(), id);
}
if (clause.rightNegated) {
	negations.emplace(clause.right(), id);
} else {
	claims.emplace(clause.right(), id);
}

Ce qui est moins lisible, car ca augmente le rapport (code technique) / (code métier)
j'aurai aussi pu écrire

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
dependency_map& lefty = (clause.leftNegated() ? negations : claims);
dependency_map& righty = (clause.rightNegated() ? negations : claims);
lefty.emplace(clause.left(), id);
righty.emplace(clause.right(), id);

Question suivante: (un commentaire de commentaire, j'aime bien )

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
/*
	if exists X where not exists !X, remove X and any clause about X
	if exists !X where not exists X, remove !X and any clause about !X
*/
// euh en fait on remove toutes les clauses relatives à X dans les deux cas, que ce soit celles qui contiennent X ou !X

Pas tout à fait, on ne supprime pas les clauses de la même sous-map (claims ou negations). Mais c'est vrai que les clauses sont completement supprimées.
Du moins, c'est ce que faisait ton code.

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
namespace { // normal que le namespace n'ait pas de nom ?
id_t pick(problem::dependency_map const& source, problem::dependency_map const& checks) {
	for (problem::dependency_map::iterator it = source.begin(), end = source.end(); it != end; it = source.upper_bound(it->first)) { // j'ai trouvé ce que faisait upper_bound,
		const id_t var = it->first; 																						// mais pk pas juste ++it ?
		if (checks.find(var)==checks.end()) { // j'ai du mal à voir c'est quoi exactement source et checks, une dependency_map c'est std::multimap<id_t, clause_id>
			return var;						 // ou std::multimap<long int, long int> donc contient probablement les id des deux variables d'une clause si j'ai compris
		}
	}
	return -1;
}                        // désolé mais au final je ne comprends pas à quoi sert la fonction, checks.find(var)==checks.end() ça veut dire que var n'est pas dans checks
 						// mais je ne vois pas ce que tu comptes faire de la var
}//::

un namespace sans nom (anonyme) est un namespace visible uniquement dans l'unité de compilation locale, en l'occurence pick() est garanti de ne pas entrer en conflit avec d'autres fonctions. C'est un peu l'équivalent d'une fonction static en C. On doit avoir une faq la dessus.

Pour le reste, j'aurai dû mettre des commentaires, et j'en dirai plus dans mon prochain post.

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
 
affectation affectation(std::set<id_t> const & vars) {
	affectation values;
	for (id_t id : vars) {
		values.emplace(id, rand()%2==0);    // là tu crées un random assignment !
	}
	return values;
}

Précisément. J'ai juste oublié de mettre un commentaire le disant.
cette fonction crée un assignement aléatoire pour chaque identifiant de variable de l'argument.
C'est exactement ce que faisait ta fonction problem::initialize().
Sauf que ca n'avait rien à voir avec problem, vu que ce n'est pas lui que tu initialises.

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
bool problem::isSolution(affectation const& affectation) const {
	for (auto it = begin(); it!=end(); ++it) {
		!(it->second.eval(affectation)) return false;   // euh je ne comprends pas non plus désolé, tu as pas mis le if ?
	}
	return true;
}

Oups, il faut le rajouter: if (!(it->second.eval(affectation))) return false;.
On va mettre ça sur le coup de la fatigue. J'espère que le compilateur hurle de douleur, le pauvre.

enfin, le main

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
namespace logika {
using affectation = std::map<id_t, bool>;
}
void flipRandomClause(logika::affectation & affectation, logika::problem::solution_errors const& errors) {
	bool that& = affectation.at(rand()%errors.size());
	that = ! that;
}

Ça, c'est une astuce, pas forcément bienvenue dans un exemple, pour ne pas indexer deux fois la map.
En fait, il y a une erreur de logique, l'index cherché n'est pas le bon.

J'aurai dû faire ainsi:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
void flipRandomClause(logika::affectation & affectation, logika::problem::solution_errors const& errors, logika::problem const& problem) {
	logika::clause const& clause = problem(errors[rand()%errors.size()]);//une clause au hasard.
	logika::variable_id var = ( rand()%2 ? clause.left() : clause.right() );
	bool that& = affectation.at(var);
	that = ! that;
}

Comme affectation est une référence non-constante vers une map, sa fonction at() retourne une référence modifiable.
en moins efficace, les deux dernière lignes aurait pu être remplacées par affectation.at(var) = ! affectation.at(var);.
Voire même, en sacrifiant le controle de validité, affectation[var]= ! affectation[var];.
Cette syntaxe ne t'aurait pas dérangé, mais on y perdrait deux choses:
on passerait deux fois plus de temps à chercher la variable, et on devrait controler nous-même la validité.

[ternel]

Passons au problème d'algorithme.

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
/*
	if exists X where not exists !X, remove X and any clause about X
	if exists !X where not exists X, remove !X and any clause about !X
*/
 
void problem::simplify() {
	std::pair<variable_id, bool> s;
	while ((s = simplifiableVar()).first!=-1) {
		if (s.second) {
			auto those = claims.equal_range(s.first);
			for(auto it = those.first; it!=those.second; ++it) {
				clauses.erase(it->first);
			}
			claims.erase(those.first, those.second);
		}
	}
}
 
namespace { // normal que le namespace n'ait pas de nom ?
variable_id pick(problem::dependency_map const& source, problem::dependency_map const& checks) {
	for (problem::dependency_map::iterator it = source.begin(), end = source.end(); it != end; it = source.upper_bound(it->first)) { // j'ai trouvé ce que faisait upper_bound,
		const variable_id var = it->first; 																						// mais pk pas juste ++it ?
		if (checks.find(var)==checks.end()) { // j'ai du mal à voir c'est quoi exactement source et checks, une dependency_map c'est std::multimap<variable_id, clause_id>
			return var;						 // ou std::multimap<long int, long int> donc contient probablement les id des deux variables d'une clause si j'ai compris
		}
	}
	return -1;
}                        // désolé mais au final je ne comprends pas à quoi sert la fonction, checks.find(var)==checks.end() ça veut dire que var n'est pas dans checks
 						// mais je ne vois pas ce que tu comptes faire de la var
}//::
 
std::pair<variable_id, bool> problem::simplifiableVar() const {
	const variable_id id = pick(claims, negations);
	if (id!=-1) {
		return std::make_pair(id, true);   // n'ayant pas compris l'utilité de pick je ne suis pas certain de celle de simplifiableVar non plus
	}
	return std::make_pair(pick(negations, claims), false);
}

Voici un problème d'un autre niveau.
Ce n'est pas vraiment le C++ qui te pose problème, mais mon absence de commentaire de développement.
Je vais donc prendre le temps de t'expliquer comment j'ai fait, car le résultat n'importe pas autant que la manière.


J'ai pris le parti de ne pas inclure dans les variables membres de problem le nécessaire à sa simplification.
En effet c'est un détail d'implémentation particulièrement inutile.
Je n'ai pas envie de recompiler les fichiers incluant problem.hpp juste parce que je change le code de problem::simplify().

Pour l'implémentation, j'ai suivi le principe qu'une fonction ne doit faire qu'une série d'actions atomiques

Voici ce que j'avais écrit avant de coder:

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
/*
	if exists X where not exists !X, remove X and any clause about X
	if exists !X where not exists X, remove !X and any clause about !X
*/
void problem::simplify() {
	while exists var v simplifiable {
		if v is claimed {
			remove all claims about v
				both as clause
				and as claim
		} else {
			remove all negations about v
				both as clause
				and as negation
		}
	}
}

Ce en quoi, j'ai oublié un morceau de code.
J'aurai du écrire:

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
void problem::simplify() {
	//while exists var v simplifiable {
	std::pair<variable_id, bool> var;//v et (true si v est une claim, false sinon)
	while ((var = simplifiableVar()).first!=-1) {
		//if v is claimed {
		if (var.second) {
			//remove all claims about v
			//	"all about v"
			auto those = claims.equal_range(var.first);
			for(auto it = those.first; it!=those.second; ++it) {
				//both as clause
				clauses.erase(it->first);
			}
			//	and as claim
			claims.erase(those.first, those.second);
		} else {
			//remove all negations about v
			//	"all about v"
			auto those = negations.equal_range(var.first);
			for(auto it = those.first; it!=those.second; ++it) {
				//both as clause
				clauses.erase(it->first);
			}
			//	and as negation
			negations.erase(those.first, those.second);
		}
	}
}

Je m'apercois qu'un ternaire serait utile, parce que je déteste le copié collé

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
/*
	if exists X where not exists !X, remove X and any clause about X
	if exists !X where not exists X, remove !X and any clause about !X
*/
void problem::simplify() {
	while exists var v simplifiable {
		remove all {claims if v is a claim, negations otherwise} about v
			both as clause
			and as {claims if v is a claim, negations otherwise}
	}
}

ou avec un ternaire pour ne pas copier coller, parce qu'il ne faut jamais le faire:

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
void problem::simplify() {
	//while exists var v simplifiable {
	std::pair<variable_id, bool> var;//v et (true si v est une claim, false sinon)
	while ((var = simplifiableVar()).first!=-1) {
 
		//remove all (v is claim ? claims : negations) about v
		dependency_map & map = var.second ? claims : negations;
		//	"all about v"
		auto those = map.equal_range(var.first);
		//	both as clause
		for(auto it = those.first; it!=those.second; ++it) {
			clauses.erase(it->first);
		}
		//and as (v is claim ? claim : negation)
		map.erase(those.first, those.second);
	}
}

J'ai poussé le problème à un sous problème: maintenant, si je sais trouvé une variable simplifiable, je sais simplifier le problème. Cela s'appelle la stratégie diviser pour régner.
J'ai donc supposé la fonction simplifiableVar, qui me renvoie trois informations simultanéement:

• s'il existe une telle variable
• l'identifiant de cette variable
• un booléen indiquant si c'était une variable affirmée ou niée.

J'ai représenté ça en retournant une pair<id, bool>, profitant de ce que l'identifiant est positif pour représenter l'inexistence par -1.

Pour la coder, j'ai constaté qu'il fallait chercher une variable affirmée non niée, ou niée non affirmée

Au début, j'ai envisagé de créer une structure de donnée simplifiant la recherche, à base de compteurs de négation et d'affirmation pour chaque variable.
Sauf que je n'ai pas trouver de moyen simple d'ajouter et mettre à jour ce bazar. Donc j'ai cherché un méthode sans contenu supplémentaire.

Pour chercher une variable affirmée non niée, je procède naturellement ainsi:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
pour chaque variable affirmée
	si elle n'est pas niée je la retourne.
au pire je retourne tant pis.

Sauf qu'une multimap n'est pas itérable directement par clé.
L'itérateur se réfère aux valeurs, et son ++ de l'itérateur parcourt successivement toutes les valeurs de chaque clé.

Ainsi, on peut utiliser upper_bound() pour récupérer un itérateur sur la première valeur dont la clé est supérieure à la clé actuellement sous l'itérateur. C'est utile.


Supposons que j'ai la multimap map = { {1, "a1"} {1, "a2"} {2, "b1"} {2, "b2"} {2, "b2"} {3, "c"} {4, "d"} }.
La boucle for (auto it = map.begin(), end = map.end(); it != end; it = map.upper_bound(it->first)) va itérer successivement sur :

1. {1, "a1"}
2. {2, "b1"}
3. {3, "c"}
4. {4, "d"}

Du coup, it->first parcoure bien les clés de la multimap.

passons à ma fonction, elle doit parcourir les deux maps, et retourner n'importe quelle clé qui est dans l'une mais pas dans l'autre, ainsi qu'un booléen disant dans laquelle je l'ai trouvée.

Il y a plusieurs solutions:
Par exemple, constituer un set des clés, puis chercher une bonne.
Sauf que pour le faire, il faut parcourir chaque maps, puis le set en indexant les deux maps pour chaque clé.
La complexité est de l'ordre de Naffirmations + Nnégations + NVar*(log2(Naffirmations)+log2(Nnégations)).

Je peux aussi parcourir d'abord les variables affirmées et pour chacune, cherchée si elle est niée, puis, si je n'ai rien, recommencer dans l'autre ordre.
La complexité est Naffirmations*log2(Nnégations) + Nnégations*(log2(Naffirmations)).

Sur un problème équilibré, j'ai le choix entre NVar + NVar*2*log2(NVar/2) et (Nvar/2)*log2(Nvar/2) + (Nvar/2)*log2(Nvar/2) = Nvar*log2(Nvar/2)Sur un problème avec extrème (que des affirmations), j'ai le choix entre
Naffirmations + 0 + Naffirmations*(log2(Naffirmations)) = Naffirmations + Nclaimed*(log2(Naffirmations)) et Naffirmations*1 + 1*log2(Naffirmations)) = Naffirmations + log2(Naffirmations))Le premier algo est entre N + 2 N logN et N + N log N, le second entre N log N et N + log N qui est inférieur à 2*N
Le choix est simple: le second algo.
J'estime que N log N est assez bon pour cherche une variable dans un espace NxN. Surtout avec une tendance au N.

Je sais où je vais, je peux me rapprocher de mon code:

Je peux parcourir d'abord les variables affirmées et pour chacune, cherchée si elle est niée, puis, si je n'ai rien, recommencer dans l'autre ordre.

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
std::pair<variable_id, bool> problem::simplifiableVar() const {
	for each claimed variable var
		if var is not negated return {var, true}
	for each negated variable var
		if var is not claimed return {var, false}
	return {-1, any}
}

Parce que je déteste toujours autant dupliquer du code, je crée une fonction intermédiaire: pick

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
std::pair<variable_id, bool> pick(???) {
	for each <claimed|negated> variable var
		if var is not <negated|claimed> return {var, <claimed ? true : false> }
	return {-1, <claimed ? true : false> }
}
std::pair<variable_id, bool> problem::simplifiableVar() const {
	auto that = pick(claims);
	if (that.first != -1) return that;
	that = pick(negations);
	if (that.first != -1) return that;
	return {-1, false};//ou true, c'est pareil
}

Tu remarqueras que pour les negations si, that.first est -1 on retourne "un autre" -1.
C'est inutile, autant supprimer le test.

Par contre, je n'ai pas envie de créer la paire dans pick.

En raffinant un peu, j'obtiens donc:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
std::pair<variable_id, bool> problem::simplifiableVar() const {
	variable_id var = pick(claims, negations);
	if (var != -1) return {var, true};
 
	return {pick(negations, claims), false};
}
 
variable_id pick(? <claimed|negated>, ? <negated|claimed>) {
	for each variable var in <claimed|negated>
		if var is not in <negated|claimed> return var
	return -1;
}

Le travail est quasiment fait, il ne reste qu'à trouver des noms valides et à parcourir efficacement les maps.
J'ai donc finalement le code suivant:

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
/*
	if exists X where not exists !X, remove X and any clause about X
	if exists !X where not exists X, remove !X and any clause about !X
*/
void problem::simplify() {
	std::pair<variable_id, bool> var;
	while ((var = simplifiableVar()).first!=-1) {
		dependency_map & map = var.second ? claims : negations;
 
		auto those = map.equal_range(var.first);
		for(auto it = those.first; it!=those.second; ++it) {
			clauses.erase(it->first);
		}
		map.erase(those.first, those.second);
	}
}
 
namespace {
//returns a key from source which is absent from checks. Or -1 if such key does not exist.
variable_id pick(problem::dependency_map const& source, problem::dependency_map const& checks) {
	//for each variable var in source
	for (auto it = source.begin(), end = source.end(); it != end; it = source.upper_bound(it->first)) {
		const variable_id var = it->first;
		//if var is not in checks return var
		if (checks.find(var)==checks.end()) [
			return var;
		}
	}
	return -1;
}
}
 
std::pair<variable_id, bool> problem::simplifiableVar() const {
	const variable_id var = pick(claims, negations);
	if (var != -1) {
		return std::make_pair(var, true);
	}
	return std::make_pair(pick(negations, claims), false);
}

Et voila, c'est ainsi que j'ai réfléchi et codé.

Après, j'ai supprimé les commentaires ligne à ligne, parce qu'il n'ont plus vraiment d'intérêt pour quelqu'un qui connait le langage, et qui à les commentaires de fonctions. Ceux sur simplify() et simplifiableVar() devrait être dans problem.hpp.
Sauf que je ne les ai pas écrit

J'espère que ca t'aidera par la suite.

[ImmoTPA]

Hey leternel, merci beaucoup pour tes commentaires je comprends de mieux en mieux ton code et j'ai pu le faire compiler, je te le post dans l'état.

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
#include <iostream>
 
#include "problem.hpp"
 
void flipRandomClause(logika::affectation & affectation, logika::problem::solution_errors const& errors, logika::problem const& problem) {
	logika::clause const& clause = problem(errors[rand()%errors.size()]);//une clause au hasard.
	logika::variable_id var = ( rand()%2 ? clause.left() : clause.right() );
	//bool that& = affectation.at(var);  // bool that& ça crée une référence sur une variable booléenne ? est ce que c'est pour modifier that et non une copie ? 
	//that = ! that;
	affectation.at(var) = !affectation.at(var);
}
 
bool papadimitriou(logika::problem const& prob) {
 
	auto steps = prob.variables().size();
 
	for (int k = 0; k < log2(steps); k++) {
		std::cout << k << std::endl;
 
		logika::affectation assignment = prob.affectation_assignment(prob.variables());
 
		for (size_t j = 0; j < 2*steps*steps; ++j) {
			auto errors = prob.asSolution(assignment);
			if (errors.empty()) {
				return true;
			}
 
			flipRandomClause(assignment, errors, prob);
		}
	}
	return false;
}
 
 
 
 
void test(const char* filename) {
	logika::problem prob = logika::parse(filename);
	prob.simplify();
	std::cout << "le probleme " << filename << (papadimitriou(prob) ? " est" : " n'est pas") << " solvable." << std::endl; // syntaxe marrante dont je déduis le sens mais
																												// si tu peux l'expliquer en une ptite phrase ça serait vraiment super
}
 
int main(int argc, char* argv[]) {
	if (argc >1) {
		for (int i = 1; i < argc; ++i) {
			test(argv[i]);
		}
		return 0;
	}
 
	const char* files[]={
		"2sat1.txt",
		"2sat2.txt",
		"2sat3.txt",
		"2sat4.txt",
		"2sat5.txt",
		"2sat6.txt",
	};
 
	for (auto file : files) {
		test(file);
	}
	return 0;
}

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
 
#ifndef PROBLEM_H_INCLUDED
#define PROBLEM_H_INCLUDED 
 
#include <string>
#include <map>
#include <vector>
#include <set>
 
#include <cmath>
#include <iosfwd>
 
namespace logika {
 
using variable_id = long int; // la dernière fois cette ligne m'a empeché de compiler probablement pareil ici, j'avais mis using id_t_ = long int pour résoudre
 
using affectation = std::map<variable_id, bool>;
 
class clause {
private:
	variable_id a;
	variable_id b;
	bool notA;
	bool notB;
public:
	clause(variable_id left, variable_id right): 
		a(abs(left)), b(abs(right)),
		notA(left<0), notB(right<0)
		{}
 
	variable_id left() const {return a;}
	variable_id right() const {return b;}
 
	bool leftNegated() const {return notA;}
	bool rightNegated() const {return notB;}
 
	//might throw std::out_of_range
	bool eval(affectation const& affectation) const;
};
 
std::ostream& operator<<(std::ostream&, clause const&);
 
 
class problem {
public:
	typedef long clause_id;
	typedef std::multimap<id_t, clause_id> dependency_map;
private:
	std::set<variable_id> vars;
	typedef std::map<clause_id, clause> clauses_type;
 
 
 
	clauses_type clauses;
	dependency_map claims, negations;
 
	clause_id last_clause_id;           
public:
	problem() : last_clause_id(0){}
 
	//construction
	void add(clause const&);
 
	//simplifying
public:
	void simplify();
 
private:
	std::pair<variable_id, bool> simplifiableVar() const;     
 
public:
	std::set<variable_id> const& variables() const {return vars;}
 
	clause const& operator()(clause_id id) const{                 // récupérer une clause quand on connait une variable impliquée ? // accesseur constant
		return clauses.at(id);
	}
 
	clause& operator()(clause_id id) {                      // pareil mais on récupère une référence sur la clause ? A quoi ça peut bien servir ? // accesseur modifiant
		return clauses.at(id);
	}
 
	typedef clauses_type::const_iterator const_iterator;
	const_iterator begin() const {return clauses.begin();}
	const_iterator end() const {return clauses.end();}
 
	//affectation operations might throw std::out_of_range, see clause.eval()        
 
    //true if affectation is solution of this problem
    bool isSolution(affectation const&) const;
 
	typedef std::vector<clause_id> solution_errors;                            // stratégiquement tu choisis de renvoyer une liste de variables et non une liste de clauses si je comprends bien
 
    //returns the clauses failing under the given affectation                  //clause_id c'est un alias de id_t, comment cela pourrait-il renvoyer un vector de clauses ? 
    solution_errors asSolution(affectation const&) const;
 
 	affectation affectation_assignment(std::set<variable_id> const& vars) const;
 
 
};
 
std::ostream& operator<<(std::ostream&, problem const&);
 
problem parse(const char* filename);
 
 
}//logika::             // t'es doué pour trouver des noms classes Oo
#endif

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
 
#include "problem.hpp"
 
#include <string>
#include <map>
#include <vector>
#include <list>
#include <set>
 
#include <cmath>
 
#include <iostream>
#include <sstream>
 
#include <utility>
#include <algorithm>
#include <ctime>
 
#include <fstream>
 
 
namespace logika {
 
bool clause::eval(affectation const& affectation) const {
	bool A = affectation.at(a);
	bool B = affectation.at(b);
	return (notA ? !A : A) || (notB ? !B : B);        // je me rappelle avoir vu la notation il y a longtemps mais ...
}
 
 
std::ostream& operator<<(std::ostream& os, clause const& c) {
	return os << (c.leftNegated() ? '!' : ' ') << c.left() << " ou "<< (c.rightNegated() ? '!' : ' ') << c.right();
}
 
 
void problem::add(clause const& clause) {
    clause_id id = ++last_clause_id;						           //pour garder trace de la taille du problem ou il y a autre chose ? 
	clauses.insert(std::make_pair(id, clause));
 
	vars.insert(clause.left());
	vars.insert(clause.right());
 
	(clause.leftNegated() ? negations : claims) .insert(std::make_pair(clause.left(), id));      // je ne comprends pas les deux lignes mais j'ai l'impression que ta syntaxe remplace une
	(clause.rightNegated() ? negations : claims) .insert(std::make_pair(clause.right(), id));    // espèce de if
}
 
/*
	if exists X where not exists !X, remove X and any clause about X                // euh en fait on remove toutes les clauses relatives à X dans les deux cas, que ce soit
	if exists !X where not exists X, remove !X and any clause about !X             // celles qui contiennent X ou !X
*/
 
void problem::simplify() {
	//while exists var v simplifiable {
	std::pair<variable_id, bool> var;//v et (true si v est une claim, false sinon)
	while ((var = simplifiableVar()).first!=-1) {
 
		//remove all (v is claim ? claims : negations) about v
		dependency_map & map = var.second ? claims : negations;
		//	"all about v"
		auto those = map.equal_range(var.first);
		//	both as clause
		for(auto it = those.first; it!=those.second; ++it) {
			clauses.erase(it->first);
		}
		//and as (v is claim ? claim : negation)
		map.erase(those.first, those.second);
	}
}
 
namespace { // normal que le namespace n'ait pas de nom ? 
id_t pick(problem::dependency_map const& source, problem::dependency_map const& checks) {
	for (problem::dependency_map::const_iterator it = source.begin(), end = source.end(); it != end; it = source.upper_bound(it->first)) { // j'ai trouvé ce que faisait upper_bound,
		const variable_id var = it->first; 																						// mais pk pas juste ++it ?
		if (checks.find(var)==checks.end()) { // j'ai du mal à voir c'est quoi exactement source et checks, une dependency_map c'est std::multimap<id_t, clause_id>
			return var;						 // ou std::multimap<long int, long int> donc contient probablement les id des deux variables d'une clause si j'ai compris
		}
	}
	return -1;
}                        // désolé mais au final je ne comprends pas à quoi sert la fonction, checks.find(var)==checks.end() ça veut dire que var n'est pas dans checks
 						// mais je ne vois pas ce que tu comptes faire de la var
}//::
 
std::pair<variable_id, bool> problem::simplifiableVar() const {
	const variable_id id = pick(claims, negations);
	if (id!=-1) {
		return std::make_pair(id, true);   // n'ayant pas compris l'utilité de pick je ne suis pas certain de celle de simplifiableVar non plus
	}
	return std::make_pair(pick(negations, claims), false);
}
 
std::ostream& operator<<(std::ostream& os, problem const& p) {
	for(auto const& that : p) {
		os << (that.second) << '\n';
	}
	return os;
}
 
 
affectation problem::affectation_assignment(std::set<variable_id> const & vars) const{
	affectation values;
	for (variable_id id : vars) {
		values.insert(std::make_pair(id, rand()%2==0));    
	}
	return values;
}
 
//true if affectation is solution of this problem
bool problem::isSolution(affectation const& affectation) const {
	for (auto it = begin(); it!=end(); ++it) {
		if(!(it->second.eval(affectation))) return false;    
	}
	return true;
}
 
//return clauses failing under the given affectation
std::vector<problem::clause_id> problem::asSolution(affectation const& affectation_) const {
	std::vector<clause_id> errors;
	for (auto it = begin(); it!= end(); ++it) {
		if(!(it->second.eval(affectation_))) errors.push_back(it->first); 
	}
	return errors;
}
 
 
problem parse(const char* filename) {
	problem prob;
 
	std::string line;
	std::ifstream fichier(filename, std::ios::in);
 
	getline(fichier, line);
 
	while(std::getline(fichier, line)){
		std::istringstream iss(line);
 
		long int var1, var2;
 
		iss >> var1 >> var2;
		prob.add(clause(var1, var2));
	}
 
	return prob;
}
 
}//logika::

Malheureusement dans l'état il ne tourne pas très vite, j'ai peut etre fait des betises en debuggant, le problème semble venir de la fonction simplify. Je regarde ce que je peux faire :p.

[ternel]

Je dois dire que je n'ai pas beaucoup réfléchi aux performances.
Pour l'essentiel, j'ai repris la logique de ton code.

Pour la suite, il faut que je m'y intéresse ce soir.
Si j'y pense... sinon, ça sera ce week-end.

[ImmoTPA]

Daccord merci ! Bon après-midi.