[Haskell-cafe] Solving integer equations in Haskell
John D. Ramsdell
ramsdell0 at gmail.com
Thu Oct 18 01:58:19 CEST 2012
For Linear integer equations, I think you want
The algorithm used to find solutions is described in Vol. 2 of The Art
of Computer Programming / Seminumerical Alorithms, 2nd Ed., 1981, by
Donald E. Knuth, pg. 327.
On Mon, Oct 15, 2012 at 10:39 PM, Levent Erkok <erkokl at gmail.com> wrote:
> On Mon, Oct 15, 2012 at 9:00 AM, Johannes Waldmann
> <waldmann at imn.htwk-leipzig.de> wrote:
>> Justin Paston-Cooper <paston.cooper <at> gmail.com> writes:
>>> Can anyone suggest a library written in Haskell which can solve equations
>>> of the form xM(transpose(x)) = y, where x should be an integer vector,
>>> M is an integer matrix and y is an integer?
>> when in doubt, use brute force:
>> write this as a constraint system
>> (in QF_NIA or QF_BV logics) and solve with Z3.
> As Johannes mentioned, you can indeed use SBV/Z3 to solve such
> problems. Indeed, there's an existing example for showing how to solve
> Diophantine equations this way:
> The technique described there can be used to solve the problem you've
> described; or systems of arbitrary constraint equations in general
> with minor tweaks.
> Having said that, using an SMT solver for this problem may not
> necessarily be the fastest route. The general purpose nature of SMT
> solving, while sound and complete for this class of problems, are not
> necessarily the most efficient when there are existing fast
> algorithms. In particular, you should check out John Ramsdell's cmu
> package: http://hackage.haskell.org/package/cmu. In particular see:
> While the approach here only applies to linear diophantine equations,
> you might be able to adapt it to your particular needs.
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe