printCNF(nv1);
printf("\n");
Edge nv2=constraintNegate(v2);
+ Edge nv3=constraintNegate(v3);
Edge iff1=constraintIFF(cnf, nv1, v2);
printCNF(iff1);
printf("\n");
- Edge iff2=constraintIFF(cnf, nv2, v3);
+
+ Edge iff2=constraintOR2(cnf, constraintAND2(cnf, v2, v3), constraintAND2(cnf, nv2, nv3));
+ printCNF(iff2);
+ printf("\n");
Edge iff3=constraintIFF(cnf, v3, nv1);
Edge cand=constraintAND(cnf, 3, (Edge[]) {iff1, iff2, iff3});
- //Edge cand=constraintAND(cnf, 2, (Edge[]) {iff1, iff2});
+
printCNF(cand);
printf("\n");
addConstraint(cnf, cand);