*To*: John Matthews <matthews at galois.com>*Subject*: Re: [isabelle] Modular arithmetic theory?*From*: Michael Norrish <Michael.Norrish at nicta.com.au>*Date*: Thu, 17 Nov 2005 09:26:24 +1100*Cc*: isabelle-users at cl.cam.ac.uk, Hasan Amjad <ha227 at cam.ac.uk>, Burkhart Wolff <bwolff at inf.ethz.ch>*In-reply-to*: <2F04C324-C280-4CE4-BA8A-894B0D332B51@galois.com>*References*: <2F04C324-C280-4CE4-BA8A-894B0D332B51@galois.com>*Reply-to*: Michael Norrish <Michael.Norrish at nicta.com.au>

John Matthews writes: > Thanks everyone for your investigation into this! It looks like I > may have to write some specialized tactics for modular arithmetic to > get enough performance. I have been hacking HOL's implementation of the Omega Test, and can now prove (x MOD c + y MOD c) MOD c = (x + y) MOD c for arbitrary c in "reasonable" time. For example, with c = 1000, the time taken is 1.6s. For c = 2^32, the time is 4s which suggests time proportional to the log of the exponent (i.e., that it's internal arithmetic on the coefficients that bottlenecks). Running an ML with a better compiler than Moscow ML should help a lot with these numbers I expect. Even with so-called "delta-elimination" enabled, I can't get comparable performance out of Cooper's algorithm, which is a shame. The key to the win in performance came from noticing that there is a universal and existential version of the formula characterising P(x MOD y), which means you can avoid introducing alternating quantifiers in a goal such as the one above. Until I saw Amine's universal version, I had been using the existential version that I posted to the Isabelle user list. > However, Hasan Amjad pointed me to an interesting paper by Domagoj > Babic and Madanlal Musuvathi on a decision procedure for integers mod > 2^k (which is really what I'm interested in). It also supports non- > linear terms and inequalities. It's the first publication on > Domagoj's web page: > http://www.cs.ubc.ca/~babic > No performance numbers, though. I'm glad that's up - when I wrote to him earlier Domagoj said it was still "lost" inside MSR. The paper also has some references to systems that solve by converting to SAT. Michael.

**Follow-Ups**:**Re: [isabelle] Modular arithmetic theory?***From:*Amine Chaieb

**References**:**Re: [isabelle] Modular arithmetic theory?***From:*John Matthews

- Previous by Date: Re: [isabelle] Modular arithmetic theory?
- Next by Date: [isabelle] JAR issue on Empirically Successful Automated Reasoning
- Previous by Thread: Re: [isabelle] Modular arithmetic theory?
- Next by Thread: Re: [isabelle] Modular arithmetic theory?
- Cl-isabelle-users November 2005 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list