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 solver->addConstraint(
55 solver->applyLogicalOperation(SATC_OR,
56 solver->applyLogicalOperation(SATC_IFF, v3, v4),
58 solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v5));
59 BooleanEdge v6 = solver->getBooleanVar(0);
60 BooleanEdge v7 = solver->getBooleanVar(0);
61 BooleanEdge v8 = solver->getBooleanVar(0);
62 solver->addConstraint(
63 solver->applyLogicalOperation(SATC_OR,
64 solver->applyLogicalOperation(SATC_IFF, v7, v8),
66 solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v6));
67 BooleanEdge v9 = solver->getBooleanVar(0);
68 solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v9, v3));
69 BooleanEdge v10 = solver->getBooleanVar(0);
70 BooleanEdge v11 = solver->getBooleanVar(0);
71 BooleanEdge v12 = solver->getBooleanVar(0);
72 solver->addConstraint(
73 solver->applyLogicalOperation(SATC_IMPLIES,
74 solver->applyLogicalOperation(SATC_AND, v10, v11),
75 solver->applyLogicalOperation(SATC_IFF, v1, v12)));
76 BooleanEdge b48 = solver->orderConstraint(order, 4, 8);
77 solver->addConstraint(
78 solver->applyLogicalOperation(SATC_OR,
79 solver->applyLogicalOperation(SATC_OR, v10, v11),
81 BooleanEdge v13 = solver->getBooleanVar(0);
82 BooleanEdge v14 = solver->getBooleanVar(0);
83 solver->addConstraint(
84 solver->applyLogicalOperation(SATC_OR,
85 solver->applyLogicalOperation(SATC_IMPLIES, v10, v11),
86 solver->applyLogicalOperation(SATC_AND,
87 solver->applyLogicalOperation(SATC_IFF, v12, v13),
88 solver->applyLogicalOperation(SATC_NOT,b48))
90 solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v11));
91 solver->addConstraint(v14);
92 solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v8, v12));
93 solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v12, v8));
94 BooleanEdge v15 = solver->getBooleanVar(0);
95 BooleanEdge v16 = solver->getBooleanVar(0);
96 BooleanEdge v17 = solver->getBooleanVar(0);
97 BooleanEdge v18 = solver->getBooleanVar(0);
98 solver->addConstraint(
99 solver->applyLogicalOperation(SATC_OR,
100 solver->applyLogicalOperation(SATC_OR, v15, v16),
101 solver->applyLogicalOperation(SATC_IFF, v17, v2)
103 BooleanEdge b57 = solver->orderConstraint(order, 5, 7);
104 solver->addConstraint(
105 solver->applyLogicalOperation(SATC_IMPLIES,
107 solver->applyLogicalOperation(SATC_OR, v15, v16)
109 solver->addConstraint(
110 solver->applyLogicalOperation(SATC_IMPLIES,
111 solver->applyLogicalOperation(SATC_AND, v15, solver->applyLogicalOperation(SATC_NOT,v16)),
112 solver->applyLogicalOperation(SATC_AND, b57, solver->applyLogicalOperation(SATC_IFF, v17, v14))
114 solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v16));
115 solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v13, v17));
116 solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v17, v13));
117 solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v4, v17));
118 solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v17, v4));
119 solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v18, v9));
120 solver->addConstraint(v18);
122 if (solver->solve() == 1){
124 printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",
125 solver->getOrderConstraintValue(order, 5, 1),
126 solver->getOrderConstraintValue(order, 1, 4),
127 solver->getOrderConstraintValue(order, 5, 4),
128 solver->getOrderConstraintValue(order, 1, 5));