2

The Tautology Problem is to determine whether a given logical expression is equivalent to true. The book I am reading says that this problem is intractable, because when the number of variables in the expression is large, the method for solving the tautology problem becomes very slow. I understand all this.

But why can't we use the algebraic method for determining if an expression is a tautology? All that involves is a applying a couple of algebraic laws to the expression until the expression is simplified to true, at which point we have proven that the expression is a tautology. Why isn't this method viable? Is it because we don't know when to stop applying the algebraic rules?

By the way, this is the book I referred to: http://infolab.stanford.edu/~ullman/focs.html

JRG
  • 123
  • 2
    The other reason is that the algebraic rules may result in an expression that is too long. E.g. it is easy to tell if a formula in DNF is satisfiable, but a CNF formula like $(x1 \lor y_1)\land (x_2 \lor y_2) \land \cdots \land (x_n \lor y_n)$ has only $n$ disjunctive clauses but if we multiply it out into DNF it will have $2^n$ conjunctive clauses. – Carl Mummert Sep 30 '18 at 03:04

1 Answers1

0

That method is viable for small number of variables. The problem is when there are a large number of variables.

Take an instance of SAT with n variables and m clauses. Call it $\phi_{n,m}$.

Make the statement $\phi_{n,m} \implies F$. If the statement $\phi_{n,m}$ is not satisfiable then this statement will give $T$ eventually. Otherwise it is not a tautology.

Determining whether or not $\phi_{n,m}$ is not satifiable is too hard.

The problem with just applying the rules is you will have to keep going for a long time in order to be guaranteed when you are done.

AHusain
  • 5,183