CS G379 Decision Procedures for Verification
Fall 2007

Homework 1: Due Sep. 21

  1. Send me a photo (jpg or gif) of yourself and tell me how to pronounce your name. Do this ASAP.
  2. Give a linear-time algorithm for 2SAT. If the formula is satisfiable, your algorithm should return a satisfying assignment (in linear time).
  3. Prove that HORNSAT can be solved in polynomial time. Come up with as efficient an algorithm as you can and prove its complexity.
  4. Consider the following restriction to SAT: each clause either has at most 2 literals or is a horn clause. Is this problem in P? Is it NPC? Provide a proof.
  5. Show that the problem of recognizing =3CNF formulas for which there is a satisfying assignment such that at most 2 literals per clause are true, is NPC.
  6. Consider the problem of recognizing satisfiable =3CNF formulas in which each variable appears exactly 3 times. Is this problem in P? Is it NPC? Provide a proof.

Last modified: Tue Sep 11 20:36:18 EDT 2007