4 * TotalOrder(0, 1, 2, 3, 4, 5, 6, 7, 8, 9)
19 int main(int numargs, char **argv) {
20 CSolver *solver = new CSolver();
21 uint64_t set1[] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
22 Set *s = solver->createSet(0, set1, 10);
23 Order *order = solver->createOrder(SATC_TOTAL, s);
24 BooleanEdge b01 = solver->orderConstraint(order, 0, 1);
25 solver->addConstraint(b01);
26 BooleanEdge b12 = solver->orderConstraint(order, 1, 2);
27 solver->addConstraint(b12);
28 BooleanEdge b23 = solver->orderConstraint(order, 2, 3);
29 solver->addConstraint(b23);
30 BooleanEdge b14 = solver->orderConstraint(order, 1, 4);
31 solver->addConstraint(b14);
32 BooleanEdge b45 = solver->orderConstraint(order, 4, 5);
33 solver->addConstraint(b45);
34 BooleanEdge b56 = solver->orderConstraint(order, 5, 6);
35 solver->addConstraint(b56);
36 BooleanEdge b17 = solver->orderConstraint(order, 1, 7);
37 solver->addConstraint(b17);
38 BooleanEdge b78 = solver->orderConstraint(order, 7, 8);
39 solver->addConstraint(b78);
40 BooleanEdge b89 = solver->orderConstraint(order, 8, 9);
41 solver->addConstraint(b89);
42 BooleanEdge b92 = solver->orderConstraint(order, 9, 2);
43 solver->addConstraint(b92);
44 BooleanEdge b62 = solver->orderConstraint(order, 6, 2);
45 solver->addConstraint(b62);
47 BooleanEdge v1 = solver->getBooleanVar(0);
48 solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v1));
49 BooleanEdge v2 = solver->getBooleanVar(0);
50 solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v2));
51 BooleanEdge v3 = solver->getBooleanVar(0);
52 BooleanEdge v4 = solver->getBooleanVar(0);
53 BooleanEdge v5 = solver->getBooleanVar(0);
54 BooleanEdge be = solver->applyLogicalOperation(SATC_IFF, v3, v4);
55 BooleanEdge sor = solver->applyLogicalOperation(SATC_OR, be, v5);
56 solver->addConstraint(sor);
57 solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v5));
58 BooleanEdge v6 = solver->getBooleanVar(0);
59 BooleanEdge v7 = solver->getBooleanVar(0);
60 BooleanEdge v8 = solver->getBooleanVar(0);
61 solver->addConstraint(
62 solver->applyLogicalOperation(SATC_OR,
63 solver->applyLogicalOperation(SATC_IFF, v7, v8),
65 solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v6));
66 BooleanEdge v9 = solver->getBooleanVar(0);
67 solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v9, v3));
68 BooleanEdge v10 = solver->getBooleanVar(0);
69 BooleanEdge v11 = solver->getBooleanVar(0);
70 BooleanEdge v12 = solver->getBooleanVar(0);
71 solver->addConstraint(
72 solver->applyLogicalOperation(SATC_OR,
73 solver->applyLogicalOperation(SATC_OR, v10, v11),
74 solver->applyLogicalOperation(SATC_IFF, v1, v12)));
75 BooleanEdge b48 = solver->orderConstraint(order, 4, 8);
76 BooleanEdge be1 = solver->applyLogicalOperation(SATC_OR, v10, v11);
77 BooleanEdge be2 = solver->applyLogicalOperation(SATC_OR, be1, b48);
78 solver->addConstraint(be2);
79 BooleanEdge v13 = solver->getBooleanVar(0);
80 BooleanEdge v14 = solver->getBooleanVar(0);
81 solver->addConstraint(
82 solver->applyLogicalOperation(SATC_OR,
83 solver->applyLogicalOperation(SATC_IMPLIES, v10, v11),
84 solver->applyLogicalOperation(SATC_AND,
85 solver->applyLogicalOperation(SATC_IFF, v12, v13),
86 solver->applyLogicalOperation(SATC_NOT,b48))
88 solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v11));
89 solver->addConstraint(v14);
90 solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v8, v12));
91 solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v12, v8));
92 BooleanEdge v15 = solver->getBooleanVar(0);
93 BooleanEdge v16 = solver->getBooleanVar(0);
94 BooleanEdge v17 = solver->getBooleanVar(0);
95 BooleanEdge v18 = solver->getBooleanVar(0);
96 solver->addConstraint(
97 solver->applyLogicalOperation(SATC_OR,
98 solver->applyLogicalOperation(SATC_OR, v15, v16),
99 solver->applyLogicalOperation(SATC_IFF, v17, v2)
101 BooleanEdge b57 = solver->orderConstraint(order, 5, 7);
102 solver->addConstraint(
103 solver->applyLogicalOperation(SATC_IMPLIES,
105 solver->applyLogicalOperation(SATC_OR, v15, v16)
107 solver->addConstraint(
108 solver->applyLogicalOperation(SATC_IMPLIES,
109 solver->applyLogicalOperation(SATC_AND, v15, solver->applyLogicalOperation(SATC_NOT,v16)),
110 solver->applyLogicalOperation(SATC_AND, b57, solver->applyLogicalOperation(SATC_IFF, v17, v14))
112 solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v16));
113 solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v13, v17));
114 solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v17, v13));
115 solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v4, v17));
116 solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v17, v4));
117 solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v18, v9));
118 solver->addConstraint(v18);
120 if (solver->solve() == 1) {
122 printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",
123 solver->getOrderConstraintValue(order, 5, 1),
124 solver->getOrderConstraintValue(order, 1, 4),
125 solver->getOrderConstraintValue(order, 5, 4),
126 solver->getOrderConstraintValue(order, 1, 5));