5 * !b2 OR b1 or (!b3 and b4) AND
6 * b7 OR (!b1 AND (b5 or !b6))
9 int main(int numargs, char **argv) {
10 CSolver *solver = new CSolver();
11 BooleanEdge b1 = solver->getBooleanVar(0);
12 BooleanEdge b2 = solver->getBooleanVar(0);
13 BooleanEdge b3 = solver->getBooleanVar(0);
14 BooleanEdge b4 = solver->getBooleanVar(0);
15 BooleanEdge b5 = solver->getBooleanVar(0);
16 BooleanEdge b6 = solver->getBooleanVar(0);
17 BooleanEdge b7 = solver->getBooleanVar(0);
18 //SATC_AND, SATC_OR, SATC_NOT, SATC_XOR, SATC_IMPLIES
19 BooleanEdge in[] = {b1};
20 BooleanEdge notb1 = solver->applyLogicalOperation(SATC_NOT, in, 1);
21 BooleanEdge in2[] = {b2};
22 BooleanEdge notb2 = solver->applyLogicalOperation(SATC_NOT, in2, 1);
23 BooleanEdge in3[] = {b3};
24 BooleanEdge notb3 = solver->applyLogicalOperation(SATC_NOT, in3, 1);
25 BooleanEdge in4[] = {notb3,b4};
26 BooleanEdge andnotb3b4 = solver->applyLogicalOperation(SATC_AND, in4, 2);
27 BooleanEdge in5[] = {notb2, b1, andnotb3b4};
28 BooleanEdge secondc = solver->applyLogicalOperation(SATC_OR, in5, 3);
29 BooleanEdge in6[] = {b6};
30 BooleanEdge notb6 = solver->applyLogicalOperation(SATC_NOT, in6, 1);
31 BooleanEdge in7[] = {b5,notb6};
32 BooleanEdge orb5notb6 = solver->applyLogicalOperation(SATC_OR, in7, 2);
33 BooleanEdge in8[] = {notb1,orb5notb6};
34 BooleanEdge andnotb1ors = solver->applyLogicalOperation(SATC_AND, in8, 2);
35 BooleanEdge in9[] = {b7, andnotb1ors};
36 BooleanEdge third = solver->applyLogicalOperation(SATC_OR, in9, 2);
37 BooleanEdge in10[] = {secondc, third, notb1};
38 BooleanEdge final = solver->applyLogicalOperation(SATC_AND, in10, 3);
39 solver->addConstraint(final);
40 printf("&&&&&&&&&&&&&&&&&&&&&&&\n");
41 solver->printConstraints();
42 if (solver->solve() == 1)
43 printf("b1=%d\nb2=%d\nb3=%d\nb4=%d\nb5=%d\nb6=%d\nb7=%d\n",
44 solver->getBooleanValue(b1), solver->getBooleanValue(b2),
45 solver->getBooleanValue(b3), solver->getBooleanValue(b4),
46 solver->getBooleanValue(b5), solver->getBooleanValue(b6),
47 solver->getBooleanValue(b7));