{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"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": 2,
"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": 3,
"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": 4,
"metadata": {},
"outputs": [],
"source": [
"def get_all_vars(formula):\n",
" \"\"\"Return a set of all variables in the provided logical formula.\"\"\"\n",
" return {var for clause in formula for var, boolean in clause}"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"{'Adam', 'Rami', 'Srini', 'Subby', 'Áron'}"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"get_all_vars(formula)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Check if we have a solution"
]
},
{
"cell_type": "code",
"execution_count": 6,
"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": 7,
"metadata": {},
"outputs": [],
"source": [
"def is_full_solution(formula, assignments):\n",
" \"\"\"Return True if the assignments satisfy the formula, false otherwise.\"\"\"\n",
" for clause in formula:\n",
" for var, boolean in clause:\n",
" # if literal evaluates to True, clause evaluates to True\n",
" if var in assignments and assignments[var] == boolean:\n",
" break\n",
" # otherwise, literal either isn't assigned or evaluates to False, so try next literal\n",
"\n",
" else:\n",
" # no break: if we don't break out of the for loop,\n",
" # none of the literals in the clause evaluated to True,\n",
" # so the clause evaluates to False\n",
" return False\n",
" # if we get through the whole formula without returning False,\n",
" # all the clauses must have evaluated to True, so the formula is True\n",
" return True\n",
"\n",
" # Equivalent code\n",
" #return all(any(var in assignments and assignments[var] == boolean for var, boolean in clause) for clause in formula)"
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"is_full_solution(formula, assignments1)"
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"False"
]
},
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"is_full_solution(formula, assignments2)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Find a solution"
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [],
"source": [
"def satisfying_assignment(formula, assignments=None):\n",
" \"\"\"Return a variable assignment dictionary if the formula can be satisfied, None otherwise.\"\"\"\n",
" \n",
" # Set up mutable default argument.\n",
" if assignments is None:\n",
" assignments = {}\n",
" \n",
" # If assignments satisfies the formula, return the assignments as they are.\n",
" if is_full_solution(formula, assignments):\n",
" return assignments\n",
" \n",
" all_variables = get_all_vars(formula)\n",
" \n",
" # If all variables have been assigned (but the assignment does not satisfy the formla), return None.\n",
" if len(assignments) == len(all_variables):\n",
" return None\n",
"\n",
" # Find the next unassigned variable, which we'll call test_var.\n",
" unassigned_variables = all_variables - assignments.keys()\n",
" test_var = unassigned_variables.pop()\n",
"\n",
" # High level idea: we can do a case analysis. there are only two cases:\n",
" # test_var has to be either True or False (we can draw a tree of the cases to see this).\n",
"\n",
" # Approach: Try test_var True, then False for some unassigned variable.\n",
" for boolean in (True, False):\n",
" assignments_attempt = satisfying_assignment(formula, {**assignments, test_var: boolean})\n",
"\n",
" if assignments_attempt is not None and is_full_solution(formula, assignments_attempt):\n",
" return assignments_attempt\n",
"\n",
" # Formula is unsatisfiable.\n",
" return None\n"
]
},
{
"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": 11,
"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": 12,
"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": 13,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"{'Subby': False,\n",
" 'Srini': False,\n",
" 'pickles': True,\n",
" 'Áron': True,\n",
" 'chocolate': True,\n",
" 'Rami': False,\n",
" 'Adam': False,\n",
" 'vanilla': False}"
]
},
"execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
],
"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
}