Efficient Verification and The Boolean Satisfiability Problem
The problem of constructing practical algorithms to determine whether sentences with large numbers of propositional variables are tautologies is an area of contemporary research in the area of automated theorem proving.
The method of truth tables illustrated above is provably correct – the truth table for a tautology will end in a column with only T, while the truth table for a sentence that is not a tautology will contain a row whose final column is F, and the valuation corresponding to that row is a valuation that does not satisfy the sentence being tested. This method for verifying tautologies is an effective procedure, which means that given unlimited computational resources it can always be used to mechanistically determine whether a sentence is a tautology. This means, in particular, the set of tautologies over a fixed finite or countable alphabet is a decidable set.
As an efficient procedure, however, truth tables are constrained by the fact that the number of valuations that must be checked increases as 2k, where k is the number of variables in the formula. This exponential growth in the computation length renders the truth table method useless for formulas with thousands of propositional variables, as contemporary computing hardware cannot execute the algorithm in a feasible time period.
The problem of determining whether there is any valuation that makes a formula true is the Boolean satisfiability problem; the problem of checking tautologies is equivalent to this problem, because verifying that a sentence S is a tautology is equivalent to verifying that there is no valuation satisfying . It is known that the Boolean satisfiability problem is NP complete, and widely believed that there is no polynomial-time algorithm that can perform it. Current research focuses on finding algorithms that perform well on special classes of formulas, or terminate quickly on average even though some inputs may cause them to take much longer.
Read more about this topic: Tautology (logic)
Famous quotes containing the words efficient, verification and/or problem:
“As machines become more and more efficient and perfect, so it will become clear that imperfection is the greatness of man.”
—Ernst Fischer (1899–1972)
“Science is a system of statements based on direct experience, and controlled by experimental verification. Verification in science is not, however, of single statements but of the entire system or a sub-system of such statements.”
—Rudolf Carnap (1891–1970)
“The problem with marriage is that it ends every night after making love, and it must be rebuilt every morning before breakfast.”
—Gabriel García Márquez (b. 1928)