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.

John

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.
>
> -Levent.
>
> _______________________________________________