4 ms·
I like this idea too, but bear in mind that the world of SMT in general (Z3 not an exception) seems to have a lot of cosmetically-similar formulations some of w
by glangdale 7y ago
I like this idea too, but bear in mind that the world of SMT in general (Z3 not an exception) seems to have a lot of cosmetically-similar formulations some of which are trivial and some of which will take forever to solve.
The honeymoon with SMT is often brief. You've gotten through the whole 'hooray, now I can nuke Sudoko and those "Mr Brown lives on the same street as the baker, who has a white house" problems' and surely all the world's problems will fall to my awesome new abilities. You then put some basic quantifier problems into Z3 or whatever and watch the prompt go away, apparently permanently.
I'd love it if there were more "intermediate" level documentation sets on SMT - aimed not at people who have just started using SMT, but also not aimed at people who are going to start doing SMT research.
- akgvn 7y ago> I'd love it if there were more "intermediate" level documentation sets on SMT - aimed not at people who have just started using SMT, but also not aimed at people who are going to start doing SMT research. Agreed. I've been doing some research to create an SAT Solver and found surprisingly low amount of learning material. I'd love some recommendations from HN crowd.
- taejo 7y agoI learned a good foundation of how SAT solvers work in this course: http://resources.mpi-inf.mpg.de/departments/rg1/teaching/autrea-ws17/readings.html http://resources.mpi-inf.mpg.de/departments/rg1/teaching/aut... Lecture notes are there; exercises are available in the linked earlier instances of the course.
- mmoskal 7y agoI wrote a paper on this a few years ago http://moskal.me/pdf/prtrig.pdf http://moskal.me/pdf/prtrig.pdf though indeed getting the quantifiers to verify is more art than science...