Satisfiability of Propositional Formulas
A propositional formula is satisfiable if there exist an interpretation under which it is true.
Example 1
The formula $(p\wedge\neg p)$ is not satisfiable, because:
\[I(p\wedge\neg p)=0\]for all interpretations $I$:
| $p$ | $\neg p$ | $(p\wedge\neg p)$ |
|---|---|---|
| 1 | 0 | 0 |
| 0 | 1 | 0 |
As you can see from the table there is no case in which the case is satisfiable.
Example 2
There are some cases which don’t require the truth table to be parsed in order to find out if it is satisfiable. See this question:
Is the formula, $P=(p_1\Rightarrow(p_2\wedge\neg p_2))$ satisfiable.
To see this, simply choose any interpretation $I$ with $I(p_1)=0$. Then $I(P)=1$ and we have found an interpretation $I$ that makes $P$ true.
The same argument shows that every formula of the form $(p_1\Rightarrow Q)$ is satisfiable.
There are also other combinations where you can prove that they are satisfiable without working any values. E.g.:
\[(p_1\Leftrightarrow Q)\]such that $p_1$ does not occur in $Q$ is satisfiable.
Deciding Satisfiability
- $P$ is satisfiable if $I(P)=1$ for some interpretation $I$.
- There are $2^n$ interpretations if $P$ has $n$ propositional atoms.
- Thus, to check whether $P$ is satisfiable directly using truth tables, a table with $2^n$ rows is needed.
- This is not practical, even for small $n$
- Another case of combinatorial explosion.
There has been great progress in developing very fast satisfiability algorithms (called SAT solvers) that can deal with formulas with bery large numbers of propositional atoms (using heuristics).