Re: [Haskell-cafe] Solving integer equations in Haskell

2012-10-21 Thread Levent Erkok
On Oct 17, 2012, at 3:35 AM, Justin Paston-Cooper paston.coo...@gmail.com 
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. ___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Solving integer equations in Haskell

2012-10-17 Thread Justin Paston-Cooper
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.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Solving integer equations in Haskell

2012-10-17 Thread John D. Ramsdell
For Linear integer equations, I think you want

http://hackage.haskell.org/packages/archive/agum/2.4/doc/html/Algebra-AbelianGroup-IntLinEq.html

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 erk...@gmail.com wrote:
 On Mon, Oct 15, 2012 at 9:00 AM, Johannes Waldmann
 waldm...@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.

 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] Solving integer equations in Haskell

2012-10-15 Thread Justin Paston-Cooper
Hello,

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? I'm aware that Mathematica can do
this, but I would like something written in Haskell. I haven't been sure of
what exact keywords I should be searching for, hence my asking here.

Thanks,

Justin
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Solving integer equations in Haskell

2012-10-15 Thread Arie Peterson
 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? I'm aware that Mathematica can do this,
 but I would like something written in Haskell. I haven't been sure of what
 exact keywords I should be searching for, hence my asking here.

You may interpret the function x ↦ x M transpose(x) as a quadratic form on the 
additive group of vectors. The group of integer vectors, together with such a 
quadratic form, is usually called a /lattice/ (not to be confused with its 
other meaning, of a set with a partial order and some meet/join operators).

A vector x satisfying your equation is sometimes said to /represent/ the 
number y, with respect to the quadratic form.

On hackage, a quick search gives the Lattices package, which seems related. 
(There is also the lattices package, but this is about the other lattices.)


Incidentally, I also have use for this functionality, but specifically for 
vectors with 2 components (so the quadratic form is then binary). The equation 
is then a generalised Pell equation, and I think I have read somewhere how to 
solve it. If such code does not exist yet, I will probably write it, but this 
might not be very soon.


Regards,

Arie


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Solving integer equations in Haskell

2012-10-15 Thread Johannes Waldmann
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.

Use SBV to write the constraints programmatically
http://hackage.haskell.org/package/sbv

J.W.



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Solving integer equations in Haskell

2012-10-15 Thread Levent Erkok
On Mon, Oct 15, 2012 at 9:00 AM, Johannes Waldmann
waldm...@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.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe