diff --git a/COPYRIGHT b/COPYRIGHT new file mode 100644 --- /dev/null +++ b/COPYRIGHT @@ -0,0 +1,5 @@ +Copyright (c) 2012, Levent Erkok (erkokl@gmail.com) +All rights reserved. + +The linearEqSolver library is distributed with the BSD3 license. See the LICENSE file +for details. diff --git a/INSTALL b/INSTALL new file mode 100644 --- /dev/null +++ b/INSTALL @@ -0,0 +1,10 @@ +The linearEqSolver library can be installed simply by issuing cabal install +like this: + + cabal install linearEqSolver + +The library uses the sbv package on hackage, which will automatically be +installed if you do not have it already. You should also install +Z3, the default SMT solver used by sbv, from Microsoft. (You can get it +from http://research.microsoft.com/en-us/um/redmond/projects/z3/.) +Please make sure that the "z3" executable is in your path. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,26 @@ +linearEqSolver: Solves linear systems of equations over integers, using SMT solving. + +Copyright (c) 2012, Levent Erkok (erkokl@gmail.com) +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + * Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + * Neither the name of the developer (Levent Erkok) nor the + names of its contributors may be used to endorse or promote products + derived from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND +ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL LEVENT ERKOK BE LIABLE FOR ANY +DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES +(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND +ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Math/LinearEquationSolver.hs b/Math/LinearEquationSolver.hs new file mode 100644 --- /dev/null +++ b/Math/LinearEquationSolver.hs @@ -0,0 +1,99 @@ +--------------------------------------------------------------------------------- +-- | +-- Module : Math.LinearEquationSolver +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- (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 +-- solution variants are supported. +--------------------------------------------------------------------------------- + +module Math.LinearEquationSolver ( + -- * Finding a solution + solveIntegerLinearEqs + -- * Finding all solutions + , solveIntegerLinearEqsAll + ) where + +import Data.SBV + +-- | Solve a system of linear integer equations. The first argument is +-- the matrix of coefficients, known as @A@, of size @mxn@. The second argument +-- is the vector of results, known as @B@, of size @mx1@. The result will be +-- either `Nothing`, if there is no solution, or @Just x@ -- such that @Ax = B@ holds. +-- (Naturally, the result @x@ will be a vector of size @nx1@ in this case.) +-- +-- Here's an example call, to solve the following system of equations: +-- +-- @ +-- 2x + 3y + 4z = 20 +-- 6x - 3y + 9z = -6 +-- 2x + z = 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] +-- 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" + +-- | Similar to `solveIntegerLinearEqs`, except returns all possible solutions. +-- Note that there might be an infinite number of solutions if the system +-- is underspecified, in which case the result will be a lazy list of solutions +-- that the caller can consume as much as needed. +-- +-- Here's an example call, where we underspecify the system and hence there are +-- multiple (in this case an infinite number of) solutions. Here, we only take the first 3 elements, +-- for testing purposes, but all such results can be computed lazily. Our system is: +-- +-- @ +-- 2x + 3y + 4z = 20 +-- 6x - 3y + 9z = -6 +-- @ +-- +-- We have: +-- +-- >>> 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" + +-- | 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 + +-- | 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) diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -0,0 +1,9 @@ +linearEqSolver +============== + +Solve systems of linear equations of many unknowns, using SMT solvers. + +Build Status +============ +We use Travis-CI's automated build infrastructure, making a build for each commit. Current build status: +[![Build Status](https://secure.travis-ci.org/LeventErkok/linearEqSolver.png?branch=master)](http://travis-ci.org/LeventErkok/linearEqSolver) diff --git a/RELEASENOTES b/RELEASENOTES new file mode 100644 --- /dev/null +++ b/RELEASENOTES @@ -0,0 +1,9 @@ +Hackage: +GitHub: + +Latest Hackage released version: 1.0 + +====================================================================== +Version 1.0, Not yet released + + - Initial release, contains solver for integer linear equations. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,18 @@ +----------------------------------------------------------------------------- +-- | +-- 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 new file mode 100644 --- /dev/null +++ b/linearEqSolver.cabal @@ -0,0 +1,38 @@ +Name: linearEqSolver +Version: 1.0 +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. + 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. + . + . + Release notes can be seen at: . + +Copyright: Levent Erkok, 2012 +License: BSD3 +License-file: LICENSE +Stability: Experimental +Author: Levent Erkok +Homepage: http://github.com/LeventErkok/linearEqSolver +Bug-reports: http://github.com/LeventErkok/linearEqSolver/issues +Maintainer: Levent Erkok (erkokl@gmail.com) +Build-Type: Simple +Cabal-Version: >= 1.14 +Extra-Source-Files: INSTALL, README, COPYRIGHT, RELEASENOTES + +source-repository head + type: git + location: git://github.com/LeventErkok/linearEqSolver.git + +Library + default-language: Haskell2010 + ghc-options : -Wall + Build-Depends : base >= 4 && < 5 + , sbv + Exposed-modules : Math.LinearEquationSolver