OpenCog as an SMT solver

[Ivan V.]

Respected OC community,

If I understood correctly, OpenCog can be used an an SMT solver. Considering this feature, how far OpenCog is from solving satisfiability problem for propositional logic in polynomial time complexity?

In explanation, I'm having a hunch about anti-axioms which derive all the contradictory anti-theorems. If, and only if a propositional logic formula belongs to such a set of anti-theorems, then it is not satisfiable. Can such anti-axioms be defined in OpenCog, maybe in URE?

Did anyone try to measure actual processing time of such an approach? If not, what obstacles do you see in this approach?

Any thoughts would be greatly appreciated.

Finest regards,

ivan v.

[Ben Goertzel]

Implementing an SMT solver in MeTTa for Hyperon would be a fun and
rewarding exercise. If Greg Meredith's acceleration of MeTTa
execution via rholang works out as planned, this could yield a fast as
well as elegant way to get SMT solving done.

Of course what one could hopefully get this way would be something
that is rapid in the average case encountered in practice, there is
nothing special about implementation in (any version of) OpenCog
that's going to automagically prove P equals NP as a side-effect ;)

ben

> --
> You received this message because you are subscribed to the Google Groups "opencog" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to opencog+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/opencog/f40317fb-fbe1-41d7-bf19-c2c4fa48d1d8n%40googlegroups.com.



--
Ben Goertzel, PhD
b...@goertzel.org

"My humanity is a constant self-overcoming" -- Friedrich Nietzsche

[Дмитрий Радомский]

Yes, you understand correctly that time matters. I have a colleague who will help me to fully form a model. Of course, no one has conducted such studies yet. I need a visa to the USA so that I can open a legal entity in the USA and start a startup. 

+79019067791 

@radomskii - telegram

ср, 19 июл. 2023 г., 20:10 Ben Goertzel <bengo...@gmail.com>:

To view this discussion on the web visit https://groups.google.com/d/msgid/opencog/CACYTDBfEKj1%3DRV1HQOsse%2B70L9Fsh%2BL6YnwT9x6FoCAgdQibOQ%40mail.gmail.com.

[Linas Vepstas]

Hi Ivan,

What is an anti-axiom?

Atomese is designed to "represent anything", and so, in principle, you can represent "anti-axioms" (whatever those are).

The query engine (aka "pattern matcher") can be used to perform simple forward chaining: so, if you have a rule that accepts anti-axioms as input, and produces more as output, then you can chain away as desired. It is (by definition) SMT, simply because it can chain "anything".  (The unifier can also "unify anything".)

However, when academics say "SMT", they usually envision something very different: a highly optimized SAT solver that has a custom API that allows "theories" to be defined (and thus, "solved"). This is "easy" to do in principle, but hard to do in practice, since the theories themselves might be hard to solve efficiently. Consider, for example, linear algebra: sounds easy, but in real life, there are fancy algorithms that solve linear programming problems. Attaching existing linear programming or integer programming codes to a SAT solver is hard/impossible.

To conclude, yes, Atomese can do SMT, but what it does does not conform to the conventional academic definition of SMT.

SAT itself is a collection of algorithms that are highly optimized to solve certain kinds of boolean problems.  The AtomSpace does not have a built-in SAT solver, due to a lack of interest in such a capability. I think I know how well you can program, and I think you could add this yourself, if you were interested. It might take you several months, maybe a bit more.  I suspect you are not interested in this :-/

Performance: you can use the query engine to do forward chaining. With some cleverness, you can go backwards, too. Performance is roughly a thousand steps per second, but that depends strongly on the number of rules, the size of the dataset, the complexity of the rules, etc.  All the usual caveats of chaining apply: if you have a combinatorial explosion, then you have a combinatorial explosion, and you are out of luck.

Some kinds of combinatorial explosion in some kinds of chaining problems are "easy" to avoid. If you can express your problem as a graph, and that graph factors into a tangle, plus many trees attached to that tangle, then you can prune the trees, solve the tangle, and then re-attach the trees.  This is what SAT solvers do. SMT is "hard" because the trees get tangled into the central tangle, and so you don't get any performance advantage. You end up having to brute-force an NP problem.

I'm still very excited by hypervector computing, but I do not have any words of wisdom to impart.

-- Linas

--

