From 7903ae5a0afe37b36f08fc67772629f2270dd745 Mon Sep 17 00:00:00 2001 From: zhang Date: Sat, 16 Apr 2022 11:04:42 +0800 Subject: =?UTF-8?q?ortools=20=E5=AE=9E=E8=B7=B5=E9=80=BB=E8=BE=91=E7=BA=A6?= =?UTF-8?q?=E6=9D=9F?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- cp/binary_encodings.py | 69 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 69 insertions(+) create mode 100644 cp/binary_encodings.py (limited to 'cp/binary_encodings.py') diff --git a/cp/binary_encodings.py b/cp/binary_encodings.py new file mode 100644 index 0000000..db38d38 --- /dev/null +++ b/cp/binary_encodings.py @@ -0,0 +1,69 @@ + +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) -- cgit v1.2.3