linearEqSolver 1.0 → 1.1
raw patch · 6 files changed
+77/−62 lines, 6 filesdep ~sbvsetup-changed
Dependency ranges changed: sbv
Files
- LICENSE +1/−1
- Math/LinearEquationSolver.hs +61/−35
- README +2/−1
- RELEASENOTES +9/−2
- Setup.hs +0/−16
- linearEqSolver.cabal +4/−7
LICENSE view
@@ -1,4 +1,4 @@-linearEqSolver: Solves linear systems of equations over integers, using SMT solving.+linearEqSolver: Solves linear systems of equations, using SMT solving. Copyright (c) 2012, Levent Erkok (erkokl@gmail.com) All rights reserved.
Math/LinearEquationSolver.hs view
@@ -4,20 +4,22 @@ -- Copyright : (c) Levent Erkok -- License : BSD3 -- Maintainer : erkokl@gmail.com--- Stability : experimental+-- Stability : stable -- -- (The linear equation solver library is hosted at <http://github.com/LeventErkok/linearEqSolver>. -- Comments, bug reports, and patches are always welcome.) ----- Solvers for linear equations over integers. Both single solution and all+-- Solvers for linear equations over integers and rationals. Both single solution and all -- solution variants are supported. --------------------------------------------------------------------------------- module Math.LinearEquationSolver (- -- * Finding a solution+ -- * Solutions over Integers solveIntegerLinearEqs- -- * Finding all solutions , solveIntegerLinearEqsAll+ -- * Solutions over Rationals+ , solveRationalLinearEqs+ , solveRationalLinearEqsAll ) where import Data.SBV@@ -36,22 +38,19 @@ -- 2x + z = 8 -- @ ----- >>> solveIntegerLinearEqs [[2,3,4],[6,-3,9],[2,0,1]] [20,-6,8]+-- >>> solveIntegerLinearEqs [[2, 3, 4],[6, -3, 9],[2, 0, 1]] [20, -6, 8] -- Just [5,6,-2] -- -- In case there are no solutions, we will get `Nothing`: ----- >>> solveIntegerLinearEqs [[1], [1]] [2,3]+-- >>> solveIntegerLinearEqs [[1], [1]] [2, 3] -- Nothing -- -- Note that there are no solutions to this second system as it stipulates the unknown is -- equal to both 2 and 3. (Overspecified.) solveIntegerLinearEqs :: [[Integer]] -> [Integer] -> IO (Maybe [Integer])-solveIntegerLinearEqs coeffs res- | Just n <- check coeffs res- = extractModel `fmap` sat (buildConstraints n coeffs res)- | True- = error "solveIntegerLinearEqs: Received ill-formed input"+solveIntegerLinearEqs coeffs res = extractModel `fmap` sat cs+ where cs = buildConstraints "solveIntegerLinearEqs" coeffs res -- | Similar to `solveIntegerLinearEqs`, except returns all possible solutions. -- Note that there might be an infinite number of solutions if the system@@ -69,31 +68,58 @@ -- -- We have: ----- >>> take 3 `fmap` solveIntegerLinearEqsAll [[2,3,4],[6,-3,9]] [20,-6]+-- >>> take 3 `fmap` solveIntegerLinearEqsAll [[2, 3, 4],[6, -3, 9]] [20, -6] -- [[5,6,-2],[-8,4,6],[18,8,-10]] solveIntegerLinearEqsAll :: [[Integer]] -> [Integer] -> IO [[Integer]]-solveIntegerLinearEqsAll coeffs res- | Just n <- check coeffs res- = extractModels `fmap` allSat (buildConstraints n coeffs res)- | True- = error "solveIntegerLinearEqsAll: Received ill-formed input"+solveIntegerLinearEqsAll coeffs res = extractModels `fmap` allSat cs+ where cs = buildConstraints "solveIntegerLinearEqsAll" coeffs res --- | Check that the arguments are well-formed. Returns Just the number of variables needed--- if the arguments are well formed, otherwise Nothing.-check :: [[Integer]] -> [Integer] -> Maybe Int-check a b- | m > 0 && not (null ns) && all (== n) ns && m == lb- = Just n- | True- = Nothing- where m = length a- ns = map length a- n = head ns- lb = length b+-- | Solve a system of linear equations over rationals. Same as the integer+-- version `solveIntegerLinearEqs`, except it takes rational coefficients+-- and returns rational results.+--+-- Here's an example call, to solve the following system of equations:+--+-- @+-- 2.4x + 3.6y = 12+-- 7.2x - 5y = -8.5+-- @+--+-- >>> solveRationalLinearEqs [[2.4, 3.6],[7.2, -5]] [12, -8.5]+-- Just [245 % 316,445 % 158]+solveRationalLinearEqs :: [[Rational]] -> [Rational] -> IO (Maybe [Rational])+solveRationalLinearEqs coeffs res = (fmap from . extractModel) `fmap` sat cs+ where to = map (fromRational :: Rational -> AlgReal)+ from = map (toRational :: AlgReal -> Rational)+ cs = buildConstraints "solveRationalLinearEqs" (map to coeffs) (to res) --- | Build the constraints corresponding to the system given-buildConstraints :: Int -> [[Integer]] -> [Integer] -> Symbolic SBool-buildConstraints n coeffs res = do- xs <- mkFreeVars n- let rowEq row r = sum (zipWith (*) xs row) .== r- solve $ zipWith rowEq (map (map literal) coeffs) (map literal res)+-- | Solve a system of linear equations over rationals. Similar to `solveRationalLinearEqs`,+-- except it returns all solutions lazily.+--+-- Example system:+--+-- @+-- 2.4x + 3.6y = 12+-- @+--+-- In this case, the system has infinitely many solutions. We can compute three of them as follows:+--+-- >>> take 3 `fmap` solveRationalLinearEqsAll [[2.4, 3.6]] [12]+-- [[5 % 1,0 % 1],[0 % 1,10 % 3],[3 % 2,7 % 3]]+solveRationalLinearEqsAll :: [[Rational]] -> [Rational] -> IO [[Rational]]+solveRationalLinearEqsAll coeffs res = (map from . extractModels) `fmap` allSat cs+ where to = map (fromRational :: Rational -> AlgReal)+ from = map (toRational :: AlgReal -> Rational)+ cs = buildConstraints "solveRationalLinearEqsAll" (map to coeffs) (to res)++-- | Build the constraints as given by the coefficient matrix and the resulting vector+buildConstraints :: (Num a, SymWord a) => String -> [[a]] -> [a] -> Symbolic SBool+buildConstraints f coeffs res+ | m == 0 || any (/= n) ns || m /= length res+ = error $ f ++ ": received ill-formed input."+ | True+ = do xs <- mkFreeVars n+ let rowEq row r = sum (zipWith (*) xs row) .== r+ solve $ zipWith rowEq (map (map literal) coeffs) (map literal res)+ where m = length coeffs+ n:ns = map length coeffs
README view
@@ -1,7 +1,8 @@ linearEqSolver ============== -Solve systems of linear equations of many unknowns, using SMT solvers.+Solve systems of linear equations, using SMT solvers. Both integer only solutions, and solutions+over rationals are supported. Build Status ============
RELEASENOTES view
@@ -1,9 +1,16 @@ Hackage: <http://hackage.haskell.org/package/linearEqSolver> GitHub: <http://github.com/LeventErkok/linearEqSolver> -Latest Hackage released version: 1.0+Latest Hackage released version: 1.1 ======================================================================-Version 1.0, Not yet released+Version 1.1, 2012-10-22++ - Add solvers over rationals, in addition to just integers.+ - Adjust SBV dependency to >= 2.7 as we depend on the new Real+ instance for the AlgReal type.++======================================================================+Version 1.0, 2012-10-18 - Initial release, contains solver for integer linear equations.
Setup.hs view
@@ -1,18 +1,2 @@--------------------------------------------------------------------------------- |--- Module : Main--- Copyright : (c) Levent Erkok--- License : BSD3--- Maintainer : erkokl@gmail.com--- Stability : experimental------ Setup module for the linearEqSolver library--------------------------------------------------------------------------------{-# OPTIONS_GHC -Wall #-}-module Main(main) where- import Distribution.Simple--main :: IO () main = defaultMain
linearEqSolver.cabal view
@@ -1,13 +1,10 @@ Name: linearEqSolver-Version: 1.0+Version: 1.1 Category: Math, SMT-Synopsis: Solve linear systems of equations over integers.-Description: Express and solve linear systems of equations over integers, using an SMT solver to do the actual solving.+Synopsis: Use SMT solvers to solve linear systems of equations over integers and rationals.+Description: Express and solve linear systems of equations over integers and rationals, using an SMT solver to do the actual solving. By default, we use Microsoft's Z3 SMT solver (<http://research.microsoft.com/en-us/um/redmond/projects/z3/>). .- You can get a single solution if it exists. Or ask for all possible solutions for underspecified- systems, which will be lazily returned in a list.- . linearEqSolver is hosted at GitHub: <http://github.com/LeventErkok/linearEqSolver>. Comments, bug reports, and patches are always welcome. .@@ -34,5 +31,5 @@ default-language: Haskell2010 ghc-options : -Wall Build-Depends : base >= 4 && < 5- , sbv+ , sbv >= 2.7 Exposed-modules : Math.LinearEquationSolver