----------- Apr 11, 2012 ------------ Hi I am not going to lecture anymore. I think it's time to focus 100% on projects. So no more lectures. OK one tiny subgoal ind. problem to think thru (basically my notes). So consulting - i.e. open-door - Monday next week on. I want you to take all the help. I will show up in class. This offers a setting for project consultations also. Peng and Geof, plz do come -- you can help students 1-1 that way. Also Tyler plz come along. So that means the lectures of 16, 18, 23, and 25 will be consulting time -- also the days around these dates also consulting time. I may walk you thru the Gordon Prover and Subgoal Induction prover on Apr 16th just because I told you I will. Hope you are happy with your project selections. If not, bug me. Projects due last day of the exam period -- which is May 3rd . Grades will be sent 1-1 in a few days after the projects are turned in. Ganesh ----------- Apr 9, 2012 ------------ Why do recursive functional programs define functions? 1) If all cases are covered, they don't define partial relations/functions 2) Assuming all cases are covered, here are the reasons: a) THE MOST OBVIOUS ANSWER: "if" is deterministic (usually sequentially evaluated). If we have overlapping conditions and an unordered "if" (almost like 'choose'), then we can obtain non-deterministic results (i.e. a relation) b) OTHER FACTS: There are theorems that further help. If the recursion is over datatypes whose constructors are "freely" interpreted (interpreted as "uninterpreted functions") then there is a classic theorem that says that such definitions always yield a unique fixed-point In general, one should appeal to fixed-point theory. In almost all cases of "first order recursion", the least fixed-point is unique, and is a function. ----------- Apr 9, 2012 ------------ General feedback from me, midterms, lecture plans, etc. Hi, -- subgoal induction -- The topic of subgoal induction is way cool. Too bad those who did not show up on 4/9/12 missed it. Those who attended are urged to look over and ask me questions. There will be one homework question on it. -- missing classes -- It is so strange why someone in grad-school would * miss lectures w/o informing me (class-rule -- see lecture 1's slides) * and yet, if you are in an industrial setting and are called for a group meeting, you would not miss it, would you? So what is the difference between a class and work-place ???? Beats me. As a student, I _never_ used to miss class and always used to ask questions. Sigh. I can tell you one thing: those not showing up have REALLY managed to insult me. One should know better. -- lecture plans -- I'll continue to lecture till the end of the semester, as * many are following the material and gaining from it * this is a grad-level class, and we have a small classroom and I'm quite friendly. I.e. you can always stop and ask me if anything is unclear. To make the lectures meaningful, there will be one short homework question per week. THE REMAINING HOMEWORK QUESTION will be on your project progress, as is due on Wed April 11th. Look over the subgoal induction material in case you wish to catch up. Look what all you can learn simply by attending the class that you are already signed up for !! * Induction and recursion don't get enough mention in our syllabi. * Invariants don't get much discussion. * Floyd/Hoare logic does not... * The fixed-point theory of programs does not.. * CTL and LTL model checking does not.. -- midterm -- The class grades for the midterm are as follows. The exam was not "hard". I'm going by those registered for the class (some have not shown up in a while; don't know if they are in the class). Students who do a good project can compensate for the exam performance unless they have earned an E. I am open to ideas. - A - A - A-+ - A- - A- - A- - B+A- - B+ - B+ - C - E - E - E - E ----------- Mar 21, 2012 ------------ Precedences of operators is listed on Page 7. Basically, negation binds tightest. Then come and, or, implication, iff. In short, I don't understand how to evaluate FOL formulas in terms of a given interpretation. The most basic example which I do not understand is Example 2.13 in the book. It claims that we know that both subformulae in this formula evaluate to true under I, but I don't see how such an evaluation is possible given the lack of a specification of p. >> p is specified. It is the same as p_I listed on this page. >> p_I is true of (0,0) and (1,1) as stated here. Most of the formulas discussed today in class were of this form, yet I couldn't follow the evaluation step in any of them. Can you give a step-by-step explanation of how to evaluate the subformulae in the book example 2.13, given the specified interpretation I? >> Plug in the evaluations for predicate symbols p, function symbols f >> and constants if any. (Constants are usually viewed as 0-ary functions.) >> >> Also choose value domain D = {0,1} as in this example. >> >> In our example, only "p" needs to be plugged in as >> p = lambda (x,y). (x,y) = (0,0) or (x,y) = (1,1). >> >> For these pairs it is true. >> >> Now forall x. p(x,x) means "p(0,0) /\ p(1,1)" which evaluates to >> true. >> >> The second conjunct evaluates to true as well because >> not exists x . forall y. p(x,y) . I.e. there isn't a single >> x such that for all y, p(x,y) holds. So the negated form >> not(exists x. forall y. p(x,y)) evaluates to true. >> >> So just before the black "QED" box, we have the negated formula >> being true. Thus the original un-negated formula is falsifiable. >> >> OK? What is not clear now? ----------- Mar 1, 2012 ------------ I could test Cantin's examples using MPEC - it works as it should (SAT for the first and UNSAT for the second). For the first process histories, it also prints an interleaving out. -- The following is the encoding for Cantin's "SAT" example, which is -- (u1 \/ u2) /\ (!u1 \/ u2) numprocs = 7 proc st.rel [x] = 1 st.rel [x] = 2 proc st.rel [x] = 3 st.rel [x] = 4 proc ld.acq r1 = [x] <1> ld.acq r2 = [x] <3> st.rel [x] = 5 proc ld.acq r3 = [x] <3> ld.acq r4 = [x] <1> st.rel [x] = 6 proc ld.acq r5 = [x] <2> ld.acq r6 = [x] <4> st.rel [x] = 5 st.rel [x] = 6 proc ld.acq r7 = [x] <4> ld.acq r8 = [x] <2> proc ld.acq r9 = [x] <5> ld.acq r10 = [x] <6> st.rel [x] = 1 st.rel [x] = 2 st.rel [x] = 3 st.rel [x] = 4 st.rel [x] = 8 -- The following is the encoding for Cantin's "UNSAT" example, which is -- u1 /\ !u1 numprocs = 5 proc st.rel [x] = 1 proc st.rel [x] = 2 proc ld.acq r1 = [x] <1> ld.acq r2 = [x] <2> st.rel [x] = 3 proc ld.acq r3 = [x] <2> ld.acq r4 = [x] <1> st.rel [x] = 4 proc ld.acq r5 = [x] <3> ld.acq r6 = [x] <4> st.rel [x] = 1 st.rel [x] = 2 st.rel [x] = 6 ----------- Feb 25, 2012 ------------ The gist: "When SAT, we must have the not-equals hold." More specifically, Given clauses SAT ==> transformed clauses SAT in a way that avoids TTT Given clauses UNSAT ==> transformed clauses either unsat (have FFF) or have a TTT hidden in some clause ----------- Feb 24, 2012 ------------ In a 3CNF formula, one can repeat literals. E.g. (a \/ a \/ b) /\ (c \/ c \/ c) /\ (.. .) is allowed. Even (a \/ a \/ a) /\ (!c \/ !c \/ !c) /\ (.. .) is allowed. This hint may help you generate 3CNF formulae that have 3 clauses in them and are unsat. ----------- Feb 22, 2012 ------------ Thanks for the questions in class today: 1) Please ask me questions on Asg5 via email (even if I'm on a trip I'll answer) This friday's submission (2/24) is mainly to force you to go thru these topics and ask me questions via emai. I'll hold open-door office hours next week Thu when I'll be back from my trip. 2) Wei-Fan's question: Let us look at the Predictor Theorem L in NPC and L in Co-NP <=> NP = Co-NP Now consider an L that is NPC (say "K-Clique"). The K-Clique language is: Given a graph G, does it have a K-Clique? What can we say about L's status wrt Co-NP ? i.e. is L likely to be Co-NP ? No, very unlikely. Thus, Clique in NPC, but Clique not in Co-NP (most likely) if it is in Co-NP, then NP=Co-NP, which is thought even more unlikely than P=NP. Thus, to answer Wei-Fan's question: For any L that is NPC, it is also the case that L is NP. But in those cases, L is not likely to be Co-NP. What is K-Clique-bar , the complement of K-Clique? It asks, given a graph G, decide whether G DOES NOT have a K-Clique. Intuitively this is even harder because it appears we can't have a polynomially long certificate (the "evidence" to show that a graph does NOT have a K-Clique seems to be to say "this K subset of nodes does not form a Clique" "neither does this subset" "nor this subset" ... In general, an exp. long certificate is what seems to be required. Such certificates (as far as we can fathom) seem to hint at K-Clique-bar not being in NP. 3) Circuit-SAT (question by Ian): What I explained was circuit complexity - http://en.wikipedia.org/wiki/Circuit_complexity . Circuit complexity is well explained in an UG automata theory book by Hoover/Greenlaw. Circuit-SAT otherwise refers to just Boolean SAT (so far as I know). Please tell me what definitions you see on the web. Whether Circuit-SAT was the first problem examined by Cook or Karp - I don't know - but their papers are available online (Cook 1971 and Karp 1972 - cited on the wikipedia page of NP-Completeness). I plan to look into it. 4) Vishal's question: Whether for general SAT, the degree of the Diophantine equations will still be 2 (squaring) . I think that should work, given the way the reduction proof goes 5) More on the Predictor Theorem and Bradley's question: L in NPC and L in Co-NP <=> NP = Co-NP This theorem's proof is elegant and short (given in my notes - adapted from the Hopcroft / Motwani / Ullman book). Let us look at this theorem a bit. First, what does it mean to say --> L in NP and L in Co-NP? Then L is in the intersection of NP and Co-NP. Notice that "P" is a subset of NP intersection Co-NP. It is not known whether P is equal to this intersection. But the theorem has --> L in NPC and L in Co-NP Thus, L is in the intersection of NP and Co-NP, and also L in NPC. then NP = Co-NP. In two past cases (primality and linear programming), an L that was in NP and Co-NP was found to be, after all, in P itself!! So all we have to say is : if L in NP and L in Co-NP , then perhaps L is in P. ----------- Feb 14, 2012 ------------ Use the proper negation symbol in DDCal - ' not `I figured out what was causing 2input_gate and xor not to work. The negation symbol when the ddc is copied off of pdf file (bdd-notes-ganesh-cs3100.pdf) is not what DDcal accepts. From pdf file it comes as "’", while it needs "'". They are not the same. ----------- Feb 9, 2012 ------------ > In Q3, you have asked us add just one clause to make the given formula unSAT. > The current options I see is to force the variables to ... > If there is such one magic clause, please nudge me towards right direction. I believe it is possible to arrive at a simple example (i.e. adding one clause to the current formula to arrive at a new formula that becomes UNSAT quicker. The idea is that the learned clause now participates in the 'propagate' algorithm, and hence may force falsification sooner. If you think you need more than one clause to be added to the end to arrive at a better illustration, feel free to do so. ----------- Feb 7, 2012 ------------ Soon I'll switch to a discussion newsgroup (sorry I have been too busy to set one up). Meanwhile. a good question asked below. Let me give you a direction. Basically I was imagining that PySat would not be this smart :-) Suppose you consider the textbook PySat: 1) Let it pick 1 from clause 1 (set "var 1" to true) 2) then 2 is forced from clause 1 3) Then let it move to pick "5" 4) Then "6" is forced 5) Then let it pick 7, 8, 9 however 6) It then conflicts at 2 5 6 7) Ah ha, this is where an ultra-naive PySat runs into trouble. It churns over 7,8,9. The smart back-jumper does better. This is what I'd like you all to think about. Hope this is clear to you all (and the original questioner). Ganesh ClauseQ1 = [ [-1 ; 2] ; [-5 ; 6] ; [ 7; 8; 9 ] ; [-2 ; -5 ; -6 ] ] On 2/7/12 8:00 PM,... wrote: > Hi Ganesh, > > I have a question about problem no. 1. The question asks how many more conflicts there will be without backjumping, but the original dpll algorithm does not have any conflicts, at least not using the PySat dpll program. It chooses pure variables -1 -5 7 8 9 and propagates their values which is enough to declare the CNF as SAT. > > I know traditionally backjumping will save steps because it can go back multiple, but I don't see that in this scenario. Am I missing something? ----------- Feb 6, 2012 ------------ Hi [ I'll post these online soon.. ] : I don't think my Q1 was good enough to illustrate the difference between non back-jumping based DPLL (the old simple Python version) and the backjumping based version. So, in order to see a sharp distinction between backjumping and not, change the formula to use for this illustration to ClauseQ1 below. ClauseQ1 = [ [-1 ; 2] ; [-5 ; 6] ; [ 7; 8; 9 ] ; [-2 ; -5 ; -6 ] ] With this clause, the illustration will be much better. Q2 can remain the same -- i.e. remove ONE clause from ClauseQ1 to eliminate the advantage of backjumping Q3 : Just add one clause to ClauseQ1 to illustrate the advantages of clause learning. Hint : the clause you add can cause the formula to be UNSAT. That's OK - because of learning, we might learn "unsat" much sooner. ----------- Jan 31, 2012 ------------ 1) Updated the BDD package online - now it generates traces - see class email (gist follows): I tried looking for a nice way to output python traces, but I decided it might be more readable if I just added some print statements to the actual BDD file. So now I have a BDDtrace.py that will print when the functions are called, (mk and build) and what arguments they are called with and what they return. I added a traceExample directory to the SVN illustrating this with the example Anderson shows on pg 18. You can follow the function calls along with the pictures! Furthermore, any of my BDD examples can be augmented to show the build trace by replacing the line: import BDD to import BDDtrace as BDD 2) Posted the paper by Holzmann and Puri on minimized automation representation of reachable states 3) Http://users.ece.utexas.edu/~adnan/syn-07/ -- look under BDDs This describes an ITE based "Build" (better in practice). Very nice slides! 4) Asg2's due date IS mentioned in that handout early on! 5) Filliatre has provided an excellent BDD package at http://www.lri.fr/~filliatr/ftp/ocaml/bdd/. Compiles and runs out of the box, and gives the # of 8-queen solutions quickly. 6) I've posted Asg3. ----------- Jan 23, 2012 ------------ 1) An Ocaml cheat-sheet is available http://www.ocamlpro.com/code/2011-06-03-cheatsheets.html 2) I made the TTT..FFF argument un-necessarily complex. Here is a much shorter one (same as the one the student who answered suggested), but presented as a proof: Suppose there is a 3CNF formula F = C1 & C2 & ... & CN that is both unsat AND avoids producing a TTT clause and an FFF clause under an arbitrary interpretation I. If I |= F is false, then clearly some Ci in F must be FFF but no Ci must be TTT. But then, under not(I), defined to be a bit-wise complement of I, all Ci must be non-FFF. But then F is not unsat, because it is sat under not(I). Contradiction. So F must, under all I, produce a TTT and an FFF under every I. ----------- Jan 18, 2012 ------------ Ocaml syntax is not arbitrary! * In many prog languages, they add arbitrary things to syntax - E.g. "wouldn't it be nice to add a 'Goatie' to this function header?" Why not put a !! there? etc. - In general, one puts arbitrary "(..)", commas, !, etc. * In Ocaml, there is only one idea: - all functions take EXACTLY one argument !!!! - So if you write f x y > you are really feeding x to f, and getting another function called (f x) in your hands. To that, you are feeding y - if you write f (x,y) > you are feeding a single tuple called (x,y) to f !! > Thus ( .. , .. ) is a tuple builder > tuples are also there in Python BTW - Things of the form f x y = .. are called "curried" functions (you can specialize it one argument at a time) - Now in mathematics, a singleton tuple of the form (x) is exactly the same as x - Thus, putting (..) around x is just to please the eye * Now when you define a function f of 9 arguments, it is ugly to look at it; it may look like this: - f a b c d e f g h i = ... * To make it readable, a nice convention is to write it as - f (a) (b) (c) (d) (e) (f) (g) (h) (i) = ... - or even f (a)(b)(c)(d)(e)(f)(g)(h)(i) = ... where each (a) is, as you know, the same as "a" * This explains my function declaration syntax. ----------- Jan 18, 2012 ------------ More on CNF conversion. 1) Almost all SAT solvers are designed to handle CNF. This is the most commonly used convention. CNF SAT solving is like "whack-a-mole". You might "whack" most of the clauses. Then a "blocking clause" might rear its head and block SAT. So in a sense, CNF SAT is like discovering those Elusive blocking clauses, or quickly concluding that there aren't any. 2) People encode problems in whatever Boolean form that happens to be most normal to them, to the problem, etc. So for instance, someone may encode it in DNF. Or they may encode using ->, nand, etc. 3) Whatever this "natural Boolean encoding", we need to render them CNF before we can use a SAT solver 4) This is where the Equisat method is better because it avoids formula blow-up even while going to CNF. The extra variables thrown in (during this Equisat method) does not hurt the run-time in most problems. ----------- Jan 18, 2012 ------------ Pattern matching is fun! Try these. You'll need this level of understanding to read cnf.ml type foo = {a:int; b:int};; (* This is OK for beginners *) # let {a=a1; b=b1} = {a=2; b=3};; val a1 : int = 2 val b1 : int = 3 (* Once you get good at it, do it this way! *) # let {a=a; b=b} = {a=2; b=3};; val a : int = 2 val b : int = 3 ---------------------- Now, remember that the way "let" pattern matches is virtually the same as "match .. with .. " also does. So to undersand "match .. with .. ", we can do experiments with "let.." ---------------------- (* This match succeeds *) (* I use this in doOr, in one place *) (* Basically this is a "trick" to check that the RHS list is singleton, AND then pull its only member out! *) # let [x] = [2];; Characters 4-7: let [x] = [2];; ^^^ Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: [] val x : int = 2 ---------------------- (* This match fails *) # let [x] = [2; 3];; ----------- Jan 18, 2012 ------------ Naive CNF conversion (equivalence preserving, and not merely equisat) is expensive! Here is an illustration. (* Try this *) Start Ocaml Type #use"gencnf.ml";; Then save the stuff below the line "--- begin" in a file "examples.ml" and type #use"examples.ml";; You'll see how direct conversion explodes. --- begin f1;; (gencnf(f1)(0)([]));; (gencnf(f1)(0)([])).cnf;; List.length (gencnf(f1)(0)([])).cnf;; f3;; (gencnf(f3)(0)([]));; (gencnf(f3)(0)([])).cnf;; List.length (gencnf(f3)(0)([])).cnf;; f4;; (gencnf(f4)(0)([]));; (gencnf(f4)(0)([])).cnf;; List.length (gencnf(f4)(0)([])).cnf;; f5;; (gencnf(f5)(0)([]));; (gencnf(f5)(0)([])).cnf;; List.length (gencnf(f5)(0)([])).cnf;; ----------------------