scratch
§ Modular Arithmetic Decision Procedure
created 2025-12-15
- Modular Arithmetic Decision Procedure by Domagoj and Madanlal
- For bounded integers, actually just perform the hensel lifting. Can handle polynomial fragment.
- I am not sure why this is supposed to be better than just performing a bit-encoding followed by bitblasting, by deriving the width bounds.
- I suppose the idea is that if the system is linear, then linear algebra can help us find the seed solution, and lifts should also be faster?
❦