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).

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 the 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

Note: To see why "Alice and Bob in different cars" can be modeled by $a \Leftrightarrow \neg b$, remember that "Alice and Bob in different cars" is equivalent to saying "$a$ and $b$ have different values", and since there are only two possible values (true/false), "$a$ and $b$ have different values" means "$a$ and $b$ have opposite values" — i.e. $a \Leftrightarrow \neg b$. We could equally well have written it as "$\neg(a \Leftrightarrow b)$", which you can verify with the propositional logic tool is equivalent.

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

• Using Alice, Bob, Cathy and Don and the Civic and Mustang again, but the following constraints:
  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 in not in the same car
  3. Cathy is in the Mustang
  Who goes in which car?

Discussion:
The solution we get has Alice, Bob, Cathy and Don all in the Mustang. What if we really want to have at least one person in each car? How could we encode that as a new constraint or set of constraints?

• "at least one person is in the civic" can be written as $(a\vee b\vee c\vee d)$.
• "at least one person is in the mustang" can be written as $(\neg a\vee \neg b\vee \neg c\vee \neg d)$.

What happens if we add those constraints? Then the formula becomes UNSAT, so there is no way to place people in cars that satisfies the original constraints with the new requirement that neither car is empty.

What if not everyone has to be in a car?

Let's look at one last variation. Suppose we consider the same scenario as in the activity, with the additional constraint that both cars have at least one person in them, but we also allow the possibility that people may not be in either car (i.e. they are left behind). In this scenario there are three possibilities for each person. They could be in the Civic, in the Mustang or in neither car. So having the single propositional variable "$a$" to represent Alice's situation, for example, no longer works. After all there are only two possible values for the variable, but we have three different situations for Alice. The solution is to have two variables for alice:

	ac : true means Alice in Civic, false means Alice not in Civic
	am : true means Alice in Mustang, false means Alice not in Mustang
      

This is great: (ac,am) = (true,false) means Alice is in the Civic, (ac,am) = (false,true) means Alice is in the Mustang, and (ac,am) = (false,false) means Alice is in neither car. However, what about (ac,am) = (true,true)? This would mean Alice is in both cars, which we (of course) cannot allow. So we also need to add

	~(ac & am)

... to our list of constraints, since this constraint disallows the situation where Alice is in both cars.

~(ac & am) & ~(bc & bm) & ~(cc & cm) & ~(dc & dm) & # nobody is in both cars at the same time
((ac | bc) => cc) &                                 # If Alice or Bob are in the Civic, then so is Cathy
((cc xor dc) => ~(ac & bc | am & bm)) &             # If Cathy or Don (but not both) are in the Civic, then Alice and Bob are in separate cars
cm &                                                # Cathy is in the Mustang
(ac | bc | cc | dc) & (am | bm | cm | dm)           # neither car is empty