Re: [isabelle] Modular arithmetic theory?



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.









This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.