Scimitar: Functional Programs as Optimization Problems
summary
Scimitar compiles a functional subset into MILP constraints (implemented in Racket) and automatically applies expert encodings like McCormick envelopes for variable multiplication, targeting solvers such as Gurobi and CBC. Benchmarks include max-flow, resource allocation, arena allocation and student recitation; compile times are high but solve times are usually faster than Rosette/Z3, with several Rosette runs hitting a 20-minute timeout. The system produces correct optimal solutions and scales well on tested problems.
AI-written summary · about
chapters (14)
- 0:00Scimitar introduction and goals
- 1:07Optimization in functional programming
- 2:35Mathematical optimization background
- 4:20Expert encodings in MILP challenges
- 7:36Solver-aided languages limitations
- 8:19Scimitar’s FP and optimization combo
- 9:01Memory allocator practical example
- 13:39Host solver boundary crossing
- 14:44Automatic expert encodings key
- 15:04McCormick envelopes variable multiplication
- 18:59Benchmarks and problem demos
- 20:24Rosette performance comparison
- 22:33Scimitar’s advantages summary
- 23:15Q&A
related talks
30mAnalyzing Programs with SMT Solvers
28mFunctional Sparse Tensor Compilation
35mThe Mastermind behind Refinement Types
55mScalable Quantum Compilation With Jasp
22mSatisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing
19mMinotaur: A SIMD-Oriented Synthesizing Superoptimizer
15mScaling Optimization Over Uncertainty via Compilation
51mSynthesis and Verification for All