Assignment: For this two part lab you will create a program that Inputs and validates a 3CNF formula Checks the satisfiability of the 3CNF formula (optional) A formula is satisfiable: When there is some assignment of truth values to the variables in the formula that makes the formula come out true. For example, if the formula is ~A ^ (B v ~C) then the following assignments to A, B and C will make the formula true: F T T, F T F, F F F Here are a couple more examples: A ^ B ^ ~A is not satisfiable. (A v B) ^ (~A v B) ^ (~A v ~B) is only satisfiable by A = F, B = T. We will not be checking the satisfiability of just any formula - that would be too difficult! Instead, you can assume that the formula is in a very specific format: 3CNF. First of all, CNF stands for conjunctive normal form. Actually the final example above is in CNF; it means that there are a bunch of clauses (they are the things in the parentheses) with only OR's in each clause that are then ANDed together. The 3 in 3CNF means that there are exactly three variables in each clause. The example above must then be 2CNF, since there are two variables in each clause. Here's an example of a 3CNF formula: (A v B v ~A) ^ (A v B v ~B) ^ (~B v A v ~A) Please note that there are only TWO variables in the formula, but there are THREE in each clause. We could also have a 3CNF formula with any other number of clauses or variables in it. Here's one with two clauses and five variables: (~X v Y v Z) ^ (~W v Z v U) If you have any questions on satisfiability or the 3CNF format, please inquire before your start!!!