Re: to CNF efficiently

In article <Iv2dnd1n3r6pXSvfRVn-pQ@xxxxxxxxxx>,
Thomas A. Li <tli@xxxxxxxxxxxxx> wrote:
>Given a Boolean Expression of length n, how to convert it into a CNF of
>length m, which is a polynomial of n?
>Here the length is defined as the number of variables, parenthesis pairs and
>operators. CNF stands for conjunctive norm form.
>
>In traditional conversion, the use of distribution may "double" the length,
>e.g. A+BC ==> (A+B)(A+C) where A is doubled. If the length of A is much
>bigger than B and C, the result has "nearly" double length. Can somebody
>give a firm proof about whether the length is kept polynomial or not in the
>conversion?
>
>>From Cook's proof of NP-completeness, a Boolean expression can be
>transformed into a CNF of polynomial length, but it is not intuitive.
>
>Is there another intuitive algorithm to do so? Any reference will be
>appreciated.

Cook's theorem can be proven with something slightly different: an algorithm
to transform a general Boolean formula phi into a CNF phi' such that phi
is satisfiable if and only if phi' is satisfiable. This involves adding
extra variables, so it is not the case that phi is equivalent to phi' where
"equivalent" means "has the same truth table" as you would get by using the
distributive law over and over. Of course, the nice thing is that phi'
has a size polynomial in the size of phi. Cormen et al. (the algorithms
book) discusses this transformation in the section on NP-completeness.
As I recall they do it with circuits instead of general Boolean formulas
but the idea is the same. Basically, the idea is to label the results of
all logical operations with new variable names and then use CNF to state the
effect of those logical operations, e.g. for something like (a & (b | c))
you would introduce new variables by equating them to the logical operations
i.e. x = (b | c) and y = (a & x). Then you use CNF to logically state that
"x is equivalent to b | c" and "y is equivalent to a & x" i.e. (b | c | !x) &
(!c | x) & (!b | x) for the first equivalence and (!a | !x | y) & (x | !y) &
(a | !y) for the second equivalence. Add a clause to state that the output
of the formula is equal to true, e.g. ( y ). Put all the clauses together,
and if the resulting CNF is satisfiable, then so is the original formula.
It's easy to derive the generic CNFs that state that some variable is
equivalent to some logical operation on one or two other variables by
just sitting down and writing out a Karnaugh map for the equivalence,
circling the zeros, and then using DeMorgan's laws to get the CNF.
--
Daniel Jiménez djimenez@xxxxxxxxxxxxx
"I've so much music in my head" -- Maurice Ravel, shortly before his death.
" " -- John Cage
.

Relevant Pages

  • Re: to CNF efficiently
    ... CNF stands for conjunctive norm form. ... a Boolean expression can be ... > to transform a general Boolean formula phi into a CNF phi' such that phi ... > all logical operations with new variable names and then use CNF to state ...
    (comp.theory)
  • to CNF efficiently
    ... CNF stands for conjunctive norm form. ... give a firm proof about whether the length is kept polynomial or not in the ... a Boolean expression can be ... Is there another intuitive algorithm to do so? ...
    (comp.theory)