toysolver-0.9.0: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc

Copyright	(c) Masahiro Sakai 2011
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	provisional
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010
Extensions	ScopedTypeVariables ExplicitForAll

ToySolver.Arith.Simplex.Textbook.LPSolver

Contents

Solver type
LP monad
Problem specification
Solving
Extract results
Utilities

Description

Naïve implementation of Simplex method

Reference:

http://www.math.cuhk.edu.hk/~wei/lpch3.pdf

Synopsis

type Solver r = (Var, Tableau r, VarSet, VarMap (Expr r))
emptySolver :: VarSet -> Solver r
type LP r = State (Solver r)
getTableau :: LP r (Tableau r)
putTableau :: Tableau r -> LP r ()
newVar :: LP r Var
addConstraint :: Real r => Atom r -> LP r ()
addConstraintWithArtificialVariable :: Real r => Atom r -> LP r ()
tableau :: RealFrac r => [Atom r] -> LP r ()
define :: Var -> Expr r -> LP r ()
phaseI :: (Fractional r, Real r) => LP r Bool
simplex :: (Fractional r, Real r) => OptDir -> Expr r -> LP r Bool
dualSimplex :: (Fractional r, Real r) => OptDir -> Expr r -> LP r Bool
data OptResult
- = Optimum
- | Unsat
- | Unbounded
twoPhaseSimplex :: (Fractional r, Real r) => OptDir -> Expr r -> LP r OptResult
primalDualSimplex :: (Fractional r, Real r) => OptDir -> Expr r -> LP r OptResult
getModel :: Fractional r => VarSet -> LP r (Model r)
collectNonnegVars :: forall r. RealFrac r => [Atom r] -> VarSet -> (VarSet, [Atom r])

Solver type

type Solver r = (Var, Tableau r, VarSet, VarMap (Expr r)) Source #

emptySolver :: VarSet -> Solver r Source #

LP monad

type LP r = State (Solver r) Source #

getTableau :: LP r (Tableau r) Source #

putTableau :: Tableau r -> LP r () Source #

Problem specification

newVar :: LP r Var Source #

Allocate a new non-negative variable.

addConstraint :: Real r => Atom r -> LP r () Source #

Add a contraint, without maintaining feasibilty condition of tableaus.

Disequality is not supported.
Unlike addConstraintWithArtificialVariable, an equality constraint becomes two rows.

addConstraintWithArtificialVariable :: Real r => Atom r -> LP r () Source #

Add a contraint and maintain feasibility condition by introducing artificial variable (if necessary).

Disequality is not supported.
Unlike addConstraint, an equality contstraint becomes one row with an artificial variable.

tableau :: RealFrac r => [Atom r] -> LP r () Source #

define :: Var -> Expr r -> LP r () Source #

Solving

phaseI :: (Fractional r, Real r) => LP r Bool Source #

simplex :: (Fractional r, Real r) => OptDir -> Expr r -> LP r Bool Source #

dualSimplex :: (Fractional r, Real r) => OptDir -> Expr r -> LP r Bool Source #

data OptResult Source #

results of optimization

Constructors

Optimum
Unsat
Unbounded

Instances

Instances details

Show OptResult Source #
Instance details Defined in ToySolver.Arith.Simplex.Textbook.LPSolver Methods showsPrec :: Int -> OptResult -> ShowS # show :: OptResult -> String # showList :: [OptResult] -> ShowS #
Eq OptResult Source #
Instance details Defined in ToySolver.Arith.Simplex.Textbook.LPSolver Methods (==) :: OptResult -> OptResult -> Bool # (/=) :: OptResult -> OptResult -> Bool #
Ord OptResult Source #
Instance details Defined in ToySolver.Arith.Simplex.Textbook.LPSolver Methods compare :: OptResult -> OptResult -> Ordering # (<) :: OptResult -> OptResult -> Bool # (<=) :: OptResult -> OptResult -> Bool # (>) :: OptResult -> OptResult -> Bool # (>=) :: OptResult -> OptResult -> Bool # max :: OptResult -> OptResult -> OptResult # min :: OptResult -> OptResult -> OptResult #

twoPhaseSimplex :: (Fractional r, Real r) => OptDir -> Expr r -> LP r OptResult Source #

primalDualSimplex :: (Fractional r, Real r) => OptDir -> Expr r -> LP r OptResult Source #

Extract results

getModel :: Fractional r => VarSet -> LP r (Model r) Source #

Utilities

collectNonnegVars :: forall r. RealFrac r => [Atom r] -> VarSet -> (VarSet, [Atom r]) Source #