Assignment 2: Logic and Constraint Programming
The objective of the assignment is to introduce Constraint Satisfaction as a general framework for formalizing and solving both static (untimed) and dynamic (timed) problems.
Given out: February 2. Assignment emailed to all registered participants, and also accessible as http://rintanen.info/ASS2/YOURPERSONALSTUDENTID.pdf.
Return: Sunday February 19 at midnight 23:59:59
Downloads: grounder (64-bit Linux binary executable) grounder (Mac executable), zebra.fma, sudoku.fma, robotmoves.fma, MathSAT (website) language documentation (PDF)
Instructions: Write solution specification as instructed in the lecture slides. Feed the specification (example: zebra.fma)
to the grounder to produce a corresponding SMT file, which is fed to
MathSAT to obtain a solution valuation (truth-values for all atomic
propositions).
./grounder zebra.fma > zebra.smt
./mathsat -model < zebra.smt > zebra.output
There may be a lot of output, and to interpret the valuation given by MathSAT, typically it is useful to look at only those lines that correspond to true atomic propositions.
grep true zebra.output
Returning the assignment: Submit your .fma file, your
.smt file, and a short document that shows the solution produced by
MathSAT in human-readable form, including an explanation of what the
solution means. Submit the files separately (not as an archive!), with your student ID as the prefix of the filenames.