diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -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. diff --git a/Math/LinearEquationSolver.hs b/Math/LinearEquationSolver.hs --- a/Math/LinearEquationSolver.hs +++ b/Math/LinearEquationSolver.hs @@ -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 . -- 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 diff --git a/README b/README --- a/README +++ b/README @@ -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 ============ diff --git a/RELEASENOTES b/RELEASENOTES --- a/RELEASENOTES +++ b/RELEASENOTES @@ -1,9 +1,16 @@ Hackage: GitHub: -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. diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -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 diff --git a/linearEqSolver.cabal b/linearEqSolver.cabal --- a/linearEqSolver.cabal +++ b/linearEqSolver.cabal @@ -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 (). . - 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: . 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