How can DPLL formula be used to check whether a DNF formula is valid?

Question

I know DPLL is for CNF formulas, but in theory, how could one use the DPLL formula to check whether a DNF formula is valid? Which rules could be used?

Answer 1

OK, so the assumption here is that you are given a (single) DNF formula, and you have to test whether it is valid, i.e. whether it is a tautology, right?

OK, yes, we can do something akin to DPLL here:

First we can make a clause set from a DNF like we do from a CNF. That is, we can take a statement in DNF like $(A \land B) \lor \neg A$ and make that into clause set $CS = \{\{A,B\},\{\neg A \}\}$.

Note that this clause set represents a disjunction (the original DNF), and each clause therein a conjunction (as opposed to the normal DPLL, where clause sets is a conjunction, and the clauses are disjunctions). And again, our question is: does the clause set represent a necessarily true (i.e. valid, i.e. tautologous) statement?

To find this out, we use the same basic splitting method that forms the core of DPLL. But, whereas in the normal DPLL we say: 'the clause set is satisfiable iff if it satisfiable when we set some literal to true or we set it to false', for the new algorithm we say: 'the clause set represents a tautology iff it represents a tautology when we set some literal to true and if we set it to false'.

And, like the normal DPLL, we can reduce the clause set as a result of setting some literal $L$ to true: if a clause contains the complement of $L$ ($L'$), then the clause will be false, meaning that the clause set can only represent a tautology if the remaining clauses represent a tautology. In other words, we can remove any clause that contains $L'$. Also, if a clause contains $L$ itself, then given that we set it to true, we can eliminate that $L$ from the clause, since it will be true iff without $L$ it will be true. Of course, all other clauses remain as they are.

Finally, there are two cases where we can stop:

1) the clause set contains an empty clause. Since an empty clause represents a conjunction with zero conjuncts, this is a tautology, and hence the clause set is a tautology as well. Return True.

2) the clause set is empty. This represents a disjunction with zero disjuncts, which is a contradiction. Hence, the clause set is certainly not a tautology. Return False.

OK, so we obtain the following algorithm:

$Taut(\{\})=False$

$Taut(\{\{\}\})=True$

$Taut(CS)=Taut(CS_L) \land Taut(CS_{L'}) $ where L is some literal in $CS$, and where:

$CS_L= \{C\setminus\{L\}|C\in CS \land L'\not\in CS\}$ (that is, remove from CS any clause $C$ that contains $L'$, and remove $L$ from all other clauses $C$ in $CS$.)

So, for our example:

$Taut(\{\{A,B\},\{\neg A\}\}) = $ (pick $A$)

$Taut(\{\{A,B\},\{\neg A\}\}_A) \land Taut(\{\{A,B\},\{\neg A\}\}_{\neg A}) =$

$Taut(\{\{B\}\}) \land Taut(\{\{\}\}) = $

$Taut(\{\{B\}\}) \land True = $

$Taut(\{\{B\}\}) = $ (pick $B$)

$Taut(\{\{B\}\}_B) \land Taut(\{\{B\}\}_{\neg B}) =$

$Taut(\{\{\}\}) \land Taut(\{\}) =$

$True \land False =$

$False$

As with the original DPLL, this algorithm can be made more efficient by :

1) testing for 'contradiction clauses' (clauses that contain a literal as well as its complement) ... since a contradiction clause represents a contradiction, the clause set is a tautology iff the clause set without this clause is a tautology, hence 'contradiction clauses' can be removed at the start of the algorithm.

2) testing for pure literals (literals that occur in the clause set while its complement does not) ... in order for the clause set to be a tautology, it better be true whenever that literal is set to false ... meaning that all clauses containing pure literals can be removed at any point during the algorithm.

3) splitting on unit clauses (clauses containing a single literal).

4) instead of waiting for the clause set to be $\{\{\}\}$, we can return True as soon as $\{\}$ is in the clause set.

Answer 2

some formula $f$ is tautological iff $\neg f$ is unsatifiable. If you negate a DNF formula, you naturally get a CNF formula. On that you can run the usual DPLL algorithm.

Answer 3

If you apply duality (swap $\vee$s and $\wedge$s) to your DNF and then feed the resulting CNF formula to a CNF-SAT solver, the answer is "unsatisfiable" if and only the original DNF formula is valid. (Provided the solver is given enough time to terminate.)

You could instead apply De Morgan's. The difference is that you would also negate all literals, but it's not necessary if all you care is the yes/no answer.

Note that DPLL is just an algorithm, and nowadays CDCL is the preferred name for the algorithm implemented in most state-of-the-art SAT solvers.