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?