| View previous topic :: View next topic |
| Author |
Message |
newbie
Guest
|
 Posted: Mon Oct 06, 2008 4:30 pm Post subject: about CNF converting |
 |
|
Hi all,
did somebody know if is possible to use a non
deterministic algorithm in order to convert
every boolean propositional formula into
an equivalent CNF formula?
Thanks a lot
Regards |
|
| |
|
 Back to top |
newbie
Guest
|
| Posted: Mon Oct 06, 2008 4:35 pm Post subject: Re: about CNF converting |
|
|
"newbie" <newbie@newbie.new> ha scritto nel messaggio
news:OFmGk.165518$FR.452835@twister1.libero.it...
[quote]Hi all,
did somebody know if is possible to use a non
deterministic algorithm in order to convert
every boolean propositional formula into
an equivalent CNF formula?
Thanks a lot
Regards
obviously non deterministic polynomial I mean[/quote]
Regards |
|
| |
|
| Back to top |
Guest
|
| Posted: Tue Oct 07, 2008 1:49 am Post subject: Re: about CNF converting |
|
|
On Oct 6, 7:35 am, "newbie" <new...@newbie.new> wrote:
[quote]"newbie" <new...@newbie.new> ha scritto nel messaggionews:OFmGk.165518$FR..452835@twister1.libero.it...> Hi all,
did somebody know if is possible to use a non
deterministic algorithm in order to convert
every boolean propositional formula into
an equivalent CNF formula?
Thanks a lot
Regards
obviously non deterministic polynomial I mean
Regards
[/quote]
I>m not positive, so someone correct me if I>m wrong, but my answer
would be no. My reason for saying this is that converting a formula
to CNF can cause the length of the formula to grow exponentially, and
a nondeterministic algorithm that runs in polynomial time would have
to somehow get to the full formula in polynomial time, while guessing
something that is polynomial-bounded with respect to the length of the
original formula. Since the final formula may not be polynomial-
bounded, there wouldn>t be a way for the nondeterministic machine to
guess it in polynomial time.
Those are just my thoughts though...I>m not an expert.
-Phil |
|
| |
|
| Back to top |
David G Mitchell
Guest
|
| Posted: Wed Oct 08, 2008 8:25 pm Post subject: Re: about CNF converting |
|
|
In article <op.uip2ghhaft6h9m@paprika>,
Jym <Jean-Yves.Moyen+news@ens-lyon.org> wrote:
[quote]On Tue, 07 Oct 2008 03:49:04 +0200, <cplxphil@gmail.com> wrote:
....
But SAT being NP (quite trivially), and CNF-SAT being NP-complete, there
should even be a deterministic polynomial algorithm to turn any boolean
formula into a CNF one.
Well, even turning it into a 3-CNF formula has to be doable in
deterministic polynomial time.
[/quote]
This is true. The question, regarding the OP, is: Is the
resulting formula logically equivalent to the original?
Every intro discrete math text I>ve seen has the answer to
the OP>s his question -- along the lines of a previous response
in this thread regarding the size of an equivalent CNF formula.
DM |
|
| |
|
| Back to top |
Mitch
Guest
|
| Posted: Wed Oct 08, 2008 8:59 pm Post subject: Re: about CNF converting |
|
|
On Oct 8, 4:25 pm, mitch...@cs.sfu.ca (David G Mitchell) wrote:
[quote]In article <op.uip2ghhaft6h9m@paprika>,
Jym <Jean-Yves.Moyen+n...@ens-lyon.org> wrote:
On Tue, 07 Oct 2008 03:49:04 +0200, <cplxp...@gmail.com> wrote:
...
But SAT being NP (quite trivially), and CNF-SAT being NP-complete, there
should even be a deterministic polynomial algorithm to turn any boolean
formula into a CNF one.
Well, even turning it into a 3-CNF formula has to be doable in
deterministic polynomial time.
This is true. The question, regarding the OP, is: Is the
resulting formula logically equivalent to the original?
[/quote]
The usual proof of NP-completeness for satisfiability of CNF (by
messing with the syntax tree, assigning a new boolean variable to the
root of each subtree) just -preserves satisfiability- (the original
formula is satisfiable iff the new one is). I don>t know (and I can>t
seem to think easily) if having a bunch of new slack variables counts
as equivalent.
Mitch |
|
| |
|
| Back to top |
Jym
Guest
|
| Posted: Thu Oct 09, 2008 1:13 am Post subject: Re: about CNF converting |
|
|
On Tue, 07 Oct 2008 03:49:04 +0200, <cplxphil@gmail.com> wrote:
[quote]On Oct 6, 7:35 am, "newbie" <new...@newbie.new> wrote:
"newbie" <new...@newbie.new> ha scritto nel
messaggionews:OFmGk.165518$FR.452835@twister1.libero.it...> Hi all,
did somebody know if is possible to use a non
deterministic algorithm in order to convert
every boolean propositional formula into
an equivalent CNF formula?
Thanks a lot
Regards
obviously non deterministic polynomial I mean
Regards
I>m not positive, so someone correct me if I>m wrong, but my answer
would be no. My reason for saying this is that converting a formula
to CNF can cause the length of the formula to grow exponentially, and
a nondeterministic algorithm that runs in polynomial time would have
to somehow get to the full formula in polynomial time, while guessing
something that is polynomial-bounded with respect to the length of the
original formula. Since the final formula may not be polynomial-
bounded, there wouldn>t be a way for the nondeterministic machine to
guess it in polynomial time.
[/quote]
I>m suddently not sure whether I understood the question correctly...
But SAT being NP (quite trivially), and CNF-SAT being NP-complete, there
should even be a deterministic polynomial algorithm to turn any boolean
formula into a CNF one.
Well, even turning it into a 3-CNF formula has to be doable in
deterministic polynomial time.
--
Hypocoristiquement,
Jym. |
|
| |
|
| Back to top |
Jym
Guest
|
| Posted: Thu Oct 09, 2008 2:01 am Post subject: Re: about CNF converting |
|
|
On Wed, 08 Oct 2008 22:25:35 +0200, David G Mitchell <mitchell@cs.sfu.ca>
wrote:
[quote]In article <op.uip2ghhaft6h9m@paprika>,
Jym <Jean-Yves.Moyen+news@ens-lyon.org> wrote:
On Tue, 07 Oct 2008 03:49:04 +0200, <cplxphil@gmail.com> wrote:
...
But SAT being NP (quite trivially), and CNF-SAT being NP-complete, there
should even be a deterministic polynomial algorithm to turn any boolean
formula into a CNF one.
Well, even turning it into a 3-CNF formula has to be doable in
deterministic polynomial time.
This is true. The question, regarding the OP, is: Is the
resulting formula logically equivalent to the original?
[/quote]
Oh. Right. The formula resulting of the reduction needs to have the same
satisfiability status than the original one, but doesn>t need to be
logically equivalent to it. My bad.
--
Hypocoristiquement,
Jym. |
|
| |
|
| Back to top |
Guest
|
| Posted: Thu Oct 09, 2008 2:04 am Post subject: Re: about CNF converting |
|
|
In article <01062fa1-df73-49dc-b588-ae1548018a3a@k13g2000hse.googlegroups.com>,
<cplxphil@gmail.com> wrote:
[quote]On Oct 6, 7:35 am, "newbie" <new...@newbie.new> wrote:
"newbie" <new...@newbie.new> ha scritto nel
messaggionews:OFmGk.165518$FR.452835@twister1.libero.it...> Hi all,
did somebody know if is possible to use a non
deterministic algorithm in order to convert
every boolean propositional formula into
an equivalent CNF formula?
[...]
I>m not positive, so someone correct me if I>m wrong, but my answer
would be no. My reason for saying this is that converting a formula
to CNF can cause the length of the formula to grow exponentially
[/quote]
This is true if you>re not allowed to introduce any new "auxiliary"
variables. Usually, though, by an "equivalent" formula, one means that
the algorithm just has to convert satisfiable instances to satisfiable
instances and unsatisfiable instances to unsatisifiable instances. It
is permissible to add extra variables in the process if desired. With
this understanding, there is a deterministic polynomial-time algorithm,
which you can find in any complexity theory text.
--
Tim Chow tchow-at-alum-dot-mit-dot-edu
The range of our projectiles---even ... the artillery---however great, will
never exceed four of those miles of which as many thousand separate us from
the center of the earth. ---Galileo, Dialogues Concerning Two New Sciences |
|
| |
|
| Back to top |
newbie
Guest
|
| Posted: Thu Oct 09, 2008 3:06 am Post subject: Re: about CNF converting |
|
|
"Jym" <Jean-Yves.Moyen+news@ens-lyon.org>
[quote]I>m suddently not sure whether I understood the question correctly...
[/quote]
Thre really problem is:
input: a propositional formula
output: a formula in CNF in canonical form logical equivalent to the
input formula.
Question: does exist a nondeterministic algoritm that receives the input
and give the output in polynomial time?
regards |
|
| |
|
| Back to top |
Daniel A. Jimenez
Guest
|
| Posted: Thu Oct 09, 2008 5:49 am Post subject: Re: about CNF converting |
|
|
In article <_9aHk.78266$Ca.20252@twister2.libero.it>,
newbie <newbie@newbie.new> wrote:
[quote]"Jym" <Jean-Yves.Moyen+news@ens-lyon.org
I>m suddently not sure whether I understood the question correctly...
Thre really problem is:
input: a propositional formula
output: a formula in CNF in canonical form logical equivalent to the
input formula.
Question: does exist a nondeterministic algoritm that receives the input
and give the output in polynomial time?
regards
[/quote]
I believe that a decision-problem version of this problem (e.g. deciding
whether the number of clauses in the CNF is greater than some integer) would
be complete for NP with an NP oracle. So there is probably not an algorithm,
nondeterministic or otherwise, for solving the decision problem in polynomial
time unless the polynomial hierarchy collapses to its second level.
For the conversion algorithm, the output itself could be exponential in
the size of the input (e.g. for the parity function of n variables) so you
would have to be careful how to pose the problem so that "polynomial time"
makes sense.
--
Daniel Jimenez djimenez@cs.utexas.edu
"I>ve so much music in my head" -- Maurice Ravel, shortly before his death.
" " -- John Cage |
|
| |
|
| Back to top |
David G Mitchell
Guest
|
| Posted: Fri Oct 10, 2008 7:48 pm Post subject: Re: about CNF converting |
|
|
In article <48ed2059$0$300$b45e6eb0@senator-bedfellow.mit.edu>,
<tchow@lsa.umich.edu> wrote:
[quote]
variables. Usually, though, by an "equivalent" formula, one means that
the algorithm just has to convert satisfiable instances to satisfiable
instances and unsatisfiable instances to unsatisifiable instances. It
[/quote]
In most SAT and logic-related literature, "equivalent formula"
means logically equivalent. Many authors in SAT and related
areas to use "satisfiability-equivalent" when reduction, but not
necessarily logical equivalence, is needed.
Of course, if you understand the role of the new variables
in e.g., Tseitin>s reduction from SAT to 3-SAT, they are only
moderately interesting and sometimes the distinction is glossed
over.
DM |
|
| |
|
| Back to top |
|
