Last Update: 14 September 2010
Note: or material is highlighted |
One interesting "application" of propositional logic in computer science
is the problem sometimes known as the "Boolean satisfiability problem",
or "SAT".
(No, it has nothing to do with the S.A.T. exams!)
It's called "Boolean", after
George Boole, one of the first modern
logicians to study two-valued logic.
(He is the
author of a book called
The Laws of Thought; there's a biography of
him on p.5 of the Rosen text;
see also
amazon.com
and an online article by him: Boole, George (1848),
"The Calculus of Logic", Cambridge and Dublin
Mathematical Journal 3: 183–198).
And it's called "satisfiability", because it concerns how to determine whether a compound proposition has the truth value T given the truth values of its atomic propositions.
Recall from class that, if a compound proposition is constructed from n
atomic propositions,
then its truth table requires 2^{n} rows, which grows
exponentially large, i.e., very quickly.
As you may know, not all problems are solvable by computer (i.e., "are
computable").
The most famous noncomputable problem is the
"Halting Problem":
But among
computable
problems, some can be solved in a reasonable
amount of time and others can't.
The theory of computational complexity
studies the efficiency of computer programs.
The ones that can be
solved in a reasonable amount of time are said to be solvable in
"polynomial time";
the others are said to be solvable only in
"non-deterministic polynomial time",
which—without going into any
details—comes down to saying that they can't be solved before the
universe ends, more or less.
Now, it turns out that some of these problems are "NP-complete", which means that
The most famous NP-complete problem is SAT.
In other words, if you can prove that you can write a computer program
that will compute any truth table in polynomial time,
then all programs
are capable of being solved in "reasonable" time.
But don't get your hopes up:
For more details, see: