Skip to content

Commit 7bf970c

Browse files
bcribasbcribas
authored
Merge pull request #13 from drianne/adiciona-solucao-adrianne-matheusRoberto
Solução de Adrianne e Matheus Roberto
2 parents 4a8cb55 + b5de607 commit 7bf970c

File tree

5 files changed

+617
-0
lines changed

5 files changed

+617
-0
lines changed

‎solucoes/adrianne-matheusRoberto/Makefile

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CC = g++
2+
REQ_FLAGS = -O2 -static
3+
ADD_FLAGS = -lpthread -std=c++14
4+
FLAGS = $(REQ_FLAGS) $(ADD_FLAGS)
5+
MAIN = versao_paralelismo.cpp
6+
EXE = exec
7+
8+
all: clean
9+
$(CC) $(MAIN) $(FLAGS) -o $(EXE)
10+
11+
12+
clean:
13+
-rm -f $(EXE)
14+
15+
run:
16+
./$(EXE)

‎solucoes/adrianne-matheusRoberto/relatorio_adrianne_matheusRoberto.pdf

439 KB
Binary file not shown.

‎solucoes/adrianne-matheusRoberto/versao_paralelismo.cpp

+289
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,289 @@
1+
#include <bits/stdc++.h>
2+
#include <pthread.h>
3+
#include <iostream>
4+
#include <stack>
5+
#include <string>
6+
#include <mutex>
7+
#include <semaphore.h>
8+
9+
// #include <thread>
10+
#define QTD_THREADS 4
11+
using namespace std;
12+
13+
sem_t s_execucao[QTD_THREADS];
14+
sem_t s_impressao[QTD_THREADS];
15+
sem_t s_comando;
16+
pthread_t threads[QTD_THREADS];
17+
bool rodando = true;
18+
bool comando_flip_full;
19+
20+
21+
long int numero_variaveis, numero_clausulas;
22+
vector<vector<long int>> clausulas;
23+
vector<bool> mudancas;
24+
vector<long int> clausulas_verdadeiras;
25+
set<long int> clausulas_falsas;
26+
map<long int, long int> literais_errados_total;
27+
map<long int,vector<long int>>variaveis_clausulas;
28+
mutex mtx, mtx1, mtx_bd, mtx3, mtx4, mtx5, mtx6, mtx10;
29+
mutex mtx_literais_errados, mtx_index, mtx_index_flip, mtx_bd_clausulas, mtx_bd_literais, mtx_clausulas_verdadeiras;
30+
long int literal_flip;
31+
long int indice_threads=0;
32+
long int indice_threads_flip=0;
33+
vector <long int> v1;
34+
vector <long int> v2;
35+
36+
void verifica_flip() {
37+
long int tamanho_vetor1 = v1.size();
38+
while(indice_threads<tamanho_vetor1) {
39+
mtx_index.lock();
40+
int index = indice_threads++;
41+
mtx_index.unlock();
42+
if(index<tamanho_vetor1) {
43+
long int valor = v1[index];
44+
if(mudancas[literal_flip]){
45+
mtx3.lock();
46+
if(clausulas_verdadeiras[valor] == 0){
47+
mtx_literais_errados.lock();
48+
for(long int i=0;i<clausulas[valor].size();i++){
49+
literais_errados_total[clausulas[valor][i]]--;
50+
if(literais_errados_total[clausulas[valor][i]]<=0){
51+
mtx_bd_literais.lock();
52+
literais_errados_total.erase(clausulas[valor][i]);
53+
mtx_bd_literais.unlock();
54+
}
55+
}
56+
mtx_literais_errados.unlock();
57+
mtx_bd_clausulas.lock();
58+
clausulas_falsas.erase(valor);
59+
mtx_bd_clausulas.unlock();
60+
}
61+
mtx_clausulas_verdadeiras.lock();
62+
clausulas_verdadeiras[valor]++;
63+
mtx_clausulas_verdadeiras.unlock();
64+
mtx3.unlock();
65+
} else if(!mudancas[literal_flip]){
66+
mtx4.lock();
67+
if(clausulas_verdadeiras[valor] == 1) {
68+
mtx_literais_errados.lock();
69+
for(long int i=0;i<clausulas[valor].size();i++){
70+
literais_errados_total[clausulas[valor][i]]++;
71+
}
72+
mtx_literais_errados.unlock();
73+
mtx_bd_clausulas.lock();
74+
clausulas_falsas.insert(valor);
75+
mtx_bd_clausulas.unlock();
76+
}
77+
mtx_clausulas_verdadeiras.lock();
78+
clausulas_verdadeiras[valor]--;
79+
mtx_clausulas_verdadeiras.unlock();
80+
mtx4.unlock();
81+
}
82+
}
83+
}
84+
}
85+
void verifica_flip2() {
86+
long int tamanho_vetor_2 = v2.size();
87+
while(indice_threads_flip<tamanho_vetor_2) {
88+
mtx_index_flip.lock();
89+
int index = indice_threads_flip++;
90+
mtx_index_flip.unlock();
91+
if(index<tamanho_vetor_2) {
92+
long int valor = v2[index];
93+
if(mudancas[literal_flip]){
94+
mtx5.lock();
95+
if(clausulas_verdadeiras[valor] == 1) {
96+
mtx_literais_errados.lock();
97+
for(long int i=0;i<clausulas[valor].size();i++){
98+
literais_errados_total[clausulas[valor][i]]++;
99+
}
100+
mtx_literais_errados.unlock();
101+
mtx_bd_clausulas.lock();
102+
clausulas_falsas.insert(valor);
103+
mtx_bd_clausulas.unlock();
104+
}
105+
mtx_clausulas_verdadeiras.lock();
106+
clausulas_verdadeiras[valor]--;
107+
mtx_clausulas_verdadeiras.unlock();
108+
mtx5.unlock();
109+
} else if(!mudancas[literal_flip]){
110+
mtx6.lock();
111+
if(clausulas_verdadeiras[valor] == 0){
112+
mtx_literais_errados.lock();
113+
for(long int i=0;i<clausulas[valor].size();i++){
114+
literais_errados_total[clausulas[valor][i]]--;
115+
if(literais_errados_total[clausulas[valor][i]]<=0){
116+
mtx_bd_literais.lock();
117+
literais_errados_total.erase(clausulas[valor][i]);
118+
mtx_bd_literais.unlock();
119+
}
120+
}
121+
mtx_literais_errados.unlock();
122+
mtx_bd_clausulas.lock();
123+
clausulas_falsas.erase(valor);
124+
mtx_bd_clausulas.unlock();
125+
}
126+
mtx_clausulas_verdadeiras.lock();
127+
clausulas_verdadeiras[valor]++;
128+
mtx_clausulas_verdadeiras.unlock();
129+
mtx6.unlock();
130+
}
131+
}
132+
}
133+
}
134+
void verifica_full() {
135+
while(indice_threads<clausulas.size()) {
136+
mtx.lock();
137+
long int i = indice_threads++;
138+
mtx.unlock();
139+
if (i < clausulas.size()) {
140+
for(auto valor:clausulas[i]) {
141+
if ((valor > 0 and mudancas[abs(valor)] == true) || (valor < 0 and mudancas[abs(valor)] == false)) {
142+
mtx_bd.lock();
143+
clausulas_verdadeiras[i]++;
144+
mtx_bd.unlock();
145+
}
146+
}
147+
if(clausulas_verdadeiras[i] == 0) {
148+
mtx3.lock();
149+
clausulas_falsas.insert(i);
150+
for(auto valor:clausulas[i]) {
151+
literais_errados_total[valor]++;
152+
}
153+
mtx3.unlock();
154+
}
155+
}
156+
}
157+
}
158+
159+
void imprimir_lista_literais_errados()
160+
{
161+
if(clausulas_falsas.empty()) {
162+
cout << "SAT\n";
163+
} else {
164+
vector<pair<long int, long int>> aux_errados;
165+
for(auto x:literais_errados_total) {
166+
if(x.second>0)
167+
aux_errados.emplace_back(x.first, x.second);
168+
}
169+
sort(aux_errados.begin(), aux_errados.end(), [](auto &left, auto &right) {
170+
if (left.second == right.second){
171+
return abs(left.first) > abs(right.first);
172+
}
173+
else {
174+
return left.second > right.second;
175+
}
176+
});
177+
cout << "[" << clausulas_falsas.size() << " clausulas falsas]";
178+
for(auto x:clausulas_falsas)
179+
cout << ' ' << x;
180+
cout << '\n';
181+
cout << "[lits]";
182+
for(auto x:aux_errados) {
183+
cout << " " << x.first;
184+
}
185+
cout << '\n';
186+
}
187+
}
188+
189+
void* funcao_thread(void* arg) {
190+
long int index = *((long int *) arg);
191+
delete (long int *) arg;
192+
while (rodando) {
193+
sem_wait(&s_execucao[index]);
194+
if (rodando) {
195+
if (comando_flip_full) {
196+
verifica_full();
197+
}
198+
else {
199+
verifica_flip();
200+
verifica_flip2();
201+
}
202+
sem_post(&s_impressao[index]);
203+
}
204+
}
205+
return 0;
206+
}
207+
208+
void executa_threads() {
209+
for (long int i = 0; i < QTD_THREADS; i++) {
210+
sem_post(&s_execucao[i]);
211+
}
212+
sem_post(&s_comando);
213+
}
214+
215+
216+
int main()
217+
{
218+
cin >> numero_variaveis >> numero_clausulas;
219+
clausulas_verdadeiras = vector<long int>(numero_clausulas, 0);
220+
for(long int i=0; i<numero_clausulas; i++) {
221+
long int valor;
222+
vector<long int> vetor_clausula;
223+
while (cin >> valor, valor != 0) {
224+
vetor_clausula.push_back(valor);
225+
226+
variaveis_clausulas[valor].push_back(i);
227+
}
228+
clausulas.push_back(vetor_clausula);
229+
}
230+
231+
sem_init(&s_comando, 0, 0);
232+
for (long int i = 0; i<QTD_THREADS; i++) {
233+
sem_init(&s_execucao[i], 0, 0);
234+
sem_init(&s_impressao[i], 0, 0);
235+
}
236+
237+
for(long int i=0; i<QTD_THREADS; i++) {
238+
pthread_create(&threads[i], NULL, funcao_thread, new long int(i));
239+
}
240+
241+
string comando;
242+
mudancas.assign(numero_variaveis, false);
243+
while(cin >> comando) {
244+
long int valor;
245+
indice_threads = 0;
246+
indice_threads_flip = 0;
247+
pthread_t threads[QTD_THREADS];
248+
if(comando.compare("full") == 0) {
249+
literais_errados_total.clear();
250+
clausulas_falsas.clear();
251+
clausulas_verdadeiras.assign(numero_clausulas, 0);;
252+
comando_flip_full = true;
253+
for(long int i=0; i<numero_variaveis; i++) {
254+
cin >> valor;
255+
if (valor > 0) {
256+
mudancas[abs(valor)] = true;
257+
} else {
258+
mudancas[abs(valor)] = false;
259+
}
260+
}
261+
}
262+
else{
263+
comando_flip_full = false;
264+
cin >> literal_flip;
265+
mudancas[abs(literal_flip)] = !mudancas[abs(literal_flip)];
266+
v1.clear();
267+
v2.clear();
268+
for( auto valor:variaveis_clausulas[literal_flip]) {
269+
v1.push_back(valor);
270+
}
271+
for( auto valor:variaveis_clausulas[-literal_flip]) {
272+
v2.push_back(valor);
273+
}
274+
}
275+
executa_threads();
276+
for (long int i = 0; i < QTD_THREADS; i++) {
277+
sem_wait(&s_impressao[i]);
278+
}
279+
imprimir_lista_literais_errados();
280+
}
281+
rodando = false;
282+
for (long int i = 0; i < QTD_THREADS; i++) {
283+
sem_post(&s_execucao[i]);
284+
}
285+
for (long int i = 0; i < QTD_THREADS; i++) {
286+
pthread_join(threads[i], NULL);
287+
}
288+
289+
}

0 commit comments

Comments
 (0)