Propositional Logic
Table of Contents
This assignment is to be done individually. You can talk to other people in the class, me (Dave), the prefect, and lab assistants for ideas and to gain assistance. You can help each other debug programs, if you wish. The code that you write should be your own, however, and you shouldn’t hand a printout of your program to others. See the course syllabus for more details or just ask me if I can clarify.
Part 1: Deduction with propositional logic, by hand
Read sections 1 through 7 of this handout on the Clue project, though this assignment is just a warmup relating to propositional logic. In section 7 of the handout, do exercise 2. Solve via resolution and turn in on paper or with an electronic document.
Grading
Meets expectations: you have followed instructions (a)-(c) from the handout, and you have done so correctly for this problem. A very minor error that doesn’t affect the outcome of the problem might be present.
Exemplary: meets expectations, plus there are no errors at all, and your submission is exceedingly clear. Your submission is organized and laid out clearly so that the grader can easily see how the steps follow. If you have done it by hand, your handwriting is neat. if you have done it electronically, you have taken the effort lay it out well. (That’s true whether you’ve done so by hand or electonically, but it’s more work to do that electonically than by hand.)
Part 2: Deduction with propositional logic, with software
Redo the exercise from the previous part, but solve with SATSolver.py and turn in your code.
Note that the above code requires both the software cryptominisat, as well as the Python bindings. Installing this on your own computer can be cumbersome, and is likely not worth the effort. We have installed cryptominisat, and the associated library (called pycryptosat) on the lab machines in Olin 310, and also on the department computer mantis. So you can remotely connect to mantis and run your code there, or you can work in Olin 310. Here are instructions on doing remote development with VSCode.
If you are determined to try to make this work on your own computer, you are welcome to try. Here are some outdated instructions. I’m happy to try updating them if you wish to post to Slack modifications as need be. Mac OS X in particular seems to be especially challenging, as different versions of OS X keep moving and/or not including necessary libraries. Mike Tie spent significant time getting it installed in out labs.
Submit your work in a file named truthteller.py. We should be able to drop your code in the same directory as out SATSolver.py, run python truthteller.py, and see the output of your code and be able to make sense of it.
Grading
Meets expectations: Your code correctly sets up the problem and correctly utilizes SATSolver.py in order to determine the truthfulness of the three people in the problem. A very minor error that doesn’t affect the outcome of the problem might be present.
Exemplary: meets expectations, plus your code does what it should do to solve the problem without excessive complexity or unnecessary actions. Your code should not merely print out True/False (for example), but will clearly print messages indicating what it all means.