Your task in this assignment is to produce a working version of WalkSat and apply it to the Wumpus World domain. You should start with Peter Norvig's python repository for the book. The code in logic.py will give you a good starting point.
Satisfiability procedures like WalkSat take a set of clauses in CNF and return a model (an assignment of values to variables) if there is one, and fail if they no such assignment can be found. There are, therefore, three sources for the complete set of clauses that will be passed to WalkSat.
Details
Use the following conventions:
There are two places where you need to work on the WalkSat code. The first task is to implement the MinConflict heuristic that WalkSat uses to choose which symbol to flip. The second is that there's a logic flaw in the code concerning the type of the clauses variable.
In addition to getting the code working, the other large task involves coding the KB for the domain. You can use as much, or as little of, the code in logic.py. In particular, you don't have to use the KB class but you can if you want. Its a good idea to interactively fool around with the examples and code to see whats there and how it works.
Example
An example scenario would be something like this: the agent starts at [1,1], notes its sensor readings, and moves on based on what it concludes is reasonable. Say for example, the agent starts in [1,1] and detects no stench and no breeze (~S11, ~B11). From this it concludes that [2,1] is safe and moves there and detects a breeze (B21). At this point it might wonder if B31 is safe (or unsafe). One thing that makes something unsafe is the potential presence of a pit or a wumpus. So it might ask if P31 is satisfiable (yes), or if W31 is satisfiable (no).
In this example, the given dynamic information would be ~S11, ~B11, B21, ~S21, and a query to be satisfied would be P31.