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:
“I make no secret of the fact that I would rather lie on a sofa than sweep beneath it. But you have to be efficient if you’re going to be lazy.”
—Shirley Conran (b. 1932)
“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)
“[How] the young . . . can grow from the primitive to the civilized, from emotional anarchy to the disciplined freedom of maturity without losing the joy of spontaneity and the peace of self-honesty is a problem of education that no school and no culture have ever solved.”
—Leontine Young (20th century)