You received this message because you are subscribed to the Google Groups "opencog" group.
To unsubscribe from this group and stop receiving emails from it, send an email to opencog+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/opencog/f40317fb-fbe1-41d7-bf19-c2c4fa48d1d8n%40googlegroups.com.

--

Patrick: Are they laughing at us?

Sponge Bob: No, Patrick, they are laughing next to us.

 

[Дмитрий Радомский]

Comrade, if you are interested in strong artificial intelligence, then write. I know your technology with perceptrons, I'm not interested in it. Write the contacts of people who want agi and are willing to pay for it.

чт, 20 июл. 2023 г., 14:10 Linas Vepstas <linasv...@gmail.com>:

To view this discussion on the web visit https://groups.google.com/d/msgid/opencog/CAHrUA36%3DOdvD29a%3De2j6Jhui2_gt%3D%3DB3G0Z8m688-x-bexQV3w%40mail.gmail.com.

[Ivan V.]

Linas,

The basic idea is this: I define some set of axioms, and I define a falsehood as a starting point. Chaining forward on, from falsehood I derive all the contradictory formulas. What I want is to pass an arbitrary formula, and check if it is contradictory. (This could also be implemented by a normal theorem constructor and passing a negated arbitrary formula to check if it is valid.)

The question is: is there an automation in OC that will simply output an yes/no answer, or do I have to do every chaining step manually until I reach the passed formula or I eventually give up? I may be interested in automating this process if it can be shown that it does its computation in polynomial time in the worst case scenario.

ivan v.

To view this discussion on the web visit https://groups.google.com/d/msgid/opencog/CAAT0KVZE41Gucwwu9NgDz4f5mUr2e3TZEMGiUGA7%3Do2%3D9HT-oA%40mail.gmail.com.

[Linas Vepstas]

Hi Ivan,

What you describe in the first paragraph sounds like what SAT solvers do. The actual algorithm doesn't "start from falsehood", nor does it chain; it picks it's own starting point and runs in the sequence that it wants to. It quickly returns a yes/no answer as to whether a collection of statements is satisfiable or not.

Negation in SAT solvers is very interesting -- if you have a variable x, and you have expressions that contain not-x then SAT solvers work best if you use a new variable, call it nx, and then, only at the very end, check to see if nx is equal to not-x.  If you declare that nx equals not-x at the very beginning, the algo runs thousands/millions of times slower. It takes a while to understand this.

If you can formulate your axioms (or their negations) as prolog, then I recommend the U. Potsdam ASP solver. It's excellent (or at least, was, when I used it a decade ago.)

In many ways, prolog statements are "just like" the "jigsaw pieces" that I keep talking about -- given a set of jigsaw pieces, they can either be assembled, or not. ("satisfied" or not). Atomese does have a "jigsaw constraint satisfaction" solver: this is Link Grammar. It's fairly general; the "best API" is a work-in-progress. It runs just as fast as SAT solvers, mostly because it uses SAT-like algorithms.

I have not attempted a prolog-to-link-grammar converter or bridge. That would be interesting and educational.

Performance: well, that depends very strongly on the actual dataset. It is "well known" that SAT solvers solve certain problems in N logN time.  Others in N^2 or N^3. It is "well known" that "most typical" user problems can be solved in linear or polynomial time. It is also known that you can write out problems that require N-factorial time. It depends strongly on the actual problem.  Thus, SAT solvers have a reputation for being "blindingly fast" for "most user problems", especially when compared to chaining. 

A standard beginner mistake is to use not-x instead of introducing a new variable nx -- this mistake will convert linear runtime problems into N-factorial problems. The books and tutorials all mention this mistake at the very beginning, but it is hard to understand, until you actually play with it for a few weeks. Then, one day, you go "ah ha!".  The meta-theory behind this is the theory of "intuitionistic logic" vs. "classical logic". Roughly speaking, the law of the excluded middle converts polynomial-time problems into factorial-time problems.

Anyway, all of the above deals with "crisp logic", true/false problems. Most of what I work on involves probabilities and counting, where most of the above ideas offer little benefit.

--linas

To view this discussion on the web visit https://groups.google.com/d/msgid/opencog/CAB5%3Dj6UyxAe70LFYcs9OM6GwczpRpJBx1RF6n1R266ufMVcktA%40mail.gmail.com.