We worked on installing rosette and ran into some issues with raco and DrRacket. After installing rosette, we spent some time looking through the homework assignment and understanding section 1 and the Rosette procedures associated with it. In particular we focused on the vc (verification condition) and the (=> and <=> procedures) which took some time getting used to.
Afterwards we got started on problem 1 and was able to finish it and provided testing in classify.rkt. Then we worked on problem 2 and the solution is in hw1_2_tseitin.rkt.
Finally, we worked on problem 6 and 7 which was about turning k-coloring graph problems into CNF form. We finished problem 6 and our answers are up in 530_rosette_hw1.pdf and we theorized about problem 7 but ran into blockers pertaining about understanding the given code and the types associated with rosette.