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:
“An efficient and valuable man does what he can, whether the community pay him for it or not. The inefficient offer their inefficiency to the highest bidder, and are forever expecting to be put into office. One would suppose that they were rarely disappointed.”
—Henry David Thoreau (1817–1862)
“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)
“I tell you, sir, the only safeguard of order and discipline in the modern world is a standardized worker with interchangeable parts. That would solve the entire problem of management.”
—Jean Giraudoux (1882–1944)