Homework 2 Review

We spent at least half the class going over the homework. There were a number of important problems there to discuss! A few comments:

• Problem 6 asked you to prove the following theorem.
  For any propositional formula, $F$, there is an equivalent propositional formula that only uses the operators $\wedge$, $\vee$ and $\neg$ (i.e. no $\Rightarrow$, $\oplus$, $\Leftrightarrow$).

  We need to ask: "What would it take to prove something like this?" Hopefully you will agree that if we could describe a process (an algorithm, as we computer scientists say) that takes formula $F$ as input and produces a formula $G$ that 1) is equivalant to $F$, and 2) only uses ands, ors and nots, then we would have proved the theorem. So that's what we do.

  Here is the 3/C Dongre algorithm:
  Input: formula $F$
  Output: formula $G$, where $G$ is equivalent to $F$ and $G$ only uses ands, ors and nots.
  

  1. construct truth table $T$ for formula $F$
  2. apply the Class 4 algorithm to construct a defining formula for truth table $T$, and call the result $G$

  $G$ and $F$ are both defining formulas for truth table $T$, so they are equivalent. Looking back at the algorithm from Class 4, you will see that it only uses ands, ors and nots.
  
• Problem 7 asks us to prove the following
  The $\wedge$ operator distributes with $\vee$, i.e. $a \wedge (b \vee c)$ is equivalent to $(a \wedge b) \vee (a \wedge c)$.
  The proof was just to check using truth tables.
• Problem 8 asks us to prove the following
  The $\wedge$ operator distributes with $\oplus$, i.e. $a \wedge (b \oplus c)$ is equivalent to $(a \wedge b) \oplus (a \wedge c)$.
  The proof was just to check using truth tables.
• We went over Problem 10 in some detail. One important thing that came out of the discussion is this: our philosophy is to translate the english language constraints into propositional logic as directly as possible. We only want to make logical deductions when we are in propositional logic world. So for example:

                             English                        Logic
  		 --------------------------------        --------
  		 it is not the case that both bob
  		 is wearing a hat and cathy is           ¬(bh∧¬cs)
  		 not wearing sunglasses	  

  This is a direct translation of the english, so that's what we do. It is equivalent to say, for example, ¬bh ∨ cs (don't worry if you don't see why). But we don't want to write that down, because it is not a direct translation of the English. There are some logic steps in between the English and the propositional formula ¬bh ∨ cs. We don't want that. We only want logic steps after we've translated to propositional logic.

Modeling real problems in propositional logic and using SAT solvers to discover new information

In small groups you will use propositional logic and SAT solvers to some the problem below. I suggest you first think about what variables you want. Not just what letters to use, but for each variable, what statement that variable stands for. Then try to model each rule with a formula.

ACTIVITY

• At the beginning of the course we looked at this problem as a motivation for why CS students study logic. We should be able to write programs that solve problems like this. Right now we are doing it by hand, but we could code this up into a program.

  Suppose a car is offered with various packages and options, with the following restrictions:

  1. the sport package requires ceramic brakes
  2. the sport package comes with rearwing and rear wing only comes with the sport package
  3. if turbo then the car can't have stock brakes
  4. ceramic brakes require the large wheels
  5. the only wheels are large wheels or regular wheels
  6. only base models (i.e. no packages) are available with regular wheels
  7. base models (i.e. no packages) don't have turbo
  8. the touring package comes with roof rack.

  Below are two questions. Your job is to model the above restrictions using propositional logic, and then use a SAT solver to answer the two questions below.

  Question 1: Can I have the turbo with regwheels?

  Question 2: Can I have the turbo without having the rearwing?

Solution to the modeling problem

Below is a screenshot of a session with the Propositional Logic Tool that solves the problem from the Activity.

A few important thoughts:

• Constraint 5 is actually a bit vague. Translating it to propositional logic requires using the background information that you can't have both large wheels and regular wheels.
• I chose not to have a variable for "base", but instead to use (~sp & ~tp) as "base". In fact, it would have probably been prettier to make a "base" variable, but then I would have had to add (base <=> (~sp & ~tp)) to the formula.
• To "ask a question", we translate the condition (like turbo and regular wheels) to a formula, and "and" it to the end of the main formula.

A few comments

This example is small, a toy example, really. But using SAT solvers to manage configurations in automotive manufacturing is absolutely a real thing (see for example this paper). In fact, SAT Solvers get used for all sorts of industrial applications. Their ability to handle enormous problems makes them very powerful tools. But in the end, the way they get used is very much what we are doing in our activity. We encode our real-world problems in propositional logic, let the SAT Solver find a solution (or determine UNSAT), and map tha solution (or the fact that there is no solution) back to the real world, thereby giving us a new fact.