sbv-7.0: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.SBV.Examples.Optimization.Production

Description

Solves a simple linear optimization problem

Synopsis

Documentation

production :: Goal Source #

Taken from http://people.brunel.ac.uk/~mastjjb/jeb/or/morelp.html

A company makes two products (X and Y) using two machines (A and B).

  • Each unit of X that is produced requires 50 minutes processing time on machine A and 30 minutes processing time on machine B.
  • Each unit of Y that is produced requires 24 minutes processing time on machine A and 33 minutes processing time on machine B.
  • At the start of the current week there are 30 units of X and 90 units of Y in stock. Available processing time on machine A is forecast to be 40 hours and on machine B is forecast to be 35 hours.
  • The demand for X in the current week is forecast to be 75 units and for Y is forecast to be 95 units.
  • Company policy is to maximise the combined sum of the units of X and the units of Y in stock at the end of the week.

How much of each product should we make in the current week?

We have:

>>> optimize Lexicographic production
Optimal model:
  X     = 45 :: Integer
  Y     =  6 :: Integer
  stock =  1 :: Integer

That is, we should produce 45 X's and 6 Y's, with the final maximum stock of just 1 expected!