SAT Solving

One fundamental problem in propositional logic is the satisfiability problem (often just called "SAT") which is this: given a propositional formula $F$, is there an interpretation under which $F$ evaluates to true (i.e. $F$ is satisfied). Usually, if the answer is "yes, $F$ is satisfiable", there is an expectation that one should also provide a satisfying interpretation. That way, whoever posed the SAT problem in the first place can check for themselves that the "yes" answer they just got is actually correct. The satisfying interpretation is, in fact, a proof that the formula is satisfiable.
Note: Logicians refer to the satisfying interpretation as a model for the formula. That's the terminology, so we are stuck with it, but it is a bit unfortunate as the word "model" has other meanings that we will also want to use. Just do the best you can and ask questions if you are not sure which meaning is intended!

If you have a truth table for a formula $F$, SAT solving is easy - just look for a row in which the result column has "true". If such a row exists, you can read off the satisfying interpretation, if no such row exists the formula is not satisfiable. Moreover, if the formula is UNSAT (i.e. not SAT), the truth table is a proof of that fact (though perhaps a very large proof if the truth table is large).

ACTIVITY Note: copy and paste these formulas into the propositional logic tool, don't try to type all this on your own!
  1. Based on its truth table, is $\neg(a \Rightarrow (b \oplus c)) \wedge \neg b$ satisfiable? If so, give a model!
  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? If so, give a model!
  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? If so, give a model!
  4. Try using the truth table for (a xor b) & (c xor d) & (e xor f) & (b => d) & (a => d) & (e => f) & (~(u=>(v xor 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?

SAT Solving the real way

Computer programs that solve the satisfiability problem are called SAT Solvers. Modern SAT Solvers are able, in practice, to solve very large formulas. They are powerful tools that are important in many practical applications. The "SAT" checkbox on the SI242 Propositional logic formula analysis tool will run a SAT solver called Minisat in your browser. It can handle formulas that are way too large to construct a truth table for. For instance, if you have 100 variables, the truth table would have 1267650600228229401496703205376 rows. So, suffice it to say, computing the truth table would take a very, very, very long time. And there would be no way to look at such a huge thing. However, the SAT-solver in your browser would almost certainly solve it in a few seconds. Just make sure the "Truth Table" check box is unchecked, otherwise your browser tab will die on you! Try the "SAT" option on that last formula from the previous activity.

How SAT solvers like Minisat work is a fascinating topic, but one that is well outside of this course. The point is that if you can model a real-world domain in propositional logic, you can leverage the power of SAT Solvers to discover new facts about that domain.

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

Reason #2 for why CS Students should study logic is: modeling problem spaces and deducing new facts! Let's see that in action.

Problem: 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?

Our first step will be to model this problem in propositional logic. To model a problem in algebra we first state what are variables are and what they *mean* in the context of the problem we are modeling. Same with modeling in propositional logic. In fact, the name "propositional" hints at this. Each variable stands for a "proposition", a statement that is either true or false.

variable
name		 proposition
(meaning)		 note
a "Alice in Civic" since Alice must be in one or the other, ~a means Alice is in the Mustang
b"Bob in Civic"same!
c"Cathy in Civic"same!
d"Don in Civic"same!

So here are facts 1,2,3,4 stated in our propositional variables: 

(a <=> ~b) & ( c <=> ~d => (a <=> ~d)) & (~c xor ~d) & (b => c)
\________/   \_______________________/   \_________/   \______/
    1                   2                    3            4

This formula, which we will call $F$, is our translation of the Civic/Mustang-World problem to Propositional Logic World. Now, if we can learn anything about $F$ using the tools of propositional logic, we can reverse-translate these new facts to Civic/Mustang World, and the whole point of logic is that these reverse-translations must hold in Civic/Mustang World! So ... what can we learn about the formula $F$? If you use the tool to create a truth table (or if you just use the SAT-solver) you will find that {a=true,b=false,c=true,d=false} is a satisfying interpretation for $F$. If we map this interpretation back, we get that putting Alice and Cathy in the Civic and Bob and Don in the Mustang satisfies the constraints! Great, right? The following picture is how you want to think about this process.

ACTIVITY
Christopher W Brown