Satisfiability
Satisfiability
Definition
Let Γ be a set of formulas. We say that Γ is satisfiable if there is some truth assignment e such that e(γ) = T for all γ ∈ Γ.
Example
{(P ∧ Q), (¬P ∨ Q)} is satisfiable.
If e(P) = T and e(Q) = T, then e((P ∧ Q)) = T and e((¬P ∨ Q)) = T.
Example
For any formula ϕ, {¬ϕ, (¬ϕ → ϕ)} is not satisfiable.
Indeed, assume for a contradiction that e(¬ϕ) = T and e((¬ϕ → ϕ)) = T.
Then, by definition of ¬ and →, e(ϕ) = F and e(ϕ) = T, a contradiction.
Example
{(P1 → P2), (P2 → P3), (P3 → P4), . . .} is satisfiable.
Indeed, taking e(Pi) = T for all i satisfies the set (as does taking e(Pi) = F for all i).
Note: The empty set of formulas is satisfiable.
Satisfiability and Logical Consequence
Proposition
Let Γ be a set of formulas and let ϕ be a formula.
(1) If Γ is satisfiable and Γ |= ϕ, then Γ ∪ {ϕ} is satisfiable.
(2) Γ 2 ϕ if and only if Γ ∪ {¬ϕ} is satisfiable.
Checking Satisfiability
Checking Satisfiability
Checking whether a finite set of formulas is satisfiable can be done using a truth table.
If there are n distinct variables in the set of formulas, the truth table will have 2
n lines.
Calculating what happens in each line involves reading each formula, breaking each formula down into its construction from the variables, and following the rules for how truth assignments work to compute the truth values of each formula under the given truth assignment.
That is, to calculate what happens in each line of the truth table requires a number of steps that is polynomial in the length of the input.
However, due to the size of the table, the total number of steps required is exponential in the length of the input.
Complexity of Algorithms
Computer scientists worry about the run times of algorithms. If there is a polynomial expression for the number of steps it will take to execute an algorithm as a function of the length of the input, then the algorithm is called a polynomial time algorithm. The collection of all problems that can be solved using a polynomial time algorithm is denoted P.
Polynomial time algorithms are, for the most part, considered efficient. Algorithms where the run time is exponential as a function of the length of the input are considered inefficient.
There are some problems where, roughly speaking, a “lucky guess” to a reason for a “yes” answer can be verified with a polynomial time algorithm, and a wrong guess to a reason for “yes” can be seen to be wrong by the same algorithm. The collection of such problems is denoted NP, which stands for “non-deterministic polynomial time.” Certainly, every problem that can be solved using a polynomial time algorithm belongs to NP (you don’t need to guess if you don’t want to). That is, P ⊆ NP.
A big open question in theoretical computer science is whether P = NP.
SAT
Definition
The problem SAT is, for any finite set of propositional formulas over the connectives ¬, ∧, and ∨, to decide whether the set is satisfiable.
To check whether a particular set Γ is satisfiable is called an instance of SAT.
The problem SAT belongs to NP. It is not known whether there is a polynomial time algorithm for solving SAT. However, it has been shown that SAT is NP-hard, in the sense that if SAT belongs to P, then P = NP.
Though there is no known algorithm for SAT that is efficient on all inputs, there are algorithms that are efficient on most inputs, or there are algorithms that are efficient but only accept special kinds of input.
Clauses
Satisfiability — Simplifying the Formulas
For any formulas ϕ and ψ, and for any truth assignment e, e((ϕ ∧ ψ)) = T if and only if e(ϕ) = e(ψ) = T. It follows that for any formulas ϕ and ψ, and for any set of formulas Γ, Γ ∪ {(ϕ ∧ ψ)} is satisfiable if and only if Γ ∪ {ϕ, ψ} is satisfiable.
When checking whether a set of formulas Γ is satisfiable, we can first bring each formula in Γ into a conjunctive form, and then replace each formula with all its conjuncts.
Example
Consider Γ = {¬(P ∧ (P → R)), ((Q ∨ R) ∧ (¬P ∨ ¬Q)), (¬P ∧ ¬S)}.
¬(P ∧ (P → R)) |= =| ¬(P ∧ (¬P ∨ R))
|= =| (¬P ∨ ¬(¬P ∨ R))
|= =| (¬P ∨ (P ∧ ¬R))
|= =| ((¬P ∨ P) ∧ (¬P ∨ ¬R)
|= =| (¬P ∨ ¬R)
So Γ is satisfiable if and only if Γe is satisfiable where
Γ =e {(¬P ∨ ¬R), (Q ∨ R), (¬P ∨ ¬Q), ¬P, ¬S}
For this reason, many algorithms that check for satisfiability assume that all formulas in the set are disjuncts of literals.
Clauses
Definition
A clause is a (possibly empty) finite set of literals.
Example
{P, Q, ¬R} is a clause.
Definition
A set Γ of clauses is satisfiable if and only if there is at least one truth assignment e such that for every clause C ∈ Γ, there is some literal L ∈ C with e(L) = T.
Example
If Γ = {{P, Q, ¬R}, {¬Q}}, then Γ is satisfiable.
Indeed, let e be a truth assignment with e(P) = T and e(Q) = F. Then
P ∈ {P, Q, ¬R} and e(P) = T and ¬Q ∈ {¬Q} with e(¬Q) = T, so e satisfies Γ.
Note that if ∅ ∈ Γ, then Γ is unsatisfiable, since there are no literals in ∅.
Clauses
Definition
If ϕ = (L1 ∨ . . . ∨ Ln) where L1, . . . , Ln are literals, then {L1, . . . , Ln} is the clause associated to ϕ.
Note that for any truth assignment e, e((L1 ∨ . . . ∨ Ln)) = T if and only if there is some Li ∈ {L1, . . . , Ln} with e(Li) = T.
So if Γ = {ϕ1, . . . , ϕk} where each ϕi is a CNF constituent and Γ =e {C1, . . . , Ck} where for 1 ≤ i ≤ k, Ci is the clause associated to ϕi, then Γ is satisfiable if and only if Γe is satisfiable.
Example
Γ = {(¬P ∨ ¬R), (Q ∨ R), (¬P ∨ ¬Q), ¬P, ¬S} is satisfiable if and only if
Γ =e {{¬P, ¬R}, {Q, R}, {¬P, ¬Q}, {¬P}, {¬S}} is satisfiable.
Definition
The problem of CNF-SAT is, for any finite set of clauses, to decide whether the set is satisfiable.