Logical Pacman,

Food is good AND ghosts are bad,

Spock would be so proud

TABLE OF CONTENTS

• Introduction

• The Expr Class

• A note on conjoin and disjoin

• Prop Symbol Names (Important!)

• Rules

• Pacphysics symbols

• SAT Solver Setup

• Question 1 (2 points): Logic Warm-up

• Question 2 (2 points): Logic Workout

• Question 3 (4 points): Pacphysics and Satisfiability

• Question 4 (3 points): Path Planning with Logic

• Question 5 (3 points): Eating All the Food

• Helper Functions for the rest of the Project

• Add pacphysics, action, and percept information to KB

• Find possible pacman locations with updated KB

• Find provable wall locations with updated KB

• Question 6 (4 points): Localization

• Question 7 (3 points): Mapping

• Question 8 (4 points): SLAM

• Submission

Introduction

n this project, you will use/write simple Python functions that generate logical sentences describing Pacman physics, aka pacphysics. Then you will use a SAT solver, pycosat, to solve the logical inference tasks associated with planning (generating action sequences  to reach goal locations and eat all the dots), localization (finding oneself in a map, given a local sensor model), mapping (building the map from scratch), and SLAM (simultaneous localization and mapping).

As in previous programming assignments, this assignment includes an autograder for you to grade your answers on your machine. This can be run with the command:

python autograder.py

Copy

The code for this project contains the following files, available as a zip archive.

Files you'll edit:

The main file that runs Pacman games.

Utility functions for  logic.py .

Utility functions primarily for other projects.

Project specific autograding test classes.

Graphics for Pacman.

Support for Pacman graphics.

ASCII graphics for Pacman.

Agents to control ghosts.

Keyboard interfaces to control Pacman.

Code for reading layout files and storing their contents.

Project autograder.

Parses autograder test and solution files.

General autograding test classes.

Files to Edit and Submit: You will fill in portions of  logicPlan.py during the assignment. Once you have completed the assignment, you will submit these files to Gradescope (for instance, you can zip the entire project folder). Please do not change the other files in     this distribution.

Evaluation: Your code will be autograded for technical correctness. Please do not change the names of any provided functions or classes within the code, or you will wreak havoc  on the autograder. However, the correctness of your implementation – not the autograder’s judgements – will be the final judge of your score. If necessary, we will        review and grade assignments individually to ensure that you receive due credit for your work.

Academic Dishonesty: We will be checking your code against other submissions in the class for logical redundancy. If you copy someone else’s code and submit it with minor changes, we will know. These cheat detectors are quite hard to fool, so please don’t try. We trust you all to submit your own work only; please don’t let us down. If you do, we  will pursue the strongest consequences available to us.

Getting Help: You are not alone! If you find yourself stuck on something, contact the      course staff for help. Office hours, section, and the discussion forum are there for your    support; please use them. If you can’t make our office hours, let us know and we will       schedule more. We want these projects to be rewarding and instructional, not frustrating and demoralizing. But, we don’t know when or how to help unless you ask.

Discussion: Please be careful not to post spoilers.

The Expr Class

In the first part of this project, you will be working with the  Expr class defined in

logic.py to build propositional logic sentences. An  Expr object is implemented as a tree with logical operators (∧, V, ¬, →, ↔) at each node and with literals (A, B, C) at the leaves. Here is an example sentence and its representation:

(A ∧ B) ↔ (¬C V D)

To instantiate a symbol named  'A' , call the constructor like this:

A = Expr('A')

The  Expr class allows you to use Python operators to build up these expressions. The following are the available Python operators and their meanings:

•    ~A : ¬A

•    A & B : A ∧ B

•    A | B : A V B

•    A >> B : A → B

•    A % B : A ↔ B

So to build the expression A ∧ B, you would type this:

A = Expr('A')                                                                    Copy

B = Expr('B')

a_and_b = A & B

(Note that  A to the left of the assignment operator in that example is just a Python variable name, i.e.  symbol1 = Expr('A') would have worked just as well.)

A note on conjoin and disjoin

One last important thing to note is that you must use  conjoin and  disjoin operators    wherever possible.  conjoin creates a chained  & (logical AND) expression, and  disjoin creates a chained  | (logical OR) expression. Let’s say you wanted to check whether        conditions A, B, C, D, and E are all true. The naive way to achieve this is writing  condition = A & B & C & D & E , but this actually translates to  ((((A & B) & C) & D) & E) , which       creates a very nested logic tree (see (1) in diagram below) and becomes a nightmare to  debug. Instead,  conjoin makes a flat tree (see (2) in diagram below).

Prop Symbol Names (Important!)

For the rest of the project, please use the following variable naming conventions:

Rules

•   When we introduce variables, they must start with an upper-case character (including Expr ).

•   Only these characters should appear in variable names:  A-Z ,  a-z ,  0-9 ,  _ ,  ^ ,  [ ,  ] .

•   Logical connective characters ( & ,  | ) must not appear in variable names. So,  Expr('A & B') is illegal because it attempts to create a single constant symbol named  'A &  B' . We would use  Expr('A') & Expr('B') to make a logical expression.

