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

Return: Sunday February 19 at midnight 23:59:59 

Downloads: grounder (64-bit Linux binary executable) grounder (Mac executable), zebra.fma, sudoku.fmarobotmoves.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.