Note that generating a grounding of boolean variables that satisfy a boolean expression is NP-complete (in general). That is just one of the many problem that lie a the bottom of conditional (if/else) logic (i.e. procedural programming).
Untitled topic
21–30 of 31 posts
Re: undefined
#22If this interests you, please do check out prolog. Declarative languages let you do something quite similar. In particular, they let you specify what you want the computer to give you rather than what you want the computer to do. Believe it or not, a very good example of such a language which you might be familiar with is SQL.
I don't believe it, because I use SQL every day, and I need to tell it which rows to lock when reading, whether to read them in share mode or fully, sometimes I need to help it figure out which indexes to use (of course I also have to manually set up the indexes too), when doing transactions I need to tell it how exactly to isolate the transaction, and I need to be very careful how I order my queries in order to avoi…
Prolog is a very different beast, in that it doesn't rely on any "thick" abstraction. It's based on resolution [1], thus the way code is executed is straightforward and unsurprising (providing you understand resolution first).
If you have never tried it out you should, maybe you will like declarative languages a little bit more afterwards.
Re: undefined
#23I'm disappointed. I thought I was going to see the solver generates code that finds the largest palindrome. I recall how mini-Kanren was used to generate quines. Z3 should be capable of similar feats.
eval-quines are pretty mindblowing.
Re: undefined
#24Another related language is Maude. It's a term-rewriting language, so for example we can implement arithmetic by defining symbols to represent numerals (eg. "zero" and "successor") and some rewrite rules which implement addition, subtraction, multiplication, etc. This is similar to languages like Pure, which lets us write code in a pure-functional style, but with the bonus that rewriting can avoid awkward recursion schemes (eg. "a + b" can recurse on both arguments at once). This makes it well-suited to implementing domain-specific languages.
However, Maude can go further than other rewrite languages since it is also a model checker: if A rewrites to B, we can supply A and get back B; or we can supply B and have Maude search for an A. If A and B are DSL terms, we can derive terms from their properties, as is being discussed here.
We can also have Maude show that some terms are unreachable, for example that there is no input which rewrites to an Error symbol.
Of course the advantage to Z3 is that it's hooked up to fast domain-specific solvers (SAT, SMT, arithmetic, etc.), whilst Maude's search is general-purpose and therefore slower.
Re: undefined
#25Note that generating a grounding of boolean variables that satisfy a boolean expression is NP-complete (in general). That is just one of the many problem that lie a the bottom of conditional (if/else) logic (i.e. procedural programming).
Yes, it basically solves a SAT problem. But modern SAT solver are very very efficient. So although your worst case is exponential, in many cases heuristics will help find a solution very quickly. That's quite impressive; in fact, the motto "if you have a NP-hard problem just reduce it to SAT and throw a SAT solver on it" is becoming more and more common.
Re: undefined
#26I'm disappointed. I thought I was going to see the solver generates code that finds the largest palindrome. I recall how mini-Kanren was used to generate quines. Z3 should be capable of similar feats.
Well, as benjamincburns says in another comment, Z3 is basically equivalent to the finite domain solver of a Prolog. Since mini-Kanren is a Prolog, it is not surprising that it is more powerful. Otherwise Z3 would also be a Prolog :).
Re: undefined
#27Note that generating a grounding of boolean variables that satisfy a boolean expression is NP-complete (in general). That is just one of the many problem that lie a the bottom of conditional (if/else) logic (i.e. procedural programming).
Yes, it basically solves a SAT problem. But modern SAT solver are very very efficient. So although your worst case is exponential, in many cases heuristics will help find a solution very quickly. That's quite impressive; in fact, the motto "if you have a NP-hard problem just reduce it to SAT and throw a SAT solver on it" is becoming more and more common.
NP-complete is an unbreakable wall, strewn with the bloodied corpses of enthusiastic heuristic authors.
You can only break it if your problem domain was never NP-hard in the first place (e.g. sparse or some other exploitable structural features). Very very fast means nothing on a true NP-hard problem for quite modest n.
Note the author had to include a spurious constraint to get his system to converge, despite it being quite a small task in the first place. My point was that this approach has fundamental reasons why it won't scale to real programming tasks, of which the interesting ones that programmers get wrong all the time are likely to be the true NP-complete type.
Re: undefined
#28http://jheusser.github.io/2013/02/03/satcoin.html is an article giving an example of using this approach (using a SAT solver) to bitcoin mining- how you would specify the problem etc.
Re: undefined
#29This is fantastic, if you want to solve only maths problems. But when there is real state and real side-effects and real hardware matters, this sort of approach breaks down.
Re: undefined
#30Note that generating a grounding of boolean variables that satisfy a boolean expression is NP-complete (in general). That is just one of the many problem that lie a the bottom of conditional (if/else) logic (i.e. procedural programming).
Yes, it basically solves a SAT problem. But modern SAT solver are very very efficient. So although your worst case is exponential, in many cases heuristics will help find a solution very quickly. That's quite impressive; in fact, the motto "if you have a NP-hard problem just reduce it to SAT and throw a SAT solver on it" is becoming more and more common.
[deleted]