Pacphysics symbols

•    PropSymbolExpr(pacman_str, x, y, time=t) : whether or not Pacman is at (x, y) at time t, writes  P[x,y]_t .

•    PropSymbolExpr(wall_str, x, y) : whether or not a wall is at (x, y), writes  WALL[x,y] .

•    PropSymbolExpr(action, time=t) : whether or not pacman takes action action at time t, where action is an element of  DIRECTIONS , writes i.e.  North_t .

•   In general,  PropSymbolExpr(str, a1, a2, a3, a4, time=a5) creates the expression str[a1,a2,a3,a4]_a5 where  str is just a string.

There is additional, more detailed documentation for the  Expr class in  logic.py .

SAT Solver Setup

A SAT (satisfiability) solver takes a logic expression which encodes the rules of the world and returns a model (true and false assignments to logic symbols) that satisfies that        expression if such a model exists. To efficiently find a possible model from an expression, we take advantage of the pycosat module, which is a Python wrapper around the picoSAT library.

Unfortunately, this requires installing this module/library on each machine. In the      command line, run  pip install pycosat , or  pip3 install pycosat on some setups, or

conda install pycosat for  conda .

On Windows, if you are getting an error message saying  error: Microsoft Visual C++    14.0 or greater is required. Get it with "Microsoft Build Tools": ... , you will have to   install a C/C++ compiler following that link; or, use  conda install pycosat , for which you will need to have Anaconda installed (recommend uninstalling current Python before installing a new one) and run this from the Anaconda prompt.

Testing  pycosat installation:

After unzipping the project code and changing to the project code directory, run:

python pycosat_test.py

Copy

This should output:

[1, -2, -3, -4, 5]

Copy

Please let us know if you have issues with this setup. This is critical to completing the      project, and we don’t want you to spend your time fighting with this installation process.

Question 1 (2 points): Logic Warm-up

This question will give you practice working with the  Expr data type used in the project

to represent propositional logic sentences. You will implement the following functions in logicPlan.py :

•    sentence1() : Create one  Expr instance that represents the proposition that the         following three sentences are true. Do not do any logical simplification, just put them in a list in this order, and return the list conjoined. Each element of your list should     correspond to each of the three sentences.

A V B

¬A ↔ (¬B V C)

¬A V ¬B V C

•    sentence2() : Create one  Expr instance that represents the proposition that the         following four sentences are true. Again, do not do any logical simplification, just put them in a list in this order, and return the list conjoined.

C ↔ (B V D)

A → (¬B ^ ¬D)

¬ (B ^ ¬C) → A

¬D → C

•    sentence3() : Using the  PropSymbolExpr constructor, create the symbols                        'PacmanAlive_0' ,  'PacmanAlive_1' ,  'PacmanBorn_0' , and  'PacmanKilled_0' (hint: recall that  PropSymbolExpr(str, a1, a2, a3, a4, time=a5) creates the expression

str[a1,a2,a3,a4]_a5 where  str is a string; you should make some strings for this    problem to match these exactly). Then, create one  Expr instance which encodes the following three English sentences as propositional logic in this order without any     simplification:

1   Pacman is alive at time 1 if and only if he was alive at time 0 and he was not killed at time 0 or he was not alive at time 0 and he was born at time 0.

2   At time 0, Pacman cannot both be alive and be born.

3   Pacman is born at time 0.

•    findModelUnderstandingCheck() :

1   Look at how the  findModel(sentence) method works: it uses  to_cnf to convert the input sentence into Conjunctive Normal Form (the form required by the SAT          solver), and passes it to the SAT solver to find a satisfying assignment to the          symbols in  sentence , i.e., a model. A model is a dictionary of the symbols in your  expression and a corresponding assignment of  True or  False . Test your                sentence1() ,  sentence2() , and  sentence3() with findModel by opening an            interactive session in Python and running  from logicPlan import * and                   findModel(sentence1()) and similar queries for the other two. Do they match what you were expecting?

2   Based on the above, fill in  findModelUnderstandingCheck so that it returns what  findModel(Expr('a')) would return if lower case variables were allowed. You     should not use  findModel or  Expr beyond what’s already given; simply directly recreate the output.

•    entails(premise, conclusion) : Return  True if and only if the  premise entails the        conclusion . Hint:  findModel is helpful here; think about what must be unsatisfiable in order for the entails to be  True , and what it means for something to be                      unstatisfiable.

•    plTrueInverse(assignments, inverse_statement) : Returns  True if and only if the (not inverse_statement ) is  True given  assignments .

Before you continue, try instantiating a small sentence, e.g. A ∧ B → C, and call  to_cnf on it. Inspect the output and make sure you understand it (refer to AIMA section 7.5.2 for details on the algorithm  to_cnf implements).

To test and debug your code run:

python autograder.py -q q1

Question 2 (2 points): Logic Workout

Implement the following three functions in  logicPlan.py (remembering to use  conjoin and  disjoin whenever possible):

