[Haskell-cafe] Solving integer equations in Haskell

[Levent Erkok]

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:

  http://hackage.haskell.org/packages/archive/sbv/2.3/doc/html/Data-SBV-Examples-Existentials-Diophantine.html

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:

    http://hackage.haskell.org/packages/archive/cmu/1.8/doc/html/Algebra-CommutativeMonoid-LinDiophEq.html

While the approach here only applies to linear diophantine equations,
you might be able to adapt it to your particular needs.

-Levent.