3 ms·

To my point, how much do you think a SMT solution costs now?

roenxi 2y ago
Couple of thousand dollars? Consultant turns up on site, gathers data, talks to a few people, sets up a model and solves it. Probably around a weeks work @ say $100/hr. Might be under-calling it for validation and there'll probably be some iteration to do so a project will take a few solves to complete + overheads.
- cjbgkagh 2y ago
  The software is free, and few people even think about the hardware cost. But that’s not how it always was, it was a core part of Bill Gates world domination plan during the ‘foundation’ era (2008). Good ones used to be super expensive, then they were sold as excel plugins, and now Z3 is given away for free. And despite being free it’s still not used nearly as often as it should be, it’s not the algorithm or price holding back adoption it’s the people. It was assumed that there was this huge untapped demand curve at the long end of the tail before finding out that there really was not. Z3 was originally released as academic use only (2012) on the assumption that it would drive demand for commercial use of Z3 or another commercial solution. Once it became clear that wasn’t going to make any real money they allowed it to be released for commercial use as well (2015). As an aside people still do pay for SMT solvers so the market hasn’t completely disappeared but it’s clearly not what it was thought to be.
  - roenxi 2y ago
    Your point being? You're stringing together a bunch of observations without any argument relevant to Jevons' paradox. My guess is that you're mistake is thinking something like [demand = 1/price]. That was never the prediction, the prediction is when efficiency improves, demand increases which is a pretty basic observation for most in-practice supply and demand curves (something like a Veblen good would be different). You're not talking about changes in demand and you're barely looking at efficiency beyond noticing that the price was positive and is now 0. > And despite being free it’s still not used nearly as often as it should be ... Case in point, if this wasn't obvious then you need to modify your expectations. Jevons' paradox predicts exactly this, because there are prices below free (ie, paying someone to use the thing) and we'd expect they eventuated people would find new uses for SMT solvers due to Jevons' paradox in context of a price signal that they were getting more efficient. That implies even at $0 in software costs we aren't going to be using them everywhere we could.

Couple of thousand dollars? Consultant turns up on site, gathers data, talks to a few people, sets up a model and solves it. Probably around a weeks work @ say $100/hr. Might be under-calling it for validation and there'll probably be some iteration to do so a project will take a few solves to complete + overheads.

cjbgkagh 2y ago
The software is free, and few people even think about the hardware cost. But that’s not how it always was, it was a core part of Bill Gates world domination plan during the ‘foundation’ era (2008). Good ones used to be super expensive, then they were sold as excel plugins, and now Z3 is given away for free. And despite being free it’s still not used nearly as often as it should be, it’s not the algorithm or price holding back adoption it’s the people. It was assumed that there was this huge untapped demand curve at the long end of the tail before finding out that there really was not. Z3 was originally released as academic use only (2012) on the assumption that it would drive demand for commercial use of Z3 or another commercial solution. Once it became clear that wasn’t going to make any real money they allowed it to be released for commercial use as well (2015). As an aside people still do pay for SMT solvers so the market hasn’t completely disappeared but it’s clearly not what it was thought to be.
- roenxi 2y ago
  Your point being? You're stringing together a bunch of observations without any argument relevant to Jevons' paradox. My guess is that you're mistake is thinking something like [demand = 1/price]. That was never the prediction, the prediction is when efficiency improves, demand increases which is a pretty basic observation for most in-practice supply and demand curves (something like a Veblen good would be different). You're not talking about changes in demand and you're barely looking at efficiency beyond noticing that the price was positive and is now 0. > And despite being free it’s still not used nearly as often as it should be ... Case in point, if this wasn't obvious then you need to modify your expectations. Jevons' paradox predicts exactly this, because there are prices below free (ie, paying someone to use the thing) and we'd expect they eventuated people would find new uses for SMT solvers due to Jevons' paradox in context of a price signal that they were getting more efficient. That implies even at $0 in software costs we aren't going to be using them everywhere we could.