HW#3 --- last modified October 27 2022 00:42:47.

Solution set.

Due date: Nov 2

Files to be submitted:
  Hw3.zip

Purpose: To become familiar with constraint satisfaction problem algorithm, to experiment with logical reasoning agents.

Related Course Outcomes:

CLO 3 - Apply forward checking in constraint satisfaction problems.

CLO 5 - Translate sentences in first-order logic to conjunctive normal form (CNF).

CLO 6 - Find proofs by using resolution.

Specification:

This homework will consist of two parts: Some written questions and a coding part. You are to write up your written questions in a file Hw3.pdf which you include as part of the zip file. Make sure to list all group members and their IDs at the top of this file. Here are the written questions:

1. Consider the statements about a possible Wumpus world:
   1. `neg W_{1,1}`
   2. `S_{1,1} <=> (W_{1,2} vv W_{2,1})`
   3. `S_{1,2} <=> (W_{1,1} vv W_{2,2} vv W_{1,3})`
   4. `S_{2,1} <=> (W_{1,1} vv W_{2,2} vv W_{3,1})`
   5. `neg S_{1,1}`
   6. `neg W_{1,2}`
   7. `neg W_{2,1}`
   8. `neg S_{1,2}`
   9. `S_{2,1}`
   Give a natural deduction proof of `W_{3,1}` from the above.
2. (a) Write down the true table for `A = MIN(A,B,C)` where `A,B,C` are propositional variables. (b) express `A = MIN(A,B,C)` as conjunctive normal form formula using the procedure from class.
3. Give a resolution refutation for the set of clauses `{{A}, {bar{C}}, {bar{A}, D, C}, {bar{B}, C}, {bar{A}, bar{D}} }` using the brute force algorithm from class Oct 26.

For the programming portion of this assignment, you are to write a CSP solver which will be run from the command line with a syntax like:

python csp_solver.py problem_filename use_forward_check_flag

Here problem_filename is the name of some text file containing a CSP using the syntax we now describe. use_forward_check_flag is either 1 or 0 and determines whether forward checking is used. A legal file consists of a domain line followed by a sequence of constraint lines.

A domain line consists of sequence of colon separated integers . For example,

2:1:5

Domains are read left-to-right, the first integer represents the domain of variable `X_0`, the second integer, domain of `X_1`, etc. If the last integer listed was at the `i`th position, then it represents the domain of `X_{i-1}` as well as the domain of `X_j` for `j \geq i`. In the above, the 2 indicates the domain of `X_0` is {0,1}, the 1 indicates the domain of `X_1` is {0}, the five indicate the domain of `X_j` where `j \geq 2` is {0, 1, 2, 3, 4}. A constraint line has the format:

Linear_Expression Rel Var_Or_Integer

Here Linear_Expression can be of the form:

Integer * Var + Integer

Integer is any integer number ..., -2, -1, 0, 1, 2, ... , a Var consists of the letter X followed by a natural number, Rel is either ==, !=, <=, >=, <, or > and Var_Or_Integer is either a variable or an integer.

Below is an example input file for the csp_solver.py:

3:3
1 * X0 + 0 > 0
1 * X1 + 0 > 0
-1 * X0 + 3 < X1

If there is at least one solution to the constraint satisfaction problem in problem_filename, then you program should output one possible solution. To do this it list values for each variable, one to a line, the first line, gives the value of `X_0`, the second line gives the value of `X_1`, etc. For example, on the above input your program should output (as there is only one solution):

2
2

The output of your program should be "NO SOLUTION" if the CSP does not have a solution. To find solutions, your program should run the backtracking procedure described in class. SELECT-UNASSIGNED VARIABLES should implement the MRV and degree heuristics, ORDER-DOMAIN-VALUES should implement the least-constraining-value heuristic. INFERENCES should either return the empty assignment or should do forward checking depending on the command line option. You should include the test files you create for this homework in the ZIP folder. At least one of these test files should be a formulation of the map coloring of Australia problem from the book where we let red = 0, green = 1, blue = 2 and you suitable describe in your experiment write-up how states names map to variable names. At least one other of these test files should be the example above. You should conduct some experiments related to the effectiveness and overhead of forward checking. Write these up in a file Experiments.pdf which you also include in your ZIP file.

Point Breakdown