From: Harald Hanche-Olsen Subject: Re: complexity class of a decision problem in the propositional calculus Date: 28 Jan 2000 14:07:21 -0500 Newsgroups: sci.math.research Summary: [missing] + mvishnu@bbcr6.uwaterloo.ca (Meenaradchagan Vishnu): | I am no theoretical computer scientist (i.e., I may be totally | wrong) but I have heard that the first paper on NP completeness by | Prof. Cook of U of Toronto showed that tautology-hood is an NP | complete problem. That is unless P=NP, there are no polynomial time | algorithm to determine whether a WFF is a tautology or not. Indeed, the first problem known to be NP-complete, and still frequently the first problem shown in texts to be NP-complete, is 3SAT: The satisfiability of a conjunction of terms, each of which is a disjunction of three variables or their negations, e.g., (using | for (not exclusive) "or", ~ for "not", and & for "and") (A | ~B | C) & (~C | D | ~E) & (~A | B | D) ... Clearly a formula is unsatisfiable iff its negation is a tautology, so this should answer your question. -- * Harald Hanche-Olsen - "There arises from a bad and unapt formation of words a wonderful obstruction to the mind." - Francis Bacon ============================================================================== From: Marcus Raitner Subject: Re: complexity class of a decision problem in the propositional calculus Date: 2 Feb 2000 03:00:02 -0600 Newsgroups: sci.math.research Summary: [missing] Harald Hanche-Olsen writes: > Indeed, the first problem known to be NP-complete, and still > frequently the first problem shown in texts to be NP-complete, is > 3SAT: The satisfiability of a conjunction of terms, each of which is a > disjunction of three variables or their negations, e.g., (using | for > (not exclusive) "or", ~ for "not", and & for "and") > > (A | ~B | C) & (~C | D | ~E) & (~A | B | D) ... > > Clearly a formula is unsatisfiable iff its negation is a tautology, so > this should answer your question. It is correct that 3SAT is NP-complete (NPC), but the first problem known to be NPC, proven by Cook, was SAT, i.e. satisfiability without the restriction three literals in each clause. --- -------------------------------------------------------------- Marcus Raitner Lst. Prof. Brandenburg raitner@fmi.uni-passau.de Uni Passau, D-94030 Passau ++49/851/509-3034, FAX: 3032