https://www.brinckerhoff.org/clements/2214-csc530/Assignments/rosette-123.html
1 hour in: I tried to get started but I'm having a really hard time understanding rosette and don't know how solve vs verify work.
I'd like to just do #1 but probably will have to wait until monday to see what I can actually do
I think I got HW problem 1 completed. This is pretty cool bc I didn't know if I'd be able to do it.
Learning rosette is very interesting and I think a major barrier for me was just really figuring out the difference between solve and verify.
I think the trouble in learning though is something with all tools as docs cannot be perfect and in a small community (i.e. rosette users) a google search hardly satisfies.
Problem 1 took me much longer than I'd like to log haha.
I took the approach of applying solve first as this will tell me if a formula is a contradiction as it will return unsatisfiable (not be able to be solved)
After we have categorized contradictions we can proceed to verify the formula and see if this returns unsatisfiable. Unsatisfiable in this setting means that no counterexample could be found and thus this formula would be a tautology but if there is a possible counterexample then this formula is indeed a contingency.
Few more hours in. Tried to go over the slides for the course and attempted homework problem 2. I am not very knowledgable of logic but I tried to folloow the slides and use online resources.
I added a pdf of my process and my final solution I came to. It was good to get more comfortable with CNF and what it is. I wrote some notes, that consisted of pretty much copying the slides, but slowly and surely I am understanding things more.
I am going to continue to go over course materials and attempt to do some of the graph coloring coding and see what happens in class on wednesday
Ok that didn't work, I can't get the graph code to run as I'm getting a permission error on trying to open a file through racket so that's no good. And I don't understand the first part at all. Hopefully we can go over this on Wednesday, but the due date has been extended until Friday so that gives me some time.
I read through all the introductory slides on propositional basics and am now about to embark on normal forms. I probably should have gone through these slides before trying problem 2 but alas. Hopefully class today will cover the remaining slides on sat solving and then these combined will guide me through some more of the hw.
I feel like I just keep uploading pdfs, but I did rename some of them and added in a notes pdf to keep track of what I've been doing. I remember things better when I write them down so it's mostly definitions and what not. These definitions are important though, because I feel like much of rosette embodies them and uses them throughout the system. (like model in rosette and intepretation in hw)
Read over all the slides up until hw 1 is due.
The algorithms seem cool and should've implemented them bc logic isn't very fun haha.
I approached problem 6 as I want to code the graph coloring program, but figured I needed to understand the problem better before I did that. I think my work shows my process well, but I'm still challenged in converting it to CNF/answering the last part. I've already spent a long time on this assignment but since we have had so many extensions I wanna try and do the graph coloring.
I tried to take my work from number 6 to apply to problem 7, but I don't think I have enough understanding of the topic to get much progress on it.
Overall this assignment has been great as the slides were very informative and I enjoyed having actual problems to work on for a change to give me some direction.
My work on some the problems can be found under problem_x.pdf and my racket code is in the necessary file locations.
I really wanted to get some more racket written but I just don't think it's gonna happen. I've spent a lot of time on this (lots of extensions) so I think I'm done for now, but want to study the solution when it comes out.
I should have paired on this or other assignments, but this quarter was so hectic for me and I'm just not comfortable in the CSC 5xx setting yet. These are bad excuses but too late, just now I know for next time.