On Jan 21, 2008 1:35 AM, Ben Goertzel <[EMAIL PROTECTED]> wrote: > However, I would rephrase the question as: How would a pragmatically useful > polynomial time solution of logical satisfiability affect AGI? > > In fact, it's interesting to talk about how existing SAT and SMT solvers > > http://en.wikipedia.org/wiki/Satisfiability_modulo_theories > > -- which are often quite effective on surprisingly large real-world problems, > in spite of being exponential time in the worst case -- affect AGI.
SAT solvers got very powerful in last years. For example, they now can be used to model-check C programs of 10K+ lines of code, keeping track of all variables, targets of pointers, function calls, execution paths and so on. All this stuff gets encoded as a huge formula, satisfiability of which can indicate that, for example, no null pointer dereference happens. So, people do have a practically useful way of cheating problems in NP now. Problem with AGI is, we don't know how to program it even given computers with infinite computational power. The best we can imagine is evolving it automagically. -- Vladimir Nesov mailto:[EMAIL PROTECTED] ----- This list is sponsored by AGIRI: http://www.agiri.org/email To unsubscribe or change your options, please go to: http://v2.listbox.com/member/?member_id=8660244&id_secret=88008437-8a08a7
