SAT Solving

ACTIVITY I
  1. Based on its truth table, is $\neg(a \Rightarrow (b \oplus c)) \wedge \neg b$ satisfiable?
  2. Based on its truth table, is $(a \vee \neg b) \wedge (\neg a \vee c) \wedge (c \vee \neg b) \wedge (\neg a \vee \neg c) \wedge (a \vee b)$ satisfiable?
  3. Based on its truth table, is $(a \oplus b) \wedge (c \oplus d) \wedge (e \oplus f) \wedge (b \Rightarrow d) \wedge (a \Rightarrow d) \wedge (e \Rightarrow f)$ satisfiable?
  4. Try using the truth table for

    (a⊕b)∧(c⊕d)∧(e⊕f)∧(b⇒d)∧(a⇒d)∧(e⇒f)∧(¬(u⇒(v⊕w))∧¬v)

    to determine whether or not it is SAT. Are you still happy with this method for SAT-solving? What is the critical factor in determining the size of the truth table? Can you quantify the size dependency?
IN-CLASS EXAMPLE
Suppose we have Alice, Bob, Cathy and Don, and two cars - a Civic and Mustang. We have some constraints:
  1. Alice and Bob have to be in different cars (the only drivers!)
  2. If Cathy and Don are in separate cars then Alice and Don have to be in separate cars too.
  3. Either Cathy or Don is in the Mustang, but not both.
  4. If Bob is in the Civic, then so is Cathy.
Can we put people in cars so that the constraints are satisfied? If so, how?
ACTIVITY II
Assume we have Alice, Bob, Cathy and Don and the Civic and Mustang like the in-class example, but use the following constraints instead:
  1. If Alice or Bob are in the Civic, then so is Cathy
  2. If Cathy or Don (but not both) are in the Civic, then Alice and Bob are not in the same car
  3. Cathy is in the Mustang
Who goes in which car?
Christopher W Brown