Re: to CNF efficiently

Thank you very much. I got it there. It's simple and easy to be programmed.

Thomas A. Li


"Daniel A. Jimenez" <djimenez@xxxxxxxxxxxxx> wrote in message
news:d96kc2$4s7$1@xxxxxxxxxxxxxxxxxxxxxxxxxx
> 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 the ...
    (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)