{
"cells": [
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"# Avoid errors when executing notebook.\n",
"Adam = Srini = Rami = Subby = Áron = None\n",
"chocolate = vanilla = pickles = None"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Backtracking Search"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Many kinds of problems can only be solved using a trial-and-error approach. We usually have a set of constraints that help us decide if a proposed solution is valid. You saw some examples of this in lecture, for example the dinner invitation problem, or the n-queens problem. This is what we call backtracking search in computer science. We try a solution, and when we encounter an impossible situation in the process, we \"bactrack\" (go back to the last partial solution that worked) and try another solution."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Boolean (Logical) Satisfiability"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"A large class of problems can be formulated as \"logical equations,\" which can also be solved using backtracking search. There are many ways to state these problems, but we will adopt a common representation."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We have a set of variables that are either true of false, represented as keys in a dictionary. Let's introduce the operation NOT. This gives us literals, where a variable can either be in itself (_a_), or in a negated form (not *a*). We can combine these with the operation OR to get so-called \"clauses.\" Finally, if we connect these clauses, we arrive at our final \"formula.\""
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"clause1 = Adam or Srini\n",
"clause2 = not Rami or not Subby or not Áron\n",
"formula = (Adam or Srini) and (not Rami or not Subby or not Áron)"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"clause1 = [('Adam', True), ('Srini', True)]\n",
"clause2 = [('Rami', False), ('Subby', False), ('Áron', False)]\n",
"formula = [clause1, clause2]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Gather all variables in the formula"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"def get_all_vars(formula):\n",
" \"\"\"Return a set of all variables in the provided logical formula.\"\"\"\n",
" pass"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"get_all_vars(formula)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Check if we have a solution"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"assignments1 = {\n",
" 'Adam': False,\n",
" 'Srini': True,\n",
" 'Rami': False,\n",
"}\n",
"assignments2 = {\n",
" 'Rami': True,\n",
" 'Subby': True,\n",
" 'Áron': True,\n",
"}"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"def is_full_solution(formula, assignments):\n",
" \"\"\"Return True if the assignments satisfy the formula, false otherwise.\"\"\"\n",
" pass"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"is_full_solution(formula, assignments1)"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"is_full_solution(formula, assignments2)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Find a solution"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"def satisfying_assignment(formula, assignments=None):\n",
" \"\"\"Return a variable assignment dictionary if the formula can be satisfied, None otherwise.\"\"\"\n",
" pass"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Example problem: who ate the donuts?"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The 6.009 staff were pleased to learn that grateful alumni had donated donuts for last week's staff meeting. Unfortunately, the donuts were gone when the staff showed up for the meeting! Who ate the donuts?\n",
"1. The suspects are Adam, Srini, Rami, Subby, and Áron.\n",
"1. Whichever suspect ate any of the donuts must have eaten all of them.\n",
"1. The donuts included exactly two of the flavors chocolate, vanilla, and pickles.\n",
"1. Adam only eats pickles-flavored donuts.\n",
"1. Years ago, Rami and Subby made a pact that, whenever either of them eats donuts, he must share with the other one.\n",
"1. Srini feels strongly about flavor fairness and will only eat donuts if he can include at least 3 different flavors."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"rule1 = (Adam or Srini or Rami or Subby or Áron)\n",
"# At least one of them must have committed the crime! Here, one of these\n",
"# variables being True represents that person having committed the crime.\n",
"\n",
"\n",
"rule2 = ((not Adam or not Srini)\n",
" and (not Adam or not Rami)\n",
" and (not Adam or not Subby)\n",
" and (not Adam or not Áron)\n",
" and (not Srini or not Rami)\n",
" and (not Srini or not Subby)\n",
" and (not Srini or not Áron)\n",
" and (not Rami or not Subby)\n",
" and (not Rami or not Áron)\n",
" and (not Subby or not Áron))\n",
"# At most one of the suspects is guilty. In other words, for any pair of\n",
"# suspects, at least one must be NOT guilty (so that we cannot possibly find\n",
"# two or more people guilty)\n",
"# Together, rule2 and rule1 guarantee that exactly one suspect is guilty.\n",
"\n",
"\n",
"rule3 = ((not chocolate or not vanilla or not pickles)\n",
" and (chocolate or vanilla)\n",
" and (chocolate or pickles)\n",
" and (vanilla or pickles))\n",
"# Here is our rule that the cupcakes included exactly two of the flavors. Put\n",
"# another way: it can't be that all flavors were present, and among any pair of\n",
"# flavors, at least one was present.\n",
"\n",
"\n",
"rule4 = ((not Adam or pickles)\n",
" and (not Adam or not chocolate)\n",
" and (not Adam or not vanilla))\n",
"# If Adam is guilty, this will evaluate to True only if only pickles-flavored\n",
"# cupcakes were present. If Adam is not guilty, this will always evaluate to\n",
"# True. This is our way of encoding the fact that, if Adam is guilty, only\n",
"# pickles-flavored cupcakes must have been present.\n",
"\n",
"\n",
"rule5 = (not Rami or Subby) and (not Subby or Rami)\n",
"# If Rami ate cupcakes without sharing with Subby, the first case will fail to\n",
"# hold. Likewise for Subby eating without sharing. Since Rami and Subby only\n",
"# eat cupcakes together, this rule excludes the possibility that only one of\n",
"# them ate cupcakes.\n",
"\n",
"\n",
"rule6 = ((not Srini or chocolate)\n",
" and (not Srini or vanilla)\n",
" and (not Srini or pickles))\n",
"# If Srini is the culprit and we left out a flavor, the corresponding case here\n",
"# will fail to hold. So this rule encodes the restriction that Srini can only\n",
"# be guilty if all three types of cupcakes are present.\n",
"\n",
"\n",
"satisfied = rule1 and rule2 and rule3 and rule4 and rule5 and rule6"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"rule1 = [[('Adam', True), ('Srini', True), ('Rami', True),\n",
" ('Subby', True), ('Áron', True)]]\n",
"\n",
"rule2 = [[('Adam', False), ('Srini', False)],\n",
" [('Adam', False), ('Rami', False)],\n",
" [('Adam', False), ('Subby', False)],\n",
" [('Adam', False), ('Áron', False)],\n",
" [('Srini', False), ('Rami', False)],\n",
" [('Srini', False), ('Subby', False)],\n",
" [('Srini', False), ('Áron', False)],\n",
" [('Rami', False), ('Subby', False)],\n",
" [('Rami', False), ('Áron', False)],\n",
" [('Subby', False), ('Áron', False)]]\n",
"\n",
"\n",
"rule3 = [[('chocolate', False), ('vanilla', False), ('pickles', False)],\n",
" [('chocolate', True), ('vanilla', True)],\n",
" [('chocolate', True), ('pickles', True)],\n",
" [('vanilla', True), ('pickles', True)]]\n",
"\n",
"rule4 = [[('Adam', False), ('pickles', True)],\n",
" [('Adam', False), ('chocolate', False)],\n",
" [('Adam', False), ('vanilla', False)]]\n",
"\n",
"rule5 = [[('Rami', False), ('Subby', True)],\n",
" [('Subby', False), ('Rami', True)]]\n",
"\n",
"rule6 = [[('Srini', False), ('chocolate', True)],\n",
" [('Srini', False), ('vanilla', True)],\n",
" [('Srini', False), ('pickles', True)]]\n",
"\n",
"rules = rule1 + rule2 + rule3 + rule4 + rule5 + rule6"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"satisfying_assignment(rules)"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.7.2+"
}
},
"nbformat": 4,
"nbformat_minor": 2
}