•    atLeastOne(literals) : Return a single expression ( Expr ) in CNF that is true only if at least one expression in the input list is true. Each input expression will be a literal.

•    atMostOne(literals) : Return a single expression ( Expr ) in CNF that is true only if at  most one expression in the input list is true. Each input expression will be a literal. Hint: Use  itertools.combinations . If you have n literals, and at most one is true, your resulting CNF expression should be a conjunction of (2(n)) clauses.

•    exactlyOne(literals) : Use  atLeastOne and  atMostOne to return a single expression ( Expr ) in CNF that is true only if exactly one expression in the input list is true. Each input expression will be a literal.

Each of these methods takes a list of  Expr literals and returns a single  Expr expression  that represents the appropriate logical relationship between the expressions in the input list. An additional requirement is that the returned  Expr must be in CNF (conjunctive     normal form). You may NOT use the to_cnf function in your method implementations (or any of the helper functions  logic.eliminate_implications ,  logic.move_not_inwards ,    and  logic.distribute_and_over_or ).

Don’t run  to_cnf on your knowledge base when implementing your planning agents in later questions. This is because  to_cnf makes your logical expression much longer        sometimes, so you want to minimize this effect;  findModel does this as needed. In later questions, reuse your implementations for  atLeastOne(.) ,  atMostOne(.) , and

exactlyOne(.) instead of re-engineering these functions from scratch. This avoids accidentally making unreasonably slow non-CNF-based implementations.

You may utilize the  logic.pl_true function to test the output of your expressions.

pl_true takes an expression and a model and returns  True if and only if the expression is true given the model.

To test and debug your code run:

python autograder.py -q q2

Question 3 (4 points): Pacphysics and Satisfiability

In this question, you will implement the basic pacphysics logical expressions, as well as learn how to prove where pacman is and isn’t by building an appropriate knowledge   base (KB) of logical expressions.

Implement the following functions in  logicPlan.py :

•    pacmanSuccessorAxiomSingle – this generates an expression defining the sufficient and necessary conditions for Pacman to be at (x, y) at t:

•   Read the construction of  possible_causes provided.

•   You need to fill out the return statement, which will be an  Expr . Make sure to use disjoin and  conjoin where appropriate. Looking at  SLAMSuccessorAxiomSingle   may be helpful, although note that the rules there are more complicated than in  this function. The simpler side of the biconditional should be on the left for          autograder purposes.

•    pacphysicsAxioms – here, you will generate a bunch of physics axioms. For timestep t:

•   Arguments:

•   Required:  t is time,  all_coords and  non_outer_wall_coords are lists of (x, y) tuples.

•   Possibly- None : You will be using these to call functions, not much logic is required.

•    walls_grid is only passed through to  successorAxioms and describes (known) walls.

•    sensorModel(t: int, non_outer_wall_coords) -> Expr returns a single  Expr describing observation rules; you can take a look at  sensorAxioms and     SLAMSensorAxioms to see examples of this.

•    successorAxioms(t: int, walls_grid, non_outer_wall_coords) -> Expr

describes transition rules, e.g. how previous locations and actions of Pacman affect the current location; we have seen this in the functions in

pacmanSuccessorAxiomSingle .

•   Algorithm:

•   For all (x, y) in  all_coords , append the following implication (if-then form): if a wall is at (x, y), then Pacman is not at (x, y) at t.

•   Pacman is at exactly one of the  non_outer_wall_coords at timestep t.

•   Pacman takes exactly one of the four actions in  DIRECTIONS at timestep t.

•   Sensors: append the result of  sensorAxioms . All callers except for                         checkLocationSatisfiability make use of this; how to handle the case where we don’t want any sensor axioms added is up to you.

•   Transitions: append the result of  successorAxioms . All callers will use this.

•   Add each of the sentences above to  pacphysics_sentences . As you can see in the return statement, these will be conjoined and returned.

•   Function passing syntax:

•   Let  def myFunction(x, y, t): return PropSymbolExpr('hello', x, y, time=t) be a function we want to use.

•   Let  def myCaller(func: Callable): ... be the caller that wants to use a function.

•   We can pass the function in:  myCaller(myFunction) . Note that  myFunction is not called with  () after it.

•   We can use  myFunction by having inside  myCaller this:  useful_return = func(0, 1, q) .

•    checkLocationSatisfiability – given a transition  (x0_y0, action0, x1_y1) ,  action1 , and a  problem , you will write a function that will return a tuple of two models         (model1, model2) :

•   In  model1 , Pacman is at (x1, y1) at time t = 1 given  x0_y0 ,  action0 ,  action1 .

This model proves that it’s possible that Pacman there. Notably, if  model1 is  False , we know Pacman is guaranteed to NOT be there.

•   In  model2 , Pacman is NOT at (x1, y1) at time t = 1 given  x0_y0 ,  action0 ,          action1 . This model proves that it’s possible that Pacman is not there. Notably, if model2 is  False , we know Pacman is guaranteed to be there.