always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

notebook: update

Browse Source
This commit is contained in:
Corentin Le Molgat
2022-12-21 09:54:15 +01:00
parent 928bfbfedb
commit 2cb9f320f6
6 changed files with 328 additions and 150 deletions
Download Patch File Download Diff File Expand all files Collapse all files

465
examples/notebook/contrib/school_scheduling_sat.ipynb
View File

@@ -67,6 +67,14 @@
"!pip install ortools"
]
},
{
"cell_type": "markdown",
"id": "description",
"metadata": {},
"source": [
"'''Solve a School Scheduling Problem'''"
]
},
{
"cell_type": "code",
"execution_count": null,
@@ -77,173 +85,344 @@
"from ortools.sat.python import cp_model\n",
"\n",
"\n",
"class SchoolSchedulingProblem(object):\n",
"class SchoolSchedulingProblem():\n",
" '''Data of the problem.'''\n",
"\n",
" def __init__(self, subjects, teachers, curriculum, specialties, working_days,\n",
" periods, levels, sections, teacher_work_hours):\n",
" self.subjects = subjects\n",
" self.teachers = teachers\n",
" self.curriculum = curriculum\n",
" self.specialties = specialties\n",
" self.working_days = working_days\n",
" self.periods = periods\n",
" self.levels = levels\n",
" self.sections = sections\n",
" self.teacher_work_hours = teacher_work_hours\n",
" def __init__(self, levels, sections, subjects, curriculum, teachers,\n",
" specialties, time_slots):\n",
" self._levels = levels\n",
" self._sections = sections\n",
" self._subjects = subjects\n",
" self._curriculum = curriculum\n",
" assert len(self._curriculum) == len(self._levels) * len(\n",
" self._subjects), 'Some curriculum are missing'\n",
" for (lvl, sub) in self._curriculum.keys():\n",
" assert lvl in self._levels, f'{lvl} not in LEVELS'\n",
" assert sub in self._subjects, f'{sub} not in SUBJECTS'\n",
"\n",
" self._teachers = teachers\n",
" self._specialties = specialties\n",
" assert len(self._specialties) == len(\n",
" self._subjects), 'Missing some rows'\n",
" for s, ts in self._specialties.items():\n",
" assert s in self._subjects, f'{s} is not in SUBJECTS'\n",
" for t in ts:\n",
" assert t in self._teachers, f'{t} is not in TEACHERS'\n",
"\n",
" self._time_slots = time_slots\n",
"\n",
" @property\n",
" def levels(self):\n",
" return self._levels\n",
"\n",
" @property\n",
" def sections(self):\n",
" return self._sections\n",
"\n",
" @property\n",
" def subjects(self):\n",
" return self._subjects\n",
"\n",
" @property\n",
" def curriculum(self):\n",
" return self._curriculum\n",
"\n",
" @property\n",
" def teachers(self):\n",
" return self._teachers\n",
"\n",
" def teacher_name(self, teacher_idx):\n",
" assert 0 <= teacher_idx < len(self._teachers)\n",
" return list(self._teachers.keys())[teacher_idx]\n",
"\n",
" def teacher_max_hours(self, teacher_idx):\n",
" assert 0 <= teacher_idx < len(self._teachers)\n",
" return list(self._teachers.values())[teacher_idx]\n",
"\n",
" @property\n",
" def specialties(self):\n",
" return self._specialties\n",
"\n",
" def specialtie_teachers(self, subject):\n",
" assert subject in self._subjects, f'{subject} not in SUBJECTS'\n",
" return self._specialties[subject]\n",
"\n",
" @property\n",
" def time_slots(self):\n",
" return self._time_slots\n",
"\n",
" def slot_duration(self, slot_idx):\n",
" assert 0 <= slot_idx < len(self._time_slots)\n",
" return list(self._time_slots.values())[slot_idx]\n",
"\n",
"\n",
"class SchoolSchedulingSatSolver(object):\n",
"class SchoolSchedulingSatSolver():\n",
" '''Solver instance.'''\n",
"\n",
" def __init__(self, problem):\n",
" # Problem\n",
" self.problem = problem\n",
" def __init__(self, problem: SchoolSchedulingProblem):\n",
" # Problem\n",
" self._problem = problem\n",
"\n",
" # Utilities\n",
" self.timeslots = [\n",
" '{0:10} {1:6}'.format(x, y)\n",
" for x in problem.working_days\n",
" for y in problem.periods\n",
" ]\n",
" self.num_days = len(problem.working_days)\n",
" self.num_periods = len(problem.periods)\n",
" self.num_slots = len(self.timeslots)\n",
" self.num_teachers = len(problem.teachers)\n",
" self.num_subjects = len(problem.subjects)\n",
" self.num_levels = len(problem.levels)\n",
" self.num_sections = len(problem.sections)\n",
" self.courses = [\n",
" x * self.num_levels + y\n",
" for x in problem.levels\n",
" for y in problem.sections\n",
" ]\n",
" self.num_courses = self.num_levels * self.num_sections\n",
" # Utilities\n",
" num_levels = len(self._problem.levels)\n",
" self._all_levels = range(num_levels)\n",
" num_sections = len(self._problem.sections)\n",
" self._all_sections = range(num_sections)\n",
" num_subjects = len(self._problem.subjects)\n",
" self._all_subjects = range(num_subjects)\n",
" num_teachers = len(self._problem.teachers)\n",
" self._all_teachers = range(num_teachers)\n",
" num_slots = len(self._problem.time_slots)\n",
" self._all_slots = range(num_slots)\n",
"\n",
" all_courses = range(self.num_courses)\n",
" all_teachers = range(self.num_teachers)\n",
" all_slots = range(self.num_slots)\n",
" all_sections = range(self.num_sections)\n",
" all_subjects = range(self.num_subjects)\n",
" all_levels = range(self.num_levels)\n",
" # Create Model\n",
" self._model = cp_model.CpModel()\n",
"\n",
" self.model = cp_model.CpModel()\n",
" # Create Variables\n",
" self._assignment = {}\n",
" for lvl_idx, level in enumerate(self._problem.levels):\n",
" for sec_idx, section in enumerate(self._problem.sections):\n",
" for sub_idx, subject in enumerate(self._problem.subjects):\n",
" for tch_idx, teacher in enumerate(self._problem.teachers):\n",
" for slt_idx, slot in enumerate(self._problem.time_slots):\n",
" key = (lvl_idx, sec_idx, sub_idx, tch_idx, slt_idx)\n",
" name = f'{level}-{section} S:{subject} T:{teacher} Slot:{slot}'\n",
" #print(name)\n",
" if teacher in self._problem.specialtie_teachers(subject):\n",
" self._assignment[key] = self._model.NewBoolVar(name)\n",
" else:\n",
" name = 'NO DISP ' + name\n",
" self._assignment[key] = self._model.NewIntVar(0, 0, name)\n",
"\n",
" self.assignment = {}\n",
" for c in all_courses:\n",
" for s in all_subjects:\n",
" for t in all_teachers:\n",
" for slot in all_slots:\n",
" if t in self.problem.specialties[s]:\n",
" name = 'C:{%i} S:{%i} T:{%i} Slot:{%i}' % (c, s, t, slot)\n",
" self.assignment[c, s, t, slot] = self.model.NewBoolVar(name)\n",
" else:\n",
" name = 'NO DISP C:{%i} S:{%i} T:{%i} Slot:{%i}' % (c, s, t, slot)\n",
" self.assignment[c, s, t, slot] = self.model.NewIntVar(0, 0, name)\n",
" # Constraints\n",
" # Each Level-Section must have the quantity of classes per Subject specified in the Curriculum\n",
" for lvl_idx, level in enumerate(self._problem.levels):\n",
" for sec_idx in self._all_sections:\n",
" for sub_idx, subject in enumerate(self._problem.subjects):\n",
" required_duration = self._problem.curriculum[level, subject]\n",
" #print(f'L:{level} S:{subject} duration:{required_duration}h')\n",
" self._model.Add(\n",
" sum(self._assignment[lvl_idx, sec_idx, sub_idx, tch_idx, slt_idx] *\n",
" int(self._problem.slot_duration(slt_idx) * 10)\n",
" for tch_idx in self._all_teachers\n",
" for slt_idx in self._all_slots) == int(required_duration * 10))\n",
"\n",
" # Constraints\n",
" # Each Level-Section can do at most one class at a time\n",
" for lvl_idx in self._all_levels:\n",
" for sec_idx in self._all_sections:\n",
" for slt_idx in self._all_slots:\n",
" self._model.Add(\n",
" sum([\n",
" self._assignment[lvl_idx, sec_idx, sub_idx, tch_idx, slt_idx]\n",
" for sub_idx in self._all_subjects\n",
" for tch_idx in self._all_teachers\n",
" ]) <= 1)\n",
"\n",
" # Each course must have the quantity of classes specified in the curriculum\n",
" for level in all_levels:\n",
" for section in all_sections:\n",
" course = level * self.num_sections + section\n",
" for subject in all_subjects:\n",
" required_slots = self.problem.curriculum[\n",
" self.problem.levels[level], self.problem.subjects[subject]]\n",
" self.model.Add(\n",
" sum(self.assignment[course, subject, teacher, slot]\n",
" for slot in all_slots\n",
" for teacher in all_teachers) == required_slots)\n",
" # Teacher can do at most one class at a time\n",
" for tch_idx in self._all_teachers:\n",
" for slt_idx in self._all_slots:\n",
" self._model.Add(\n",
" sum([\n",
" self._assignment[lvl_idx, sec_idx, sub_idx, tch_idx, slt_idx]\n",
" for lvl_idx in self._all_levels\n",
" for sec_idx in self._all_sections\n",
" for sub_idx in self._all_subjects\n",
" ]) <= 1)\n",
"\n",
" # Teacher can do at most one class at a time\n",
" for teacher in all_teachers:\n",
" for slot in all_slots:\n",
" self.model.Add(\n",
" sum([\n",
" self.assignment[c, s, teacher, slot]\n",
" for c in all_courses\n",
" for s in all_subjects\n",
" ]) <= 1)\n",
" # Maximum work hours for each teacher\n",
" for tch_idx in self._all_teachers:\n",
" self._model.Add(\n",
" sum([\n",
" self._assignment[lvl_idx, sec_idx, sub_idx, tch_idx, slt_idx] *\n",
" int(self._problem.slot_duration(slt_idx) * 10)\n",
" for lvl_idx in self._all_levels\n",
" for sec_idx in self._all_sections\n",
" for sub_idx in self._all_subjects\n",
" for slt_idx in self._all_slots\n",
" ]) <= int(self._problem.teacher_max_hours(tch_idx) * 10))\n",
"\n",
" # Maximum work hours for each teacher\n",
" for teacher in all_teachers:\n",
" self.model.Add(\n",
" sum([\n",
" self.assignment[c, s, teacher, slot] for c in all_courses\n",
" for s in all_subjects for slot in all_slots\n",
" ]) <= self.problem.teacher_work_hours[teacher])\n",
" # Teacher makes all the classes of a subject's course\n",
" teacher_courses = {}\n",
" for lvl_idx, level in enumerate(self._problem.levels):\n",
" for sec_idx, section in enumerate(self._problem.sections):\n",
" for sub_idx, subject in enumerate(self._problem.subjects):\n",
" for tch_idx, teacher in enumerate(self._problem.teachers):\n",
" name = f'{level}-{section} S:{subject} T:{teacher}'\n",
" teacher_courses[lvl_idx, sec_idx, sub_idx, tch_idx] = self._model.NewBoolVar(name)\n",
" temp_array = [\n",
" self._assignment[lvl_idx, sec_idx, sub_idx, tch_idx, slt_idx]\n",
" for slt_idx in self._all_slots\n",
" ]\n",
" self._model.AddMaxEquality(\n",
" teacher_courses[lvl_idx, sec_idx, sub_idx, tch_idx], temp_array)\n",
" self._model.Add(\n",
" sum([teacher_courses[lvl_idx, sec_idx, sub_idx, tch_idx]\n",
" for tch_idx in self._all_teachers\n",
" ]) == 1)\n",
"\n",
" # Teacher makes all the classes of a subject's course\n",
" teacher_courses = {}\n",
" for level in all_levels:\n",
" for section in all_sections:\n",
" course = level * self.num_sections + section\n",
" for subject in all_subjects:\n",
" for t in all_teachers:\n",
" name = 'C:{%i} S:{%i} T:{%i}' % (course, subject, teacher)\n",
" teacher_courses[course, subject, t] = self.model.NewBoolVar(name)\n",
" temp_array = [\n",
" self.assignment[course, subject, t, slot] for slot in all_slots\n",
" ]\n",
" self.model.AddMaxEquality(teacher_courses[course, subject, t],\n",
" temp_array)\n",
" self.model.Add(\n",
" sum(teacher_courses[course, subject, t]\n",
" for t in all_teachers) == 1)\n",
"\n",
" def solve(self):\n",
" print('Solving')\n",
" solver = cp_model.CpSolver()\n",
" solution_printer = SchoolSchedulingSatSolutionPrinter()\n",
" status = solver.Solve(self.model, solution_printer)\n",
" print()\n",
" print('status', status)\n",
" print('Branches', solver.NumBranches())\n",
" print('Conflicts', solver.NumConflicts())\n",
" print('WallTime', solver.WallTime())\n",
" def print_teacher_schedule(self, tch_idx):\n",
" teacher_name = self._problem.teacher_name(tch_idx)\n",
" print(f'Teacher: {teacher_name}')\n",
" total_working_hours = 0\n",
" for slt_idx, slot in enumerate(self._problem.time_slots):\n",
" for lvl_idx, level in enumerate(self._problem.levels):\n",
" for sec_idx, section in enumerate(self._problem.sections):\n",
" for sub_idx, subject in enumerate(self._problem.subjects):\n",
" key = (lvl_idx, sec_idx, sub_idx, tch_idx, slt_idx)\n",
" if self._solver.BooleanValue(self._assignment[key]):\n",
" total_working_hours += self._problem.slot_duration(slt_idx)\n",
" print(f'{slot}: C:{level}-{section} S:{subject}')\n",
" print(f'Total working hours: {total_working_hours}h')\n",
"\n",
"\n",
" def print_class_schedule(self, lvl_idx, sec_idx):\n",
" level = self._problem.levels[lvl_idx]\n",
" section = self._problem.sections[sec_idx]\n",
" print(f'Class: {level}-{section}')\n",
" total_working_hours = {}\n",
" for sub in self._problem.subjects:\n",
" total_working_hours[sub] = 0\n",
" for slt_idx, slot in enumerate(self._problem.time_slots):\n",
" for tch_idx, teacher in enumerate(self._problem.teachers):\n",
" for sub_idx, subject in enumerate(self._problem.subjects):\n",
" key = (lvl_idx, sec_idx, sub_idx, tch_idx, slt_idx)\n",
" if self._solver.BooleanValue(self._assignment[key]):\n",
" total_working_hours[subject] += self._problem.slot_duration(slt_idx)\n",
" print(f'{slot}: S:{subject} T:{teacher}')\n",
" for (subject, hours) in total_working_hours.items():\n",
" print(f'Total working hours for {subject}: {hours}h')\n",
"\n",
"\n",
" def print_school_schedule(self):\n",
" print('School:')\n",
" for slt_idx, slot in enumerate(self._problem.time_slots):\n",
" tmp = f'{slot}:'\n",
" for lvl_idx, level in enumerate(self._problem.levels):\n",
" for sec_idx, section in enumerate(self._problem.sections):\n",
" for sub_idx, subject in enumerate(self._problem.subjects):\n",
" for tch_idx, teacher in enumerate(self._problem.teachers):\n",
" key = (lvl_idx, sec_idx, sub_idx, tch_idx, slt_idx)\n",
" if self._solver.BooleanValue(self._assignment[key]):\n",
" tmp += f' {level}-{section}:({subject},{teacher})'\n",
" print(tmp)\n",
"\n",
"\n",
" def solve(self):\n",
" print('Solving')\n",
" # Create Solver\n",
" self._solver = cp_model.CpSolver()\n",
"\n",
" solution_printer = SchoolSchedulingSatSolutionPrinter()\n",
" status = self._solver.Solve(self._model, solution_printer)\n",
" print('Status: ', self._solver.StatusName(status))\n",
"\n",
" if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:\n",
" print('\\n# Teachers')\n",
" for teacher_idx in self._all_teachers:\n",
" self.print_teacher_schedule(teacher_idx)\n",
"\n",
" print('\\n# Classes')\n",
" for level_idx in self._all_levels:\n",
" for section_idx in self._all_sections:\n",
" self.print_class_schedule(level_idx, section_idx)\n",
"\n",
" print('\\n# School')\n",
" self.print_school_schedule()\n",
"\n",
" print('Branches: ', self._solver.NumBranches())\n",
" print('Conflicts: ', self._solver.NumConflicts())\n",
" print('WallTime: ', self._solver.WallTime())\n",
"\n",
"\n",
"class SchoolSchedulingSatSolutionPrinter(cp_model.CpSolverSolutionCallback):\n",
"\n",
" def __init__(self):\n",
" cp_model.CpSolverSolutionCallback.__init__(self)\n",
" self.__solution_count = 0\n",
" def __init__(self):\n",
" cp_model.CpSolverSolutionCallback.__init__(self)\n",
" self.__solution_count = 0\n",
"\n",
" def OnSolutionCallback(self):\n",
" print('Found Solution!')\n",
" def OnSolutionCallback(self):\n",
" print(\n",
" f'Solution #{self.__solution_count}, objective: {self.ObjectiveValue()}'\n",
" )\n",
" self.__solution_count += 1\n",
"\n",
"\n",
"def main():\n",
" # DATA\n",
" subjects = ['English', 'Math', 'History']\n",
" levels = ['1-', '2-', '3-']\n",
" sections = ['A']\n",
" teachers = ['Mario', 'Elvis', 'Donald', 'Ian']\n",
" teachers_work_hours = [18, 12, 12, 18]\n",
" working_days = ['Monday', 'Tuesday', 'Wednesday', 'Thursday', 'Friday']\n",
" periods = ['08:00-09:30', '09:45-11:15', '11:30-13:00']\n",
" curriculum = {\n",
" ('1-', 'English'): 3,\n",
" ('1-', 'Math'): 3,\n",
" ('1-', 'History'): 2,\n",
" ('2-', 'English'): 4,\n",
" ('2-', 'Math'): 2,\n",
" ('2-', 'History'): 2,\n",
" ('3-', 'English'): 2,\n",
" ('3-', 'Math'): 4,\n",
" ('3-', 'History'): 2\n",
" }\n",
" # DATA\n",
" ## Classes\n",
" LEVELS = [\n",
" '1',\n",
" '2',\n",
" '3',\n",
" ]\n",
" SECTIONS = [\n",
" 'A',\n",
" 'B',\n",
" ]\n",
" SUBJECTS = [\n",
" 'English',\n",
" 'Math',\n",
" #'Science',\n",
" 'History',\n",
" ]\n",
" CURRICULUM = {\n",
" ('1', 'English'): 3,\n",
" ('1', 'Math'): 3,\n",
" ('1', 'History'): 2,\n",
" ('2', 'English'): 4,\n",
" ('2', 'Math'): 2,\n",
" ('2', 'History'): 2,\n",
" ('3', 'English'): 2,\n",
" ('3', 'Math'): 4,\n",
" ('3', 'History'): 2,\n",
" }\n",
"\n",
" # Subject -> List of teachers who can teach it\n",
" specialties_idx_inverse = [\n",
" [1, 3], # English -> Elvis & Ian\n",
" [0, 3], # Math -> Mario & Ian\n",
" [2, 3] # History -> Donald & Ian\n",
" ]\n",
" ## Teachers\n",
" TEACHERS = { # name, max_work_hours\n",
" 'Mario': 14,\n",
" 'Elvis': 12,\n",
" 'Harry': 12,\n",
" 'Ian': 14,\n",
" }\n",
" # Subject -> List of teachers who can teach it\n",
" SPECIALTIES = {\n",
" 'English': ['Elvis', 'Ian'],\n",
" 'Math': ['Mario', 'Ian'],\n",
" 'History': ['Harry', 'Ian'],\n",
" }\n",
"\n",
" problem = SchoolSchedulingProblem(\n",
" subjects, teachers, curriculum, specialties_idx_inverse, working_days,\n",
" periods, levels, sections, teachers_work_hours)\n",
" solver = SchoolSchedulingSatSolver(problem)\n",
" solver.solve()\n",
" ## Schedule\n",
" TIME_SLOTS = {\n",
" 'Monday:08:00-09:30': 1.5,\n",
" 'Monday:09:45-11:15': 1.5,\n",
" 'Monday:11:30-12:30': 1,\n",
" 'Monday:13:30-15:30': 2,\n",
" 'Monday:15:45-17:15': 1.5,\n",
" 'Tuesday:08:00-09:30': 1.5,\n",
" 'Tuesday:09:45-11:15': 1.5,\n",
" 'Tuesday:11:30-12:30': 1,\n",
" 'Tuesday:13:30-15:30': 2,\n",
" 'Tuesday:15:45-17:15': 1.5,\n",
" 'Wednesday:08:00-09:30': 1.5,\n",
" 'Wednesday:09:45-11:15': 1.5,\n",
" 'Wednesday:11:30-12:30': 1,\n",
" 'Thursday:08:00-09:30': 1.5,\n",
" 'Thursday:09:45-11:15': 1.5,\n",
" 'Thursday:11:30-12:30': 1,\n",
" 'Thursday:13:30-15:30': 2,\n",
" 'Thursday:15:45-17:15': 1.5,\n",
" 'Friday:08:00-09:30': 1.5,\n",
" 'Friday:09:45-11:15': 1.5,\n",
" 'Friday:11:30-12:30': 1,\n",
" 'Friday:13:30-15:30': 2,\n",
" 'Friday:15:45-17:15': 1.5,\n",
" }\n",
"\n",
" problem = SchoolSchedulingProblem(LEVELS, SECTIONS, SUBJECTS, CURRICULUM,\n",
" TEACHERS, SPECIALTIES, TIME_SLOTS)\n",
" solver = SchoolSchedulingSatSolver(problem)\n",
" solver.solve()\n",
"\n",
"\n",
"main()\n",

1
examples/notebook/graph/balance_min_flow.ipynb
View File

@@ -128,7 +128,6 @@
" status = smcf.solve()\n",
"\n",
" if status == smcf.OPTIMAL:\n",
" smcf.solve()\n",
" print('Total cost = ', smcf.optimal_cost())\n",
" print()\n",
" for arc in range(smcf.num_arcs()):\n",

2
examples/notebook/graph/simple_min_cost_flow_program.ipynb
View File

@@ -109,7 +109,7 @@
" start_nodes, end_nodes, capacities, unit_costs)\n",
"\n",
" # Add supply for each nodes.\n",
" smcf.set_nodes_supply(np.arange(0, len(supplies)), supplies)\n",
" smcf.set_nodes_supplies(np.arange(0, len(supplies)), supplies)\n",
"\n",
" # Find the min cost flow.\n",
" status = smcf.solve()\n",

1
examples/notebook/linear_solver/simple_lp_program.ipynb
View File

@@ -109,6 +109,7 @@
" # Maximize x + 10 * y.\n",
" solver.Maximize(x + 10 * y)\n",
"\n",
" print(f'Solving with {solver.SolverVersion()}')\n",
" status = solver.Solve()\n",
"\n",
" if status == pywraplp.Solver.OPTIMAL:\n",

3
examples/notebook/linear_solver/simple_mip_program.ipynb
View File

@@ -87,7 +87,7 @@
"\n",
"def main():\n",
" # Create the mip solver with the SCIP backend.\n",
" solver = pywraplp.Solver.CreateSolver('SCIP')\n",
" solver = pywraplp.Solver.CreateSolver('SAT')\n",
" if not solver:\n",
" return\n",
"\n",
@@ -109,6 +109,7 @@
" # Maximize x + 10 * y.\n",
" solver.Maximize(x + 10 * y)\n",
"\n",
" print(f'Solving with {solver.SolverVersion()}')\n",
" status = solver.Solve()\n",
"\n",
" if status == pywraplp.Solver.OPTIMAL:\n",

6
examples/notebook/sat/nqueens_sat.ipynb
View File

@@ -124,7 +124,8 @@
" model = cp_model.CpModel()\n",
"\n",
" # Creates the variables.\n",
" # The array index is the column, and the value is the row.\n",
" # There are `board_size` number of variables, one for a queen in each column\n",
" # of the board. The value of each variable is the row that the queen is in.\n",
" queens = [\n",
" model.NewIntVar(0, board_size - 1, 'x%i' % i) for i in range(board_size)\n",
" ]\n",
@@ -133,9 +134,6 @@
" # All rows must be different.\n",
" model.AddAllDifferent(queens)\n",
"\n",
" # All columns must be different because the indices of queens are all\n",
" # different.\n",
"\n",
" # No two queens can be on the same diagonal.\n",
" model.AddAllDifferent(queens[i] + i for i in range(board_size))\n",
" model.AddAllDifferent(queens[i] - i for i in range(board_size))\n",