1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
|
from ortools.sat.python import cp_model
# https://developers.google.com/optimization/cp/cryptarithmetic
class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback):
"""Print intermediate solutions."""
def __init__(self, variables):
cp_model.CpSolverSolutionCallback.__init__(self)
self.__variables = variables
self.__solution_count = 0
def on_solution_callback(self):
self.__solution_count += 1
for v in self.__variables:
print('%s=%i' % (v, self.Value(v)), end=' ')
print()
def solution_count(self):
return self.__solution_count
def imply(x, y):
# x=> y
# not(x) or y
# 0, 0/1
# 1, 1
# 1, 0
# 0 or 0 = 0 false
model.AddBoolOr([x.Not(), y])
def imply_2(x, y):
# x => y
model.AddImplication(x, y)
def two_way_imply(x, y):
# x <=> y
# x == y
imply_2(x, y)
imply_2(y, x)
def xor(x, y):
# x or y
model.AddBoolOr([x, y])
# not (x and y) <=> not(x) or not(y)
model.AddBoolOr([x.Not(), y.Not()])
if __name__ == '__main__':
model = cp_model.CpModel()
solver = cp_model.CpSolver()
x = model.NewBoolVar('x')
y = model.NewBoolVar('y')
solution_printer = VarArraySolutionPrinter([x, y])
solver.parameters.enumerate_all_solutions = True
# imply
# imply_2(x, y)
# two_way_imply(x, y)
xor(x, y)
solver.Solve(model, solution_printer)
|
