Skip to content

Commit

Permalink
limit to 3sat
Browse files Browse the repository at this point in the history
  • Loading branch information
Marc Vincenti committed Nov 26, 2019
1 parent 9eaabb4 commit 759bc5a
Show file tree
Hide file tree
Showing 4 changed files with 60 additions and 63 deletions.
2 changes: 1 addition & 1 deletion include/cnf.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ typedef struct value_t {
} value;

typedef struct clause_t {
litteral litterals[4];
litteral litterals[3];
litteral max_litteral;
struct clause_t * next;
} clause;
Expand Down
99 changes: 53 additions & 46 deletions src/cnf.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -68,12 +68,11 @@ cnf* copy_cnf(cnf* old_cnf) {
return ret;
}

void new_clause(cnf* cnf, litteral l_a, litteral l_b, litteral l_c, litteral l_d) {
void new_clause(cnf* cnf, litteral l_a, litteral l_b, litteral l_c) {
clause* cl = malloc(sizeof(clause));
cl->litterals[0] = l_a;
cl->litterals[1] = l_b;
cl->litterals[2] = l_c;
cl->litterals[3] = l_d;
cl->max_litteral = cnf->nb_litterals;
cl->next = cnf->head;
cnf->head = cl;
Expand All @@ -84,14 +83,14 @@ cnf* fix_value(cnf* cnf, litteral l) {
clause* pred = NULL;
clause* toRelax = NULL;
while (cl != NULL && cl->max_litteral >= abs(l)) {
if (cl->litterals[0] == l || cl->litterals[1] == l || cl->litterals[2] == l || cl->litterals[3] == l) {
if (cl->litterals[0] == l || cl->litterals[1] == l || cl->litterals[2] == l) {
/* We satisfy the clause */
if (pred != NULL) { pred->next = cl->next; } else { cnf->head = cl->next; }
toRelax = cl;
cl = cl->next;
free(toRelax);
} else if (cl->litterals[0] == -l) {
if (cl->litterals[1] == 0 && cl->litterals[2] == 0 && cl->litterals[3] == 0) {
if (cl->litterals[1] == 0 && cl->litterals[2] == 0) {
/* We unsatisfy the clause */
if (pred != NULL) { pred->next = cl->next; } else { cnf->head = cl->next; }
toRelax = cl;
Expand All @@ -103,7 +102,7 @@ cnf* fix_value(cnf* cnf, litteral l) {
cl = cl->next;
}
} else if (cl->litterals[1] == -l) {
if (cl->litterals[0] == 0 && cl->litterals[2] == 0 && cl->litterals[3] == 0) {
if (cl->litterals[0] == 0 && cl->litterals[2] == 0) {
/* We unsatisfy the clause */
if (pred != NULL) { pred->next = cl->next; } else { cnf->head = cl->next; }
toRelax = cl;
Expand All @@ -115,7 +114,7 @@ cnf* fix_value(cnf* cnf, litteral l) {
cl = cl->next;
}
} else if (cl->litterals[2] == -l) {
if (cl->litterals[0] == 0 && cl->litterals[1] == 0 && cl->litterals[3] == 0) {
if (cl->litterals[0] == 0 && cl->litterals[1] == 0) {
/* We unsatisfy the clause */
if (pred != NULL) { pred->next = cl->next; } else { cnf->head = cl->next; }
toRelax = cl;
Expand All @@ -126,18 +125,6 @@ cnf* fix_value(cnf* cnf, litteral l) {
pred = cl;
cl = cl->next;
}
} else if (cl->litterals[3] == -l) {
if (cl->litterals[0] == 0 && cl->litterals[1] == 0 && cl->litterals[2] == 0) {
/* We unsatisfy the clause */
if (pred != NULL) { pred->next = cl->next; } else { cnf->head = cl->next; }
toRelax = cl;
cl = cl->next;
free(toRelax);
} else {
cl->litterals[3] = 0;
pred = cl;
cl = cl->next;
}
} else {
pred = cl;
cl = cl->next;
Expand Down Expand Up @@ -200,9 +187,9 @@ value* or(cnf* cnf, value* a, value* b) {
} else {
/* a V b -> (¬r V a V b) & (r V ¬a) & (r V ¬b) */
r = new_litteral(cnf);
new_clause(cnf, -r->value.l, a->value.l, b->value.l, 0);
new_clause(cnf, r->value.l, -a->value.l, 0, 0);
new_clause(cnf, r->value.l, -b->value.l, 0, 0);
new_clause(cnf, -r->value.l, a->value.l, b->value.l);
new_clause(cnf, r->value.l, -a->value.l, 0);
new_clause(cnf, r->value.l, -b->value.l, 0);
return r;
}
}
Expand Down Expand Up @@ -230,9 +217,9 @@ value* and(cnf* cnf, value* a, value* b) {
} else {
/* a & b -> (r V ¬a V ¬b) & (¬r V a) & (¬r V b) */
r = new_litteral(cnf);
new_clause(cnf, r->value.l, -a->value.l, -b->value.l, 0);
new_clause(cnf, -r->value.l, a->value.l, 0, 0);
new_clause(cnf, -r->value.l, b->value.l, 0, 0);
new_clause(cnf, r->value.l, -a->value.l, -b->value.l);
new_clause(cnf, -r->value.l, a->value.l, 0);
new_clause(cnf, -r->value.l, b->value.l, 0);
return r;
}
}
Expand All @@ -258,10 +245,10 @@ value* xor(cnf* cnf, value* a, value* b) {
} else {
/* a ^ b -> (a V b V ¬r) & (a V ¬b V r) & (¬a V b V r) & (¬a V ¬b V ¬r) */
r = new_litteral(cnf);
new_clause(cnf, -r->value.l, a->value.l, b->value.l, 0);
new_clause(cnf, -r->value.l, -a->value.l, -b->value.l, 0);
new_clause(cnf, r->value.l, -a->value.l, b->value.l, 0);
new_clause(cnf, r->value.l, a->value.l, -b->value.l, 0);
new_clause(cnf, -r->value.l, a->value.l, b->value.l);
new_clause(cnf, -r->value.l, -a->value.l, -b->value.l);
new_clause(cnf, r->value.l, -a->value.l, b->value.l);
new_clause(cnf, r->value.l, a->value.l, -b->value.l);
return r;
}
}
Expand Down Expand Up @@ -295,15 +282,35 @@ value* xor_3(cnf* cnf, value* a, value* b, value* c) {
& (r V s1 V ¬c) & (r V ¬s1 V c) & (¬r V s1 V c) & (¬r V ¬s1 V ¬c)
& (r V s2 V ¬b) & (r V ¬s2 V b) & (¬r V s2 V b) & (¬r V ¬s2 V ¬b)
& (r V s3 V ¬a) & (r V ¬s3 V a) & (¬r V s3 V a) & (¬r V ¬s3 V ¬a) */
s1 = new_litteral(cnf);
s2 = new_litteral(cnf);
s3 = new_litteral(cnf);
r = new_litteral(cnf);
new_clause(cnf, r->value.l, -a->value.l, b->value.l, c->value.l);
new_clause(cnf, r->value.l, a->value.l, -b->value.l, c->value.l);
new_clause(cnf, r->value.l, a->value.l, b->value.l, -c->value.l);
new_clause(cnf, r->value.l, -a->value.l, -b->value.l, -c->value.l);
new_clause(cnf, -r->value.l, a->value.l, b->value.l, c->value.l);
new_clause(cnf, -r->value.l, -a->value.l, -b->value.l, c->value.l);
new_clause(cnf, -r->value.l, a->value.l, -b->value.l, -c->value.l);
new_clause(cnf, -r->value.l, -a->value.l, b->value.l, -c->value.l);
new_clause(cnf, s1->value.l, a->value.l, -b->value.l);
new_clause(cnf, s1->value.l, -a->value.l, b->value.l);
new_clause(cnf, -s1->value.l, a->value.l, b->value.l);
new_clause(cnf, -s1->value.l, -a->value.l, -b->value.l);
new_clause(cnf, s2->value.l, a->value.l, -c->value.l);
new_clause(cnf, s2->value.l, -a->value.l, c->value.l);
new_clause(cnf, -s2->value.l, a->value.l, c->value.l);
new_clause(cnf, -s2->value.l, -a->value.l, -c->value.l);
new_clause(cnf, s3->value.l, b->value.l, -c->value.l);
new_clause(cnf, s3->value.l, -b->value.l, c->value.l);
new_clause(cnf, -s3->value.l, b->value.l, c->value.l);
new_clause(cnf, -s3->value.l, -b->value.l, -c->value.l);
new_clause(cnf, r->value.l, s1->value.l, -c->value.l);
new_clause(cnf, r->value.l, -s1->value.l, c->value.l);
new_clause(cnf, -r->value.l, s1->value.l, c->value.l);
new_clause(cnf, -r->value.l, -s1->value.l, -c->value.l);
new_clause(cnf, r->value.l, s2->value.l, -b->value.l);
new_clause(cnf, r->value.l, -s2->value.l, b->value.l);
new_clause(cnf, -r->value.l, s2->value.l, b->value.l);
new_clause(cnf, -r->value.l, -s2->value.l, -b->value.l);
new_clause(cnf, r->value.l, s3->value.l, -a->value.l);
new_clause(cnf, r->value.l, -s3->value.l, a->value.l);
new_clause(cnf, -r->value.l, s3->value.l, a->value.l);
new_clause(cnf, -r->value.l, -s3->value.l, -a->value.l);
free(s3); free(s2); free(s1);
return r;
}
}
Expand Down Expand Up @@ -336,10 +343,10 @@ value* ch(cnf* cnf, value* a, value* b, value* c) {
/* (a & b) V (¬a & c) -> (r V ¬a V ¬b) & (r V a V ¬c)
& (¬r V ¬a V b) & (¬r V a V c) */
r = new_litteral(cnf);
new_clause(cnf, r->value.l, -a->value.l, -b->value.l, 0);
new_clause(cnf, r->value.l, a->value.l, -c->value.l, 0);
new_clause(cnf, -r->value.l, -a->value.l, b->value.l, 0);
new_clause(cnf, -r->value.l, a->value.l, c->value.l, 0);
new_clause(cnf, r->value.l, -a->value.l, -b->value.l);
new_clause(cnf, r->value.l, a->value.l, -c->value.l);
new_clause(cnf, -r->value.l, -a->value.l, b->value.l);
new_clause(cnf, -r->value.l, a->value.l, c->value.l);
return r;
}
}
Expand Down Expand Up @@ -376,12 +383,12 @@ value* maj(cnf* cnf, value* a, value* b, value* c) {
(r V ¬a V ¬b) & (r V ¬b V ¬c) & (r V ¬a V ¬c)
& (¬r V a V b) & (¬r V b V c) & (¬r V a V c) */
r = new_litteral(cnf);
new_clause(cnf, r->value.l, -a->value.l, -b->value.l, 0);
new_clause(cnf, r->value.l, -b->value.l, -c->value.l, 0);
new_clause(cnf, r->value.l, -a->value.l, -c->value.l, 0);
new_clause(cnf, -r->value.l, a->value.l, b->value.l, 0);
new_clause(cnf, -r->value.l, b->value.l, c->value.l, 0);
new_clause(cnf, -r->value.l, a->value.l, c->value.l, 0);
new_clause(cnf, r->value.l, -a->value.l, -b->value.l);
new_clause(cnf, r->value.l, -b->value.l, -c->value.l);
new_clause(cnf, r->value.l, -a->value.l, -c->value.l);
new_clause(cnf, -r->value.l, a->value.l, b->value.l);
new_clause(cnf, -r->value.l, b->value.l, c->value.l);
new_clause(cnf, -r->value.l, a->value.l, c->value.l);
return r;
}
}
15 changes: 4 additions & 11 deletions src/karloff_zwick.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,8 +10,6 @@ litteral pick_litteral(cnf* cnf) {
return cl->litterals[1];
} else if (cl->litterals[2] != 0) {
return cl->litterals[2];
} else if (cl->litterals[3] != 0) {
return cl->litterals[3];
}
}
return 0;
Expand All @@ -22,26 +20,21 @@ kz_value test_litteral(cnf* cnf, litteral l) {
kz_value res;
res.nb_sat = res.nb_unsat = 0;
while (cl != NULL && cl->max_litteral >= abs(l)) {
if (cl->litterals[0] == l || cl->litterals[1] == l || cl->litterals[2] == l || cl->litterals[3] == l) {
if (cl->litterals[0] == l || cl->litterals[1] == l || cl->litterals[2] == l) {
/* We satisfy the clause */
res.nb_sat++;
} else if (cl->litterals[0] == -l) {
if (cl->litterals[1] == 0 && cl->litterals[2] == 0 && cl->litterals[3] == 0) {
if (cl->litterals[1] == 0 && cl->litterals[2] == 0) {
/* We unsatisfy the clause */
res.nb_unsat++;
}
} else if (cl->litterals[1] == -l) {
if (cl->litterals[0] == 0 && cl->litterals[2] == 0 && cl->litterals[3] == 0) {
if (cl->litterals[0] == 0 && cl->litterals[2] == 0) {
/* We unsatisfy the clause */
res.nb_unsat++;
}
} else if (cl->litterals[2] == -l) {
if (cl->litterals[0] == 0 && cl->litterals[1] == 0 && cl->litterals[3] == 0) {
/* We unsatisfy the clause */
res.nb_unsat++;
}
} else if (cl->litterals[3] == -l) {
if (cl->litterals[0] == 0 && cl->litterals[1] == 0 && cl->litterals[2] == 0) {
if (cl->litterals[0] == 0 && cl->litterals[1] == 0) {
/* We unsatisfy the clause */
res.nb_unsat++;
}
Expand Down
7 changes: 2 additions & 5 deletions src/loop.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@ int main (int argc, char* argv[]) {
value** hashed = hash(cnf, "", 256);
for (i = 0; i < 256; i++) {
if (hashed[i]->type == variable) {
new_clause(cnf, hashed[i]->value.l, -(i+1), 0, 0);
new_clause(cnf, -hashed[i]->value.l, (i+1), 0, 0);
new_clause(cnf, hashed[i]->value.l, -(i+1), 0);
new_clause(cnf, -hashed[i]->value.l, (i+1), 0);
} else {
fprintf(stderr, "hashed[%i] is a constant.\n", i);
EXIT_FAILURE;
Expand All @@ -35,9 +35,6 @@ int main (int argc, char* argv[]) {
if (cl->litterals[2] != 0) {
fprintf(stdout, "%i ", cl->litterals[2]);
}
if (cl->litterals[3] != 0) {
fprintf(stdout, "%i ", cl->litterals[3]);
}
fprintf(stdout, "0\n");
cl = cl->next;
}
Expand Down

0 comments on commit 759bc5a

Please sign in to comment.