Computer Science 242

Homework 1

You are asked to write a program which solves propositional satisfiability problems by simply iterating through all possible assignments.

A formula of the propositional calculus is considered satisfiable if there exists some interpretation of the atoms where the formula is true under that interpretation. All formulas are either satisfiable or unsatisfiable. For example, the formula "A" is satisfiable. It is true under any interpretation that assigns the atom A to be true. In contrast, the formula "A ∧ ¬ A" is not satisfiable ‐ there is no way we can choose a truth value for the atom A such that both A and its negation are true.

The input to your program will be a propsitional formula expressed as a set of clauses in conjunctive normal form. You will be presented with one clause per line, where the clauses are given as comma separated literals.

A literal is either an atom or a negated atom. Atoms may be any string that does not contain whitespace or the comma symbol. (Practically speaking we will test your code with atoms consisting of a letter possibly followed by some digits.) The negation symbol is the tilde character: ~. An example input problem is given below:

A,B,C
~B,D
C,~A,F,E
~F
This means (A ∨ B ∨ C) ∧ (¬B ∨ D) ∧ (C ∨ ¬A ∨ F ∨ E) ∧ (¬F). There are no restrictions on the number of literals per clause or the number of clauses. A given literal may appear multiple times in a single clause. A given atom may appear both as a positive literal and a negative literal in the same clause. For example, the following clauses are also allowed as input:
A,A,A
A,B,~A,C,~B,A
Your program should read a set of clauses from standard input, and print the result to standard output in the format shown below. You are allowed to use Python or Java. Your program should be an executable file named sat, and should run exactly as shown in the example below on your instructional account:
% cat /u/cs242/hw1/sat-problem1.txt
A,B
~B,C
% ./sat < /u/cs242/hw1/sat-problem1.txt
satisfiable A=T B=F C=T
% cat /u/cs242/hw1/sat-problem2.txt
A
~A
% ./sat < /u/cs242/hw1/sat-problem2.txt
unsatisfiable	  
	  

The smoke_test script can be used to check the format of your program. The smoke_test script takes the name of a submission directory as a command line argument, and runs the two test cases shown above.

  /u/cs242/hw1/smoke_test ./hw1
...  
  Test cases passed: 2/2 | Score: 100.0%