[Haskell-cafe] [ANN] New release of SBV, now with optimization
erkokl at gmail.com
Mon May 8 03:25:44 UTC 2017
I'm happy to announce a new release of SBV (v6.0); a library for
seamlessly integrating SMT solvers with Haskell:
This version brings optimization features to SBV, where arithmetic goals
can be minimized or maximized. The algorithms employed are particularly
suitable for linear-optimization problems, over bounded/unbounded integers
and reals. Multiple objective functions with optimization priorities are
Objective values that assume their optimal values at infinity and epsilon
are also supported, allowing the user to express arbitrary combinations of
goals. Furthermore, soft-goals (i.e., those that can be violated with a
user-specified penalty) are included as well. Such goals can be used to
expressed "nice-to-have" constraints, for instance as they appear in
classic scheduling problems.
(Optimization is currently only supported by the z3-backend, and leverages
the features of the z3 SMT solver. Please make sure you get a fresh copy of
it from github <https://github.com/Z3Prover/z3>.)
A few basic examples:
- Basic linear optimization over reals
- Workshop product allocation
- Allocating virtual-machines in data-centers
This release also comes with a number of other changes/features, including
support for user given tactics, mainly aimed for advanced users. See here
<https://hackage.haskell.org/package/sbv-6.0/changelog> for details.
Bug reports, as always, are most welcome.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe