On Mon, Oct 15, 2012 at 9:00 AM, Johannes Waldmann wrote:

Justin Paston-Cooper 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-Exampl... 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-Commuta... While the approach here only applies to linear diophantine equations, you might be able to adapt it to your particular needs. -Levent.

On Oct 17, 2012, at 3:35 AM, Justin Paston-Cooper wrote:

Thanks for all the informative replies. SBV seems the simplest solution right now, and speed isn't too much of an issue here. Anything under 20 seconds per solution should be bearable.

I'm happy to announce the SMT based linear equation solver library: http://hackage.haskell.org/package/linearEqSolver You can use it get solutions over Integers only, or over Rationals if so needed. Functions are provided to extract one solution, or all possible solutions (as a lazy list). The latter variant is useful for underspecified systems. Regarding performance: SMT solvers are very good at solving such equations, so aside from the overhead of calling out to an external program, it should be fairly fast. I'd expect no practical instance to come to anywhere near the 20 second limit you've mentioned. For most practical instances, the process switch overhead would dominate computation time, which should be negligible. Let me know if you find otherwise. -Levent.