[Haskell-cafe] Linear Diaphantine equation solver bug

[John D. Ramsdell]

Recall I reported a surprising result from an implementation of a
Linear Diophantine equation solver based on an algorithm by Contejean
and Devie.  When using it to solve an inhomogeneous equation, a
version of my code generated a non-minimal solution.  It turns out
that when solving the inhomogeneous problem, one must filter out
solutions to the homogeneous problem.  This was not clear from the
description of the algorithm I used, but a careful analysis of the
section on inhomogeneous equations in the Contejean and Devie papers
makes clear the correct fix.

In other news, Levent Erkok sent news about his SVB package.

John

Levent:

In case this is of any interest to you; the latest release of SBV now
has a diophantine solver example:

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

It's generalized to a system of equations instead of just one, and
uses the underlying SMT solver to find the minimal solutions. I see it
as a nice complement to your work, where one can check the results of
your solver against the SBV produced one for extra assurance if
needed.

On Wed, Apr 25, 2012 at 7:09 PM, John D. Ramsdell <ramsdell0 at gmail.com> wrote:
> I uploaded a new version of the ACU unifier in package cmu.  It
> includes a Linear Diophantine equation solver that now handles
> inhomogeneous equations.  What's interesting  is the algorithm is
> based on a paper by Contejean and Devie.  That paper includes a proof
> of correctness of their algorithm.  Yet I found an example in which
> following the steps in the order they gave, the algorithm produces
> extra answers.  I had to switch the order of the steps in the
> algorithm to get the right answer.  I wonder if anyone else knows of
> this issue.  The example is given in the module documentation on
> Hackage.
>
> John
>
> http://hackage.haskell.org/packages/archive/cmu/1.7/doc/html/Algebra-CommutativeMonoid-LinDiophEq.html