i haven't done solver stuff in maybe a year, i wonder if z3 works any better than it used to? it used to have problems with problems that other solvers could solve

@notwa isn't this somewhat true of every automatic prover? The design space is so large that there is always a way to do a little bit better than the existing competitors for some category of inputs, and they each do?

@spun_off true, but z3 struggled with quantifier-free bitvector problems that SAT solvers with my unoptimized bit-blaster could solve in seconds. i worry that this kind of thing leaves a bad taste for any newcomers to solvers.

@notwa For properties that come from program verification (among other classes of problems), Z3 has the highest success rate overall. Don't worry about it leaving a bad taste, if every solver out there was as consistently good at at least one thing, people would find automatic solvers more usable.

@notwa Damien Doligez (working on Zenon) told me that Zenon was solving problems where the conclusion to prove or disprove was exactly one of the hypotheses modulo alpha-conversion better than every other provers, because it has techniques that made this trivial and other provers didn't. It's just a large design space.

Sign in to participate in the conversation

cybrespace: the social hub of the information superhighway jack in to the mastodon fediverse today and surf the dataflow through our cybrepunk, slightly glitchy web portal support us on patreon or liberapay!