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

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Documentation.SBV.Examples.Optimization.Production

Description

Solves a simple linear optimization problem

Synopsis

- production :: Goal

# 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!