Hacker News Reader

Comment by jfries | Hacker News Reader

I would be super interested in more details on how that works. What do you actually pass to z3 to solve?

I wrote a superoptimizer using z3 here: https://github.com/falk-hueffner/sematrope . The idea is to have variables that encode the program and a giant if-then-else statement that represents program execution. Then for a list of input/output pairs you let the solver find a program encoding that yields correct outputs. Next you let the solver find a counterexample where the current program candidate does not give the correct result. If one is found, it is added to the list of input/output pairs, otherwise you have found a correct program.

What if the solver both fails to find a counterexample and fails to conclude there isn't one? (i.e. it times out)

That's very unlikely to happen, since finding a counterexample or proving there isn't one is much easier than finding a program candidate, so it'll usually time out in that phase.

OK, so what happens when it fails to find a candidate?

Then you learned something, I guess ("solving is hard"). I see a lot of timeouts with mine. Mine is 'easy' in that I'm looking for SIMD programs so the domain is essentially u8 "in lane only" SIMD code, so the small bit-width makes life easier.

I write something similar for my own problems. Usually a single instance alone isn’t going to cut it, so we run a portfolio of solvers and treat it like a multi armed bandit problem as to choose which solver with its specific hyper parameters is finding solutions / counter examples faster. A pretty common trick when you do this is to dynamically resize your portfolio with new solvers introduced with a high likelihood of solving fast based off the parameters of other solvers that are solving fast, a particle filter of sorts. This takes care of setting and handling individual solver timeouts, while allowing the user to specify not only a timeout for the whole portfolio, possibly lengthening when new solvers are introduced, but also a max delay between any two solutions.

Either way, you’re still forced to consider if the model can return sat or unsat, or a timeout. If it’s a timeout we don’t swap in the faster code, if it’s unsat then same deal, but if it’s sat we can get some new code to jump to

Right, the problem with SMT solvers (and the SAT solvers they're based on, although the problem there is slightly better) is that they're unpredictable and highly dependent on the form in which you pose the instance, often in very unintiitive ways (they can fail on an instance that you'd think would be as easy or even easier than another they do manage).

SAT/SMT hardness regression has come a long way, especially if you can insert profiling information for real instances.

If this is a production model for the cloud, the engineer should have put some thought into the encoding as to express sat/unsat clearly, if possible.

In the general case, sure, to some extent one can construct an adversarial example just as with NN (random 3-sat hardness cliff). Real world formulations of problems are either nice or atrocious IME, discoverable at dev time.

Oh, I don't mind adversarial examples. As a user of SMT solvers (for semi-automated program verification), I just find them unpredictable and frustrating. But I've never employed SMT solvers as a library in some production system, and it's good to hear that in that case the instances could be controlled well enough for the normal operation to be predictable.

Very cool. I will have to read through your implementation which seems tractably small enough that I can actually find stuff in it (unlike some of the bigger projects). This is pretty much how my superoptimizer works too. I'm very anxious that I'm doing something flagrantly stupid as I sort of half-read a few research papers and then went off to build something which worked...

User hairtuq gave a good summary. There seems to be a tension between pushing more work into the solver vs breaking up the problem into smaller sets, so there are many different designs. For example, I can pass thousands of candidate programs to the solver with opcodes specified ("please go get me some constants that make this program work for this task") or one completely unspecified program ("find me all the opcodes and all the programs") or some continuum between. My current experience is that partial specialization works well.

I have a lot of optimizations I'd like to apply. I'm doing the slightly brain-melting task of trying to get the super-optimizer to cough up its own optimization rules to speed the process, but that's a long topic and I'll be a lot chattier about if I see it ever work properly.

I'm also trying to figure out a way to make this pay in some fashion, being between jobs. Love to work on it more but I suspect reality will kick in soon.

Reply on news.ycombinator.com