FPL: Fast Presburger Arithmetic through Transprecision
summary
A new C++ Presburger library lives inside MLIR and targets real polyhedral workloads: a benchmark of over 1,000,000 extracted Presburger cases shows coefficients are tiny (90% zeros, 99% ≤512) and 90% of sets have ≤10 dimensions, so most work fits in short integers. The library uses library-level transprecision (templated instantiations that throw on overflow and retry at higher precision) to enable vectorized SIMD on 16–32-bit rows, yielding about a 5.25x speedup versus isl default and 3.14x versus an optimized isl variant.
AI-written summary · about
chapters (14)
- 0:00Start
- 2:16The basic building blocks: Integer Polyhedra
- 3:27The internal representation
- 5:05Transprecision Computing
- 7:30Set Operations: Intersection
- 7:51Set Operations: Complement
- 8:45Set Operations: Checking Integer Emptiness
- 9:59Algorithmic Design
- 10:42Evaluation
- 10:53Applicability of Transprecision
- 11:41Speedups over isl (GMP)
- 12:08Library-level transprecision has low overhead
- 13:00FPL is developed within LLVM/MLIR
- 13:52Conclusion
related talks
14mFast Linear Programming through Transprecision Computing on Small and Sparse Data
58mPortable floating-point calculations
14mFast and Efficient Bit-Level Precision Tuning
22mOne Polynomial Approximation to Produce Correctly Rounded Results of an Elementa
26mGenerating Correctly Rounded Math Libraries for New Floating Point Variants
15mPushing the Packed SIMD Extension Over the Line: An Update on the Progress of Key RISC...
15mSealing Pointer-Based Optimizations Behind Pure Functions
30mBit-Precise Reasoning via Int-Blasting