#| CS 2800 Homework 4 - Spring 2019 This homework is done in groups. * Groups should consist of 2-3 people. * One group member will create a group in BlackBoard. See the class Webpage for instructions on how to do that. * Other group members then join the group. * Homework is submitted by only one person per group. Therefore make sure the person responsible for submitting actually does so. If that person forgets to submit, your team gets 0. - We recommend that groups email confirmation messages and submit early and often. * Submit the homework file (this file) on Blackboard. Do not rename this file. There will be a 10 point penalty for this. When done, save your file and submit it as hwk04.lisp. * You must list the names of ALL group members below, using the given format. This way we can confirm group membership with the BB groups. If you fail to follow these instructions, it costs us time and it will cost you points, so please read carefully. The format should be: FirstName1 LastName1, FirstName2 LastName2, ... For example: Names of ALL group members: Frank Sinatra, Billy Holiday There will be a 10 pt penalty if your names do not follow this format. Replace "..." below with the names as explained above. Names of ALL group members: ... * Later in the term if you want to change groups, the person who created the group should stay in the group. Other people can leave and create other groups or change memberships. See the class Webpage. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; For this homework you will need to use ACL2s. Technical instructions: - Open this file in ACL2s. - Make sure you are in ACL2s mode. This is essential! Note that you can only change the mode when the session is not running, so set the correct mode before starting the session. - Insert your solutions into this file where indicated (usually as "..."). Sometimes we require textual explanations (e.g., complexity analysis below) so just add your explanation inside the ACL2s comments. - Only add to the file. Do not remove or comment out anything pre-existing. - Make sure the entire file is accepted by ACL2s. In particular, there must be no "..." left in the code. If you don't finish all problems, comment the unfinished ones out. Comments should also be used for any English text that you may add. This file already contains many comments, so you can see what the syntax is. We will deduct points for files that are not accepted by ACL2s: we sometimes ask explicitly to insert your answer in the comments, when the answer is not to be accepted by ACL2s. When asked to insert your answer in the comments, do so. - Do not submit the session file (which shows your interaction with the theorem prover). This is not part of your solution. Only submit the lisp file. Instructions for programming problems: For each function definition, you must provide both contracts and a body. You must also ALWAYS supply your own tests. This is in addition to the tests sometimes provided. Make sure you produce sufficiently many new test cases. This means: cover at least the possible scenarios according to the data definitions of the involved types. For example, a function taking two lists should have at least 4 tests: all combinations of each list being empty and non-empty. Beyond that, the number of tests should reflect the difficulty of the function. For very simple ones, the above coverage of the data definition cases may be sufficient. For complex functions with numerical output, you want to test whether it produces the correct output on a reasonable number of inputs. Use good judgment. For unreasonably few test cases we will deduct points. We use the following ASCII character combinations to represent the Boolean connectives: NOT ~ AND /\ or & OR \/ or + IMPLIES => EQUIV <=> XOR >< or XOR The binding powers of these functions are listed from highest to lowest in the above table. Within one group (no blank line), the binding powers are equal. This is the same as in class. |# #| PART I: PROPOSITIONAL LOGIC BASICS A. Construct the truth table for the following Boolean formulas. Use alphabetical order for the variables in the formula, and create columns for all variables occurring in the formula AND for all intermediate subexpressions. For example, if your formula is (p => q) \/ r your table should have 5 columns: for p, q, r, p => q, and (p => q) \/ r . For each formula, you also have to: B. Indicate if is satisfiable, unsatisfiable, valid, or falsifiable (exactly two of these characterizations will hold!). C. Indicate how many assignments satisfy the formula (i.e., make the formula true). D. Simplify the formula: provide an alternative formula that is equivalent to the original formula and show equivalence by constructing a truth table for your formula whose final column has to be equal to the final column of the original truth table. If you wind up simplifying away a variable, include it in the truth table anyway so that you can compare the new truth table with the previous one. Your simplification should be minimal: that is, the number of symbols in your simplification should be as small as possible. If the formula cannot be simplified, write "cannot be simplified". E. Write a test? stating that the original formula and the simplified formula are equivalent. This should *not* be in a comment. ACL2s includes a decision procedure for validity, so you can use it as a SAT/validity solver to check your work. For example, you can use it to check your characterization of formulas (part B, above). Example question: p & (q + ~q) A: (Notice that we place T's and F's under the operator associated with the column, e.g., in the final column, we are taking a conjunction.) p | q | ~q | q + ~q | p & (q + ~q) ----------------------------- T | T | F | T | T T | F | T | T | T F | T | F | T | F F | F | T | T | F B: satisfiable and falsifiable C: 2 D: p p | q | p ---------- T | T | T T | F | T F | T | F F | F | F E: |# (thm (implies (and (booleanp p) (booleanp q)) (equal (and p (or q (not q))) p))) #| Question I.1: ~p => (p => (p => q)) ; Answers: A: ... B: ... C: ... D: ... E |# (thm (... #| Question I.2: (p \/ q) /\ (~p \/ q) /\ ~q ; Answers: A: ... B: ... C: ... D: ... E |# (thm (... #| Question I.3: Consider the boolean formula p <=> q <=> r and notice that there are multiple ways to parse the above formula that are consistent with out binding rules: (a) (p <=> q) <=> r (b) p <=> (q <=> r) Prove, using the truth table method, that <=> is associative, meaning that formulas (a) and (b) are equivalent. That is, your truth table should have columns for both formulas (a) and (b) above and their corresponding columns should be identical. Also answer questions A, B, C (but not D) as in the previous problems. ;Answers: A: ... B: ... C: ... |# #| I.4. Also prove using ACL2s that the formulas (a) and (b) from problem I.3 above are equivalent. Use iff for Boolean equality. |# ;answer: (thm (... #| I.5. Simplify each of the Boolean formulas below. That is, for each formula f, find an equivalent formula g, such that g is as simple as possible, meaning as short as possible. Use "0" and "1" for the constant expressions "true" and "false". You can use any of the simplification rules from Section 3.3 in the lecture notes. You don't have to state which rule you are using, but perform the simplification step by step. Example: p & (p & q) = (p & p) & q = p & q I.5.1: (p & q) => p answer: ... I.5.2: p => ((p => q) => q) answer: ... I.5.3: ~p => ~((p + q) & ~q) answer: ... I.5.4: ((p => q) & q) => ((p => q) & (p => r)) answer: ... I.5.5: (p XOR q) & (p => q) & (~q + p) answer: ... |# #| PART II: a SAT solver We will build a rudimentary SAT solver. A SAT solver is a tool that takes as input propositional logic formulas, and checks whether they are satisfiable or not. We begin by defining data types to represent our formulas: |# (defdata UnaryOp '~) (defdata BinOp (enum '(& + => <=> ><))) (defdata PropEx (oneof boolean var (list UnaryOp PropEx) (list PropEx Binop PropEx))) ; here's some examples of valid and invalid formulas: (check= (PropExp '(x & y)) t) (check= (PropExp '((~ x) & y)) t) (check= (PropExp '((~ x) <=> (y >< z))) t) (check= (PropExp '(~x)) nil) (check= (PropExp '(~ x)) t) #| II.1. Give at least 10 more examples of valid formulas and 10 examples of invalid formulas: |# ; (check= (PropExp ... ) t) ; (check= (PropExp ... ) nil) #| II.2. Our functions below will rely on knowing what the set of variables ("var"s) in a formula is. Define the data type "lov" (for list of variables) that represents such a set as a list of var: |# ;answer: (defdata lov ... #| II.3. Before proceeding, we will define two helper functions that we'll need below. First, define the function is-in-list which takes a true list l and an object x and checks whether x is in l: |# ;answer: (definec is-in-list (l :tl x :all) :boolean ... (check= (is-in-list '(1 2 3) 0) nil) (check= (is-in-list '(1 2 3) 1) t) #| Next, we define the function list-union which takes two true lists l1 and l2 and returns a true list l which contains the union of all the elements of l1 and l2. Note that list-union removes duplicates, so if an element of l1 is already in l2, it is not added a second time in the union. (However, if l2 already has duplicates these are not removed.) |# (definec list-union (l1 :tl l2 :tl) :tl (cond ((endp l1) l2) ((is-in-list l2 (first l1)) (list-union (rest l1) l2)) (t (list-union (rest l1) (cons (first l1) l2))))) (check= (list-union '(1 2 3) '(2 3 4)) '(1 2 3 4)) (check= (list-union '(1 2 3 7) '(1 2 3 3)) '(7 1 2 3 3)) #| For the remainder of this homework we switch to program mode. Otherwise ACL2s might take a long time and/or fail to prove things. Feel free to stay in logic mode and complete the homework in logic mode if you want to. However, please make sure your file is processed by ACL2s in a reasonable amount of time (a few minutes). |# :program #| II.4. Now define the function set-of-vars which takes as input a formula f and returns a lov representing the set of variables appearing in f. Notice that the returned list must be a set, meaning that duplicate elements are not allowed. That is, each var appearing in the formula must appear only once in the list of vars. Hint: you can use the function list-union defined above. |# ;answer: (definec set-of-vars ... (check= (set-of-vars '((~ t) + t)) nil) (check= (set-of-vars '(x & y)) '(x y)) (check= (set-of-vars '(~ (x & (y & z)))) '(x y z)) (check= (set-of-vars '(x & x)) '(x)) #| II.5. Define the function eval-varfree-formula which takes as input a formula f and evaluates it. We require that f has no variables, that is, the set of variables of f must be empty. Therefore f can only contain constants (t or nil) or boolean operators. Evaluating f results in t or nil, so eval-varfree-formula returns t or nil (a boolean). |# ;answer: (defunc eval-varfree-formula ... (check= (eval-varfree-formula '((~ t) + t)) t) (check= (eval-varfree-formula '(t & t)) t) (check= (eval-varfree-formula '(~ (t & (t & t)))) nil) #| II.6. Define the function sbst (for "substitute") which takes a formula f, a variable x, and a boolean value v (t or nil) and returns a new formula g, such that all occurrences of x in g have been replaced by v. The variable x may appear one time or many times in f. It may also not appear at all in f. All these are legal inputs for sbst. What is certain is that x must not appear in g. |# ;answer: (definec sbst ... ... (check= (sbst '(~ (x & (y & z))) 'x t) '(~ (t & (y & z)))) (check= (sbst '(~ (x & (y & x))) 'x t) '(~ (t & (y & t)))) (check= (sbst '(~ (x & (y & z))) 'w t) '(~ (x & (y & z)))) #| II.7. Define the function sat? (for "satisfiable ?") which takes a formula f and checks whether f is satisfiable. Hint: Follow the following pattern in your definition of sat?: if f has no variables, then we can simply evaluate f using the function eval-varfree-formula defined above; otherwise, we can pick one variable x appearing in f and: try to replace x with t (true) and check whether the resulting formula (call it f1) is satisfiable; try to replace x with nil (false) and check whether the resulting formula (call it f2) is satisfiable; if either f1 or f2 are satisfiable, then f must be satisfiable; if both f1 and f2 are unsatisfiable, then so must be f. Note: we recommend that you follow the above pattern, but you don't have to. You are free to define sat? in a different way if you want to. |# ;answer: (definec sat? (f :PropEx) :boolean ... (check= (sat? '(x & y)) t) (check= (sat? '(x & (~ x))) nil) #| II.8. Define using defconst 10 different satisfiable formulas, and 10 different unsatisfiable formulas, and test your sat? function on these 20 formulas: |# ;answer: ... #| II.9. How powerful is your SAT solver? Put it to the test by generating some large formulas and trying to check them using sat?. You can generate large formulas by hand, or by writing a program (in ACL2s or in your favorite programming language) to generate such formulas automatically. For example, you can write a program that takes as input a natural number n and generates a formula with n variables. We will not look at nor grade your formula generation code, so please do not submit it. Write below in the comments the largest formula that your sat? implementation was able to check in a reasonable amount of time (<1 min). Write also a formula whose checking time exceeded that amount (>1 min). For each of the two formulas, write how many propositional variables each has: ... Large formula which checks in <1 min ... : ... Above formula has ... variables. ... Large formula which doesn't check in <1 min ... : ... Above formula has ... variables. |# ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Part III: Feedback (5 points) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; #| Each week we will ask a few questions to monitor how the course is progressing and to solicit suggestions for improvement. Please fill out the following form. https://docs.google.com/forms/d/e/1FAIpQLSd0SoOi44dHM9ESI0LKvccZpQylYHTUwgYuz9exA5owel20-w/viewform?usp=sf_link Feedback is anonymous and each team member should fill out the form (only once per person). After you fill out the form, write your name below in this file, but not on the questionnaire. We have no way of checking if you submitted the file, but by writing your name below you are claiming that you did, and we'll take your word for it. The questionnaire is worth 5 points (hence the rest of the homework problems are worth 95 points). The following team members filled out the feedback survey provided by the link above (replace the ...'s with the names of the team members who filled out the questionnaire). --------------------------------------------- ... |#