Checking tautology

371 Views Asked by At

Given a Boolean formula $\phi$ in CNF form, I'll check whether there exists a clause that can be falsified i.e. check for literals of the form $x \vee \neg x$. If there are not any such literals in a clause, I'll assign false to all the literals in that clause.

But tautology is the complement of SAT problem, right? Am I missing something?

1

There are 1 best solutions below

0
On BEST ANSWER

Solving SAT this way means starting with a CNF, and then taking the negation, and writing that in CNF form. That can result in an expression with an exponential increase in terms.

For example, if $\phi$ is $$(p\lor \lnot q)\land(q\lor\lnot r)\land(r\lor \lnot p)$$ then $\lnot \phi$ is:

$$(\lnot p\land q)\lor (\lnot q\land r)\lor (\lnot r\land p)$$ That part is easy. If $\phi$ in CNF has length $N,$ then computing $\lnot\phi$ in “disjunctive normal form” (DNF) takes $O(N)$ time.

But your algorithm requires $\lnot\phi$ in CNF.

Using distributive law to get $\lnot \phi$ into CNF form gets you $8$ terms and all of them are tautologies. An expression for $\phi$ with $6$ atoms becomes an expression for $\lnot\phi$ with $24$ atoms.

If $\phi$ has $n$ clauses with $m_i$ atoms in the $i$th clause, then $\lnot \phi$ in CNF form will have $\prod_i m_i$ clauses with $n$ atoms in each. So, yes, with an input of length $\sum m_i$ your algorithm lets you solve whether $\lnot \phi$ is a tautology in $O(n\prod_i m_i).$ But that isn’t polynomial time.

For example, in $3$-SAT, where all $m_i=3,$ the length of $\lnot \phi$ in CNF form is $3^n$ clauses each of length $n.$

The distributive law amounts to checking all $3^n$ cases.

What you’ve found is that SAT is easily solved if we restrict to inputs that are in “disjunctive normal form.” Then $\lnot \phi$ is in CNF in $O(N)$ time.

But this is obvious directly, by using the same process without negating - just look for a clause that doesn’t have an immediate contradiction and satisfy it.

Solving SAT is easiest with inputs in DNF. Solving Tautology is easiest with inputs in CNF.