113 lines
4.1 KiB
Plaintext
113 lines
4.1 KiB
Plaintext
{
|
|
"cells": [
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"# Copyright 2010-2018 Google LLC\n",
|
|
"# Licensed under the Apache License, Version 2.0 (the \"License\");\n",
|
|
"# you may not use this file except in compliance with the License.\n",
|
|
"# You may obtain a copy of the License at\n",
|
|
"#\n",
|
|
"# http://www.apache.org/licenses/LICENSE-2.0\n",
|
|
"#\n",
|
|
"# Unless required by applicable law or agreed to in writing, software\n",
|
|
"# distributed under the License is distributed on an \"AS IS\" BASIS,\n",
|
|
"# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.\n",
|
|
"# See the License for the specific language governing permissions and\n",
|
|
"# limitations under the License.\n",
|
|
"\"\"\"Implements a step function.\"\"\"\n",
|
|
"\n",
|
|
"from __future__ import absolute_import\n",
|
|
"from __future__ import division\n",
|
|
"from __future__ import print_function\n",
|
|
"\n",
|
|
"from ortools.sat.python import cp_model\n",
|
|
"\n",
|
|
"\n",
|
|
"class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback):\n",
|
|
" \"\"\"Print intermediate solutions.\"\"\"\n",
|
|
"\n",
|
|
" def __init__(self, variables):\n",
|
|
" cp_model.CpSolverSolutionCallback.__init__(self)\n",
|
|
" self.__variables = variables\n",
|
|
" self.__solution_count = 0\n",
|
|
"\n",
|
|
" def on_solution_callback(self):\n",
|
|
" self.__solution_count += 1\n",
|
|
" for v in self.__variables:\n",
|
|
" print('%s=%i' % (v, self.Value(v)), end=' ')\n",
|
|
" print()\n",
|
|
"\n",
|
|
" def solution_count(self):\n",
|
|
" return self.__solution_count\n",
|
|
"\n",
|
|
"\n",
|
|
"def step_function_sample_sat():\n",
|
|
" \"\"\"Encode the step function.\"\"\"\n",
|
|
"\n",
|
|
" # Model.\n",
|
|
" model = cp_model.CpModel()\n",
|
|
"\n",
|
|
" # Declare our primary variable.\n",
|
|
" x = model.NewIntVar(0, 20, 'x')\n",
|
|
"\n",
|
|
" # Create the expression variable and implement the step function\n",
|
|
" # Note it is not defined for x == 2.\n",
|
|
" #\n",
|
|
" # - 3\n",
|
|
" # -- -- --------- 2\n",
|
|
" # 1\n",
|
|
" # -- --- 0\n",
|
|
" # 0 ================ 20\n",
|
|
" #\n",
|
|
" expr = model.NewIntVar(0, 3, 'expr')\n",
|
|
"\n",
|
|
" # expr == 0 on [5, 6] U [8, 10]\n",
|
|
" b0 = model.NewBoolVar('b0')\n",
|
|
" model.AddLinearExpressionInDomain(\n",
|
|
" x, cp_model.Domain.FromIntervals([(5, 6), (8, 10)])).OnlyEnforceIf(b0)\n",
|
|
" model.Add(expr == 0).OnlyEnforceIf(b0)\n",
|
|
"\n",
|
|
" # expr == 2 on [0, 1] U [3, 4] U [11, 20]\n",
|
|
" b2 = model.NewBoolVar('b2')\n",
|
|
" model.AddLinearExpressionInDomain(\n",
|
|
" x, cp_model.Domain.FromIntervals([(0, 1), (3, 4),\n",
|
|
" (11, 20)])).OnlyEnforceIf(b2)\n",
|
|
" model.Add(expr == 2).OnlyEnforceIf(b2)\n",
|
|
"\n",
|
|
" # expr == 3 when x == 7\n",
|
|
" b3 = model.NewBoolVar('b3')\n",
|
|
" model.Add(x == 7).OnlyEnforceIf(b3)\n",
|
|
" model.Add(expr == 3).OnlyEnforceIf(b3)\n",
|
|
"\n",
|
|
" # At least one bi is true. (we could use a sum == 1).\n",
|
|
" model.AddBoolOr([b0, b2, b3])\n",
|
|
"\n",
|
|
" # Search for x values in increasing order.\n",
|
|
" model.AddDecisionStrategy([x], cp_model.CHOOSE_FIRST,\n",
|
|
" cp_model.SELECT_MIN_VALUE)\n",
|
|
"\n",
|
|
" # Create a solver and solve with a fixed search.\n",
|
|
" solver = cp_model.CpSolver()\n",
|
|
"\n",
|
|
" # Force the solver to follow the decision strategy exactly.\n",
|
|
" solver.parameters.search_branching = cp_model.FIXED_SEARCH\n",
|
|
"\n",
|
|
" # Search and print out all solutions.\n",
|
|
" solution_printer = VarArraySolutionPrinter([x, expr])\n",
|
|
" solver.SearchForAllSolutions(model, solution_printer)\n",
|
|
"\n",
|
|
"\n",
|
|
"step_function_sample_sat()\n",
|
|
"\n"
|
|
]
|
|
}
|
|
],
|
|
"metadata": {},
|
|
"nbformat": 4,
|
|
"nbformat_minor": 4
|
|
